Selon cet article , qui discute d'une extension non déterministe de l' hypothèse de temps exponentiel fort (SETH), "[…] Williams a récemment montré que les hypothèses liées à la complexité de Merlin-Arthur de k-TAUT sont fausses". Cependant, ce document ne cite qu'une communication personnelle.
Comment la version MA de SETH est-elle avérée fausse?
Je soupçonne que cela implique l' algèbre de la formule, mais je n'ai aucune autre idée.
sat
proofs
nondeterminism
argentpepper
la source
la source
Réponses:
Vous pouvez trouver une préimpression en suivant ce lien http://eccc.hpi-web.de/report/2016/002/
EDIT (1/24) Sur demande, voici un bref résumé, tiré du papier lui-même, mais passant sous silence beaucoup de choses. Supposons que Merlin peut se révéler Arthur que , pour un circuit arithmétique -variable C , sa valeur sur tous les points dans { 0 , 1 } k est un certain tableau de 2 k éléments de champ, dans le temps au sujet ( s + 2 k ) ⋅ d , où s est la taille de C et d est le degré du polynôme calculé par Ck C {0,1}k 2k (s+2k)⋅d s C d C . (Nous appelons cela une "courte preuve non interactive d'évaluation par lots" --- évaluation de sur de nombreuses affectations.)C
Merlin peut alors résoudre SAT pour Arthur comme suit. Étant donné un CNF F sur n variables et m clauses, Merlin et Arthur construisent d'abord un circuit arithmétique C sur n / 2 variables de degré au plus m n , d'une taille d'environ m n ⋅ 2 n / 2 , qui prend une somme sur toutes les affectations à les n / 2 premières variables du CNF F (en ajoutant 1 à la somme lorsque F est vrai, et 0# F n m C n/2 mn mn⋅2n/2 n/2 F 1 F 0 quand c'est faux). En utilisant le protocole d'évaluation par lots, Merlin peut alors prouver que prend 2 n / 2 valeurs particulières sur toutes ses 2 n / 2 affectations booléennes, en environ 2 n / 2 p o l y ( n , m ) temps. Résumant toutes ces valeurs, nous obtenons le nombre des affectations SAT à F .C 2n/2 2n/2 2n/2poly(n,m) F
Maintenant, nous disons à un niveau élevé comment faire le protocole d'évaluation par lots. Nous voulons que la preuve soit une représentation succincte du circuit qui soit à la fois facile à évaluer sur toutes les 2 k entrées données, et aussi facile à vérifier par hasard. Nous définissons la preuve comme un polynôme univarié Q ( x ) défini sur un champ d'extension suffisamment grand du champ de base K (de caractéristique au moins 2 n pour notre application), où Q ( x ) a un degré d'environ 2 k ⋅ d , et Q `` esquisse '' l'évaluation du diplômeC 2k Q(x) K 2n Q(x) 2k⋅d Q circuit arithmétique C sur toutes les 2 k assignations. Le polynôme Q satisfait deux conditions conflictuelles:d C 2k Q
Le vérificateur peut utiliser le schéma pour produire efficacement la table de vérité de C . En particulier, pour certains α i explicitement connus à partir de l'extension de K , nous voulons ( Q ( α 0 ) , Q ( α 1 ) , … , Q ( α K ) ) = ( C ( a 1 ) , … , C ( a 2 K ) ) , où unQ C αi K (Q(α0),Q(α1),…,Q(αK))=(C(a1),…,C(a2K)) est la i ème affectation booléenne aux k variables de C (sous un certain ordre sur les affectations).ai i k C
Le vérificateur peut vérifier que est une représentation fidèle du comportement de C sur toutes les affectations booléennes de 2 k , dans environ 2 k + s de temps, avec un caractère aléatoire. Cela devient fondamentalement un test d'identité polynomiale univariée.Q C 2k 2k+s
La construction de utilise une astuce d'interpolation issue des preuves holographiques, où les expressions multivariées peuvent être efficacement `` exprimées '' comme univariées. Les deux éléments utilisent des algorithmes rapides pour manipuler des polynômes univariés.Q
la source