Quels problèmes SAT sont faciles?

Que sont les "régions faciles" pour la satisfiabilité? En d'autres termes, des conditions suffisantes pour qu'un solveur SAT puisse trouver une affectation satisfaisante, en supposant qu'elle existe.

Un exemple est lorsque chaque clause partage des variables avec quelques autres clauses, en raison d'une preuve constructive de LLL, d'autres résultats dans ce sens?

Il existe une littérature considérable sur les régions faciles pour la propagation de la croyance, y a-t-il quelque chose dans ce sens pour la satisfiabilité?

Je suppose que vous connaissez le résultat classique de Schaefer de STOC'78, mais juste au cas où.

10.1145 / 800133.804350

Schaefer a prouvé que si SAT est paramétré par un ensemble de relations autorisées dans n'importe quelle instance, alors il n'y a que 6 cas traitables: 2-SAT (c'est-à-dire que chaque clause est binaire), Horn-SAT, dual-Horn-SAT, affine-SAT ( solutions aux équations linéaires dans GF (2)), 0-valide (relations satisfaites par l'affectation tout-0) et 1-valide (relations satisfaites par l'affectation tout-1).

Je ne sais pas si c'est ce que vous recherchez, mais il existe une littérature importante sur la transition de phase 3-SAT.

Monasson, Zecchina, Kirkpatrcik, Selman et Troyansky avaient un document dans la nature qui parle de la transition de phase de k-SAT aléatoire. Ils ont utilisé une paramétrisation du rapport des clauses aux variables. Pour le 3-SAT aléatoire, ils ont trouvé numériquement que le point de transition est d'environ 4,3. Au-dessus de ce point, les instances aléatoires de 3-SAT sont trop contraintes et presque sûrement insatiables et en dessous de ce point, les problèmes sont sous-contraints et satisfaisables (avec une forte probabilité). Mertens, Mezard et Zecchina utilisent des procédures de méthode de cavité pour estimer le point de transition de phase avec un degré de précision plus élevé.

Loin du point critique, les algorithmes "stupides" fonctionnent bien pour des instances satisfaisables (marche assis, etc.). D'après ce que je comprends, les temps d'exécution du solveur déterministe croissent de façon exponentielle à ou près de la transition de phase (voir ici pour plus de discussion?).

Un proche cousin de la propagation des croyances, Braunstein, Mezard et Zecchina ont introduit la propagation de l'enquête qui résoudrait des instances 3-SAT satisfaisantes dans des millions de variables, même extrêmement proches de la transition de phase. Mezard a une conférence ici sur les verres de spin (dont il a utilisé la théorie dans l'analyse des transitions de phase NP-Complete aléatoires) et Maneva a une conférence ici sur la propagation de l'enquête.

De l'autre côté, il semble que nos meilleurs solveurs prennent un temps exponentiel pour prouver leur insatisfaction. Voir ici , ici et ici pour des preuves / discussion de la nature exponentielle de certaines méthodes courantes pour prouver l'insatisfaction (procédures Davis-Putnam et méthodes de résolution).

Il faut faire très attention aux affirmations de «facilité» ou de «dureté» pour les problèmes aléatoires NP-Complete. Le fait d'avoir un problème NP-Complete affichant une transition de phase ne donne aucune garantie quant à l'emplacement des problèmes difficiles ou à leur existence. Par exemple, le problème du cycle de Hamiltoniain sur les graphes aléatoires d'Erdos-Renyi est prouvé facilement, même au point de transition critique ou à proximité. Le problème de partition numérique ne semble pas avoir d'algorithmes qui le résolvent bien dans la plage de probabilité 1 ou 0, sans parler du seuil critique. D'après ce que je comprends, les problèmes aléatoires de 3-SAT ont des algorithmes qui fonctionnent bien pour des instances satisfaisables presque au niveau ou en dessous du seuil critique (propagation de l'enquête, marche assis, etc.) mais aucun algorithme efficace au-dessus du seuil critique pour prouver l'insatisfiance.

Il y a beaucoup de conditions suffisantes. Dans un certain sens, une grande partie de la CS théorique a été consacrée à la collecte de ces conditions - tractabilité à paramètres fixes, 2-SAT, 3-SAT aléatoires de différentes densités, etc.

il n'y a pas beaucoup de reconnaissance répandue de ce concept jusqu'à présent dans la littérature, mais le graphique de clause du problème SAT (le graphique avec un nœud par clause, et les nœuds sont connectés si les clauses partagent des variables), ainsi que d'autres graphiques connexes de la représentation SAT, semble avoir de nombreux indices de base sur la difficulté de l'instance en moyenne.

le graphe de la clause peut être analysé via toutes sortes d'algorithmes théoriques des graphes, est une mesure apparemment naturelle de la "structure" et avec des liens solides avec la mesure / estimation de la dureté, et il semble que la recherche sur cette structure et ses implications est encore très tôt. étapes. il n'est pas inconcevable que la recherche sur les points de transition, a / la manière traditionnelle et bien étudiée d'aborder cette question, puisse éventuellement être intégrée dans la structure graphique de cette clause (dans une certaine mesure, elle l'a déjà fait). en d'autres termes, le point de transition dans SAT peut être vu comme existant "à cause de" la structure du graphe de clause.

voici une excellente référence dans ce sens, une thèse de doctorat de Herwig, il y en a bien d'autres.

[1] Décomposition des problèmes de satisfiabilité ou Utilisation de graphiques pour mieux comprendre les problèmes de satisfiabilité , Herwig 2006 (83pp)

Il est facile de déplacer toutes les instances près du point de "transition" aussi loin que l'on veut du point de "transition". Le mouvement implique un effort temps / espace polynomial.

Si les instances éloignées du point de «transition» sont plus faciles à résoudre, alors celles proches du point de transition doivent être tout aussi faciles à résoudre. (Transformations polynomiales et tout.)

$\kappa$

il trouve une structure d' autosimilarité fractale apparente des instances dures par rapport au paramètre de contrainte de telle sorte qu'un solveur DP (LL) pendant la recherche tend à trouver des sous-problèmes avec la même contrainte critique, quelle que soit la variable choisie à côté de la branche. il y a une analyse plus approfondie de la structure fractale dans les instances SAT (comme la dimension de Hausdorff des formules SAT et la connexion à la dureté) dans par exemple [2,3]

une autre piste de recherche quelque peu interdépendante est la relation entre les petits graphes du monde et la structure SAT (dure), par exemple [4,5]

$\stackrel{?}{=}$

[1] Le tranchant du couteau de contrainte par Toby Walsh 1998

[2] SELF-SIMILARITÉ DES EXPRESSIONS BOOLÉENNES SATISFAISANTES DÉCIPHÉES EN TERMES DE SYSTÈMES DE FONCTION IÉRÉS DIRIGÉS GRAPHIQUES par Ni et Wen

[3] Visualisation de la structure interne des instances SAT (rapport préliminaire) Sinz

[4] Recherche dans un petit monde par Walsh 1999

[5] Modélisation de problèmes SAT plus réalistes par Slater 2002