Classes bien connues de formules booléennes qui nécessitent des preuves de résolution exponentiellement longues

Vous pouvez souvent trouver des méthodes de plan de coupe, de propagation variable, de branchement et de limite, d'apprentissage de clause, de retour en arrière intelligent ou même d'heuristique humaine tissée à la main dans les solveurs SAT. Pourtant, pendant des décennies, les meilleurs solveurs SAT se sont largement appuyés sur des techniques de preuve de résolution et utilisent une combinaison d'autres choses simplement pour l'aide et pour diriger la recherche de style de résolution. De toute évidence, on soupçonne que TOUT algorithme ne parviendra pas à décider de la question de satisfiabilité en temps polynomial dans au moins certains cas.

En 1985, Haken a prouvé dans son article "L'intractabilité de la résolution" que le principe des trous de pigeon codé en CNF n'admettait pas les preuves de résolution de taille polynomiale. Bien que cela prouve quelque chose sur l'intractabilité des algorithmes basés sur la résolution, cela donne également des critères par lesquels les solveurs de pointe peuvent être jugés - et en fait, l'une des nombreuses considérations qui entrent dans la conception d'un solveur SAT aujourd'hui est de savoir comment il est susceptible de fonctionner sur des cas «durs» connus.

Avoir une liste de classes de formules booléennes qui admettent de manière prouvable des preuves de résolution de taille exponentielle est utile dans le sens où cela donne des formules «dures» pour tester de nouveaux solveurs SAT. Quel travail a été fait pour compiler ces classes ensemble? Quelqu'un at-il une référence contenant une telle liste et leurs preuves pertinentes? Veuillez énumérer une classe de formule booléenne par réponse.

Instances matérielles de résolution :

1. Formules de Tseitin (sur les graphiques d'expansion).

2. $m$$n$$n$$m>n$

3. $n$$O(n^{1.5-\epsilon})$$0<\epsilon<1/2$

Bonne étude technique, relativement à jour pour les limites inférieures de la complexité de la preuve, voir:

Nathan Segerlind: La complexité des preuves propositionnelles. Bulletin of Symbolic Logic 13 (4): 417-481 (2007) disponible sur: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

Il existe un certain nombre de bonnes enquêtes et d'ouvrages sur la complexité des preuves propositionnelles qui contiennent de telles listes. De nombreux systèmes de preuve p-simulent la résolution, donc toute formule qui leur est difficile sera difficile à résoudre.

Livres:
1. Jan Krajicek, "Arithmétique bornée, logique propositionnelle et théorie de la complexité", 1995
2. Stephen A. Cook et Phoung The Neguyen, "Fondements logiques de la complexité de la preuve", 2010

Enquêtes:
1. Paul Beame et Toniann Pitassi, «Complexité de la preuve propositionnelle: passé, présent et futur», 2001
2. Samuel R. Buss, «Complexité de la preuve arithmétique et propositionnelle», 1997
3. Alasdair Urquhart, «La complexité de preuves propositionnelles ", 1995

Voir aussi ceux listés ici et ici .

$2n \times 2n$$2\times 1$

Michael Alekhnovich. Le problème de l'échiquier mutilé est exponentiellement difficile à résoudre. Informatique théorique 310 (1-3): 513-525 (2004). http://dx.doi.org/10.1016/S0304-3975(03)00395-5

$n\to (k)^2_2$$k=\lfloor \frac12 \log n \rfloor$$\bigvee_{i,j\in K} x_{i,j}$$\bigvee_{i,j\in K} \neg x_{i,j}$$K\subseteq \{ 1 , \ldots , n \}$$|K| = k$

Il y a une construction à la page 9 de ce document par Groote et Zantema .

DIMACS ne gère- t-il pas des jeux d'échantillons d'instances SAT matérielles? Je ne pouvais pas le trouver là avec juste un regard superficiel, mais si vous entrez "SAT" dans leur boîte de recherche, il affichera de nombreux hits, y compris plusieurs articles / discussions sur les instances SAT dures.