Wird „Experimentelle Komplexitätstheorie“ zur Lösung offener Probleme verwendet?

Scott Aaronson schlug eine interessante Herausforderung vor : Können wir heute Supercomputer einsetzen, um CS-Probleme auf dieselbe Weise zu lösen, wie Physiker Kollider für große Teilchen einsetzen?

Konkreter ist mein Vorschlag, einen Teil der Rechenleistung der Welt für einen umfassenden Versuch zu verwenden, Fragen wie die folgenden zu beantworten: Benötigt die Berechnung der Permanenz einer 4-mal-4-Matrix mehr arithmetische Operationen als die Berechnung ihrer Determinante?

Er kommt zu dem Schluss, dass dies ~ Gleitkommaoperationen erfordern würde , die über unseren derzeitigen Möglichkeiten liegen. Die Folien sind vorhanden und auch lesenswert. $10^{123}$

Gibt es einen Präzedenzfall für die Lösung offener TCS-Probleme durch Brute-Force-Experimente?

In "Effiziente Schaltkreise mit SAT-Solvern finden" haben Kojevnikov, Kulikov und Yaroslavtsev mit SAT-Solvern bessere Schaltkreise für die Berechnung der Funktion gefunden.$MOD_k$

Ich habe Computer verwendet, um Beweise für Zeit-Raum-Untergrenzen zu finden, wie hier beschrieben . Das war aber nur möglich, weil ich mit einem extrem restriktiven Beweissystem gearbeitet habe.

Maverick Woo und ich arbeiten seit einiger Zeit daran, die "richtige" Domäne für den Nachweis der oberen / unteren Grenzen von Schaltkreisen mithilfe von Computern zu finden. Wir hatten gehofft, dass wir gegen (oder eine sehr schwache Version davon) mit SAT-Solvern auflösen können , aber dies scheint immer unwahrscheinlicher. (Ich hoffe, Maverick macht es nichts aus, wenn ich das sage ...)$CC^0$$ACC^0$

Das erste generelle Problem bei der Verwendung der Brute-Force-Suche zum Nachweis nichttrivialer Untergrenzen ist, dass es selbst auf einem sehr schnellen Computer einfach zu lange dauert. Die Alternative besteht darin, SAT-Löser, QBF-Löser oder andere hochentwickelte Optimierungswerkzeuge zu verwenden, die jedoch nicht ausreichen, um die enorme Größe des Suchraums auszugleichen. Schaltkreissyntheseprobleme gehören zu den schwierigsten praktischen Beispielen.

Das zweite generische Problem ist, dass der "Beweis" der resultierenden Untergrenze (erhalten durch Ausführen von Brute-Force-Suche und Finden von nichts) wahnsinnig lang ist und anscheinend keine Einsicht ergibt (abgesehen von der Tatsache, dass die Untergrenze gilt). Eine große Herausforderung für die "experimentelle Komplexitätstheorie" besteht also darin, interessante untere Schranken zu finden, für die der mögliche "Beweis" der unteren Schranke kurz genug ist, um überprüfbar zu sein, und interessant genug, um zu weiteren Einsichten zu führen.

Viele der besten Schranken in der Ramsey-Theorie werden durch brachiales Erzwingen von Sätzen geschickt erzeugter (nicht-isomorpher) Graphen gezogen. Fortschritte in der Ramsey-Theorie schwanken im Allgemeinen zwischen mathematischen und rechnerischen Fortschritten.

Im Allgemeinen wird Computer-Brute-Force häufig eingesetzt, um Beweise für Vermutungen zu erhalten, wenn keine Beweise bekannt sind. Zum Beispiel wurden die Goldbach-Vermutung und die Riemann-Hypothese durch Computersuche bis zu einer sehr großen Anzahl verifiziert.