Czy „teoria złożoności eksperymentalnej” jest używana do rozwiązywania otwartych problemów?

Scott Aaronson zaproponował interesujące wyzwanie : czy możemy dziś wykorzystać superkomputery, aby pomóc rozwiązać problemy z CS w taki sam sposób, w jaki fizycy używają zderzaczy dużych cząstek?

Mówiąc konkretniej, moja propozycja polega na poświęceniu części światowej mocy obliczeniowej na całkowitą próbę odpowiedzi na następujące pytania: czy obliczenie stałej macierzy 4 na 4 wymaga więcej operacji arytmetycznych niż obliczenie jej wyznacznika?

Dochodzi do wniosku, że wymagałoby to ~ operacji zmiennoprzecinkowych, co przekracza nasze obecne środki. Te slajdy są dostępne i są warte czytania. $10^{123}$

Czy istnieje jakikolwiek priorytet w rozwiązywaniu otwartych problemów TCS poprzez eksperymenty z użyciem siły brutalnej?

W „Finding Efficient Circuits With Solver-SATvers” Kojevnikov, Kulikov i Yaroslavtsev zastosowali solvery SAT do znalezienia lepszych obwodów do obliczania funkcji .$MOD_k$

Użyłem komputerów, aby znaleźć dowody na dolne granice czasoprzestrzeni, jak opisano tutaj . Ale było to możliwe tylko dlatego, że pracowałem z niezwykle restrykcyjnym systemem dowodowym.

Maverick Woo i ja pracowaliśmy od jakiegoś czasu, aby znaleźć „właściwą” domenę do sprawdzania górnych / dolnych granic obwodu za pomocą komputerów. Mieliśmy nadzieję, że możemy rozwiązać vs (lub jego bardzo słabą wersję) za pomocą solverów SAT, ale wydaje się to coraz bardziej mało prawdopodobne. (Mam nadzieję, że Maverick nie ma nic przeciwko, że to powiem ...) A C C $CC^0$$ACC^0$

Pierwszym ogólnym problemem związanym z użyciem wyszukiwania z użyciem siły brutalnej do udowodnienia nietrywialnych dolnych granic jest to, że zajmuje to zbyt cholernie długo, nawet na bardzo szybkim komputerze. Alternatywą jest próba użycia solverów SAT, QBF lub innych zaawansowanych narzędzi optymalizacyjnych, ale nie wydają się one wystarczające, aby zrównoważyć ogrom przestrzeni wyszukiwania. Problemy z syntezą obwodów należą do najtrudniejszych praktycznych przypadków.

Drugi ogólny problem polega na tym, że „dowód” wynikającej z tego dolnej granicy (uzyskany przez przeszukanie brutalnej siły i znalezienie niczego) byłby niesamowicie długi i najwyraźniej nie dałby wglądu (poza faktem, że dolna granica się utrzymuje). Tak więc dużym wyzwaniem dla „eksperymentalnej teorii złożoności” jest znalezienie interesujących dolnych granic, dla których ostateczny „dowód” dolnej granicy jest wystarczająco krótki, aby można go było zweryfikować i wystarczająco interesujący, aby doprowadzić do dalszych spostrzeżeń.

Wiele z najlepszych granic w teorii Ramseya odbywa się poprzez brutalne wymuszanie przez zestawy sprytnie wygenerowanych (nieizomorficznych) wykresów. Postęp w teorii Ramseya zasadniczo zmienia się pomiędzy postępem matematycznym i obliczeniowym problemu.

Ogólnie rzecz biorąc, brutalna siła komputerowa jest często używana do uzyskania dowodów na domniemania, gdy nie wiadomo, że istnieją dowody. Na przykład hipoteza Goldbacha i hipoteza Riemanna zostały zweryfikowane przez wyszukiwanie komputerowe do bardzo dużej liczby.