Existe-t-il un algorithme parfois efficace pour résoudre #SAT?

Soit une formule booléenne composée des opérateurs ET, OU et NON habituels et de certaines variables. Je voudrais compter le nombre de missions satisfaisant pour . Autrement dit, je veux trouver le nombre d'affectations différentes de valeurs de vérité aux variables de pour lesquelles suppose une valeur vraie. Par exemple, la formule a trois affectations satisfaisantes; a quatre. C'est le problème #SAT . $B$ $B$ $B$ $B$ $a\lor b$ $(a\lor b)\land(c\lor\lnot b)$

De toute évidence, une solution efficace à ce problème impliquerait une solution efficace à SAT, ce qui est peu probable, et en fait ce problème est # P-complet, et peut donc être strictement plus difficile que SAT. Je ne m'attends donc pas à une solution efficace et garantie.

Mais il est bien connu qu'il y a relativement peu d'instances vraiment difficiles de SAT lui-même. (Voir par exemple Cheeseman 1991, "Où sont les problèmes vraiment difficiles" .) La recherche élaguée ordinaire, bien qu'exponentielle dans le pire des cas, peut résoudre efficacement de nombreux cas; les méthodes de résolution, bien qu'exponentielles dans le pire des cas, sont encore plus efficaces en pratique.

Ma question est:

Existe-t-il des algorithmes connus qui peuvent compter rapidement le nombre d'assignations satisfaisantes d'une formule booléenne typique, même si ces algorithmes nécessitent un temps exponentiel dans l'instance générale? Y a-t-il quelque chose de nettement mieux que d'énumérer toutes les affectations possibles?

complexity-theory reference-request satisfiability Mark Dominus
la source

J'ai essayé d'ajouter une balise pour # p-exhausteness, mais le logiciel Stack Exchange n'aime pas le signe #.

Mark Dominus

Je serais prudent en affirmant qu '"il y a relativement peu d'exemples vraiment difficiles de SAT lui-même". Je crois que l'article que vous liez parle en fait de -SAT aléatoire . De plus, le phénomène de transition de phase ne s'applique qu'aux cas aléatoires. Il existe de nombreux exemples de SAT fabriqués à la main, industriels, etc., très difficiles.

k

$k$

Juho

Merci. Pensez-vous que cela tend à rendre ma question moins claire? Comprenez-vous ce que je demande?

Mark Dominus

C'est clair pour moi. Il est seulement important de se rappeler quelles instances présentent la transition de phase :)

Juho

Réponses:

Compter dans le cas général

Le problème qui vous intéresse est appelé #SAT, ou comptage de modèles. Dans un sens, c'est le problème classique # P-complet. Le comptage des modèles est difficile, même pour -SAT! Sans surprise, les méthodes exactes ne peuvent gérer que des instances contenant des centaines de variables. Des méthodes approximatives existent également, et elles pourraient être capables de gérer des instances avec environ 1000 variables. $2$

Les méthodes de comptage exactes sont souvent basées sur une recherche exhaustive de style DPLL ou une sorte de compilation des connaissances. Les méthodes approximatives sont généralement classées comme des méthodes qui donnent des estimations rapides sans aucune garantie et des méthodes qui fournissent des limites inférieures ou supérieures avec une garantie d'exactitude. Il existe également d'autres méthodes qui peuvent ne pas correspondre aux catégories, telles que la découverte de portes dérobées, ou des méthodes qui insistent sur certaines propriétés structurelles pour conserver les formules (ou leur graphique de contraintes).

Il existe des implémentations pratiques. Certains compteurs de modèles exacts sont CDP, Relsat, Cachet, sharpSAT et c2d. Les types de techniques principales utilisées par les solveurs exacts sont les comptages partiels, l'analyse des composants (du graphe de contraintes sous-jacentes), la mise en cache des formules et des composants et le raisonnement intelligent à chaque nœud. Une autre méthode basée sur la compilation des connaissances convertit la formule CNF d'entrée en une autre forme logique. De cette forme, le nombre de modèles peut être déduit facilement (temps polynomial dans la taille de la formule nouvellement produite). Par exemple, on pourrait convertir la formule en un diagramme de décision binaire (BDD). On pourrait alors traverser le BDD de la feuille "1" jusqu'à la racine. Ou pour un autre exemple, le c2d utilise un compilateur qui transforme les formules CNF en forme normale de négation décomposable déterministe (d-DNNF).

Si vos instances deviennent plus grandes ou si vous ne vous souciez pas d'être exact, des méthodes approximatives existent également. Avec des méthodes approximatives, nous nous soucions de la qualité de l'estimation et de la fiabilité de l'exactitude associée à l'estimation rapportée par notre algorithme. Une approche de Wei et Selman [2] utilise l'échantillonnage MCMC pour calculer une approximation du nombre réel de modèles pour la formule d'entrée. La méthode est basée sur le fait que si l'on peut échantillonner (presque) uniformément à partir de l'ensemble de solution d'une formule , alors on peut calculer une bonne estimation du nombre de solutions de . $\phi$ $\phi$

Gogate et Dechter [3] utilisent une technique de comptage de modèles connue sous le nom de SampleMinisat. Il est basé sur l'échantillonnage à partir de l'espace de recherche sans retour arrière d'une formule booléenne. La technique s'appuie sur l'idée d'un rééchantillonnage important, en utilisant des solveurs SAT basés sur DPLL pour construire l'espace de recherche sans retour en arrière. Cela peut être fait complètement ou jusqu'à une approximation. Un échantillonnage pour les estimations avec garanties est également possible. En s'appuyant sur [2], Gomes et al. [4] ont montré qu'en utilisant l'échantillonnage avec une stratégie randomisée modifiée, on peut obtenir des limites inférieures prouvables sur le nombre total de modèles avec des garanties d'exactitude probabiliste élevées.

Il existe également des travaux qui s'appuient sur la propagation des croyances (BP). Voir Kroc et al. [5] et le BPCount qu'ils introduisent. Dans le même article, les auteurs donnent une deuxième méthode appelée MiniCount, pour fournir des limites supérieures sur le nombre de modèles. Il existe également un cadre statistique qui permet de calculer les limites supérieures sous certaines hypothèses statistiques.

Algorithmes pour # 2-SAT et # 3-SAT

Si vous limitez votre attention à # 2-SAT ou # 3-SAT, il existe des algorithmes qui s'exécutent en et pour ces problèmes respectivement [1]. Il y a de légères améliorations pour ces algorithmes. Par exemple, Kutzkov [6] a amélioré la limite supérieure de [1] pour # 3-SAT avec un algorithme fonctionnant dans le temps . $O(1.3247^n)$ $O(1.6894^n)$ $O(1.6423^n)$

Comme dans la nature du problème, si vous voulez résoudre des instances en pratique, cela dépend beaucoup de la taille et de la structure de vos instances. Plus vous en savez, plus vous êtes capable de choisir la bonne méthode.

[1] Vilhelm Dahllöf, Peter Jonsson et Magnus Wahlström. Compter les affectations satisfaisantes en 2-SAT et 3-SAT. Dans les actes de la 8e conférence internationale annuelle sur l'informatique et la combinatoire (COCOON-2002), 535-543, 2002.

[2] W. Wei et B. Selman. Une nouvelle approche du comptage de modèles. In Proceedings of SAT05: 8th International Conference on Theory and Applications of Satisfiability Testing, volume 3569 of Lecture Notes in Computer Science, 324-339, 2005.

[3] R. Gogate et R. Dechter. Comptage approximatif en échantillonnant l'espace de recherche sans retour en arrière. In Proceedings of AAAI-07: 22nd National Conference on Artificial Intelligence, 198–203, Vancouver, 2007.

[4] CP Gomes, J. Hoffmann, A. Sabharwal et B. Selman. De l'échantillonnage au comptage de modèles. In Proceedings of IJCAI-07: 20th International Joint Conference on Artificial Intelligence, 2293–2299, 2007.

[5] L. Kroc, A. Sabharwal et B. Selman. Tirer parti de la propagation des croyances, de la recherche de retour en arrière et des statistiques pour le comptage de modèles. Dans CPAIOR-08: 5e Conférence internationale sur l'intégration des techniques de l'IA et de la RO dans la programmation par contraintes, volume 5015 des notes de cours en informatique, 127–141, 2008.

[6] K. Kutzkov. Nouvelle limite supérieure pour le problème # 3-SAT. Lettres de traitement de l'information 105 (1), 1-5, 2007.

Juho
la source

En plus des articles répertoriés par Juho, voici quelques autres qui décrivent les travaux sur ce sujet, en particulier sur l'approximation du nombre de solutions:

Comptage de modèles . Carla P. Gomes, Ashish Sabharwal, Bart Selman Handbook of Satisfiability, IOS Press. Rédacteurs: Armin Biere, Marijn Heule, Hans van Maaren et Toby Walsh. Chapitre 20, pp 633-654, 2009.
- Cela a un bon aperçu du sujet et une introduction à un certain nombre de techniques.
Échantillonnage quasi uniforme des espaces combinatoires à l'aide de contraintes XOR . Carla P. Gomes, Ashish Sabharwal, Bart Selman. NIPS-06. 20e conférence annuelle sur les systèmes de traitement de l'information neuronale, pp 481-488, Vancouver, BC, Canada, décembre 2006.
XOR courts pour le comptage de modèles: de la théorie à la pratique . Carla P. Gomes, Joerg Hoffmann, Ashish Sabharwal, Bart Selman SAT-07. 10e Conférence internationale sur la théorie et les applications des tests de satisfaction, LNCS volume 4501, pp 100-106, Lisbonne, Portugal, mai 2007.
Tirer parti de la propagation des croyances, de la recherche de retour en arrière et des statistiques pour le comptage de modèles . Lukas Kroc, Ashish Sabharwal, Bart Selman ANOR-2011. Annals of Operations Research, volume 184, numéro 1, pp 209-231, 2011.
Heuristique pour le comptage rapide de modèles exacts . Tian Sang, Paul Beame et Henry Kautz. Théorie et applications des tests de satisfaction (SAT 2005), pp 226-240.

DW
la source