La «théorie de la complexité expérimentale» est-elle utilisée pour résoudre des problèmes ouverts?

Scott Aaronson a proposé un défi intéressant : pouvons-nous utiliser des superordinateurs aujourd'hui pour aider à résoudre les problèmes de CS de la même manière que les physiciens utilisent de grands collisionneurs de particules?

Plus concrètement, ma proposition est de consacrer une partie de la puissance de calcul mondiale à une tentative totale de répondre à des questions comme les suivantes: le calcul du permanent d'une matrice 4 par 4 nécessite-t-il plus d'opérations arithmétiques que le calcul de son déterminant?

Il conclut que cela nécessiterait ~ opérations en virgule flottante, ce qui est au-delà de nos moyens actuels. Les diapositives sont disponibles et valent également la peine d'être lues. $10^{123}$

Y a-t-il une priorité pour résoudre les problèmes de TCS ouverts grâce à l'expérimentation par force brute?

Dans "Trouver des circuits efficaces en utilisant des solveurs SAT", Kojevnikov, Kulikov et Yaroslavtsev ont utilisé des solveurs SAT pour trouver de meilleurs circuits pour calculer la fonction .$MOD_k$

J'ai utilisé des ordinateurs pour trouver des preuves de limites inférieures d'espace-temps, comme décrit ici . Mais cela n'était possible que parce que je travaillais avec un système de preuve extrêmement restrictif.

Maverick Woo et moi travaillons depuis un certain temps pour trouver le "bon" domaine pour prouver les limites supérieures / inférieures des circuits à l'aide d'ordinateurs. Nous espérions pouvoir résoudre vs A C C 0 (ou une version très faible de celui-ci) en utilisant des solveurs SAT, mais cela semble de plus en plus improbable. (J'espère que Maverick ne me dérange pas de dire cela ...)$CC^0$$ACC^0$

Le premier problème générique avec l'utilisation de la recherche par force brute pour prouver les limites inférieures non triviales est que cela prend trop de temps, même sur un ordinateur très rapide. L'alternative est d'essayer d'utiliser des solveurs SAT, des solveurs QBF ou d'autres outils d'optimisation sophistiqués, mais ils ne semblent pas être suffisants pour compenser l'énormité de l'espace de recherche. Les problèmes de synthèse de circuits sont parmi les cas pratiques les plus difficiles à résoudre.

Le deuxième problème générique est que la "preuve" de la borne inférieure résultante (obtenue en exécutant une recherche par force brute et en ne trouvant rien) serait incroyablement longue et ne donnerait apparemment aucune idée (autre que le fait que la borne inférieure soit vérifiée). Ainsi, un grand défi à la "théorie de la complexité expérimentale" est de trouver des questions de borne inférieure intéressantes pour lesquelles la "preuve" finale de la borne inférieure est suffisamment courte pour être vérifiable, et suffisamment intéressante pour conduire à de nouvelles perspectives.

La plupart des meilleures limites de la théorie de Ramsey sont obtenues par forçage brutal à travers des ensembles de graphiques (non isomorphes) intelligemment générés. Les progrès de la théorie de Ramsey fluctuent généralement entre les avancées mathématiques et informatiques du problème.

En général, la force brute informatique est souvent utilisée pour obtenir des preuves de conjectures quand aucune preuve n'est connue. Par exemple, la conjecture de Goldbach et l' hypothèse de Riemann ont été vérifiées par recherche informatique jusqu'à de très grands nombres.