Téléchargement de #SAT Solver

21

Quelqu'un pourrait-il indiquer un ou plusieurs sites Web où il est possible de télécharger une implémentation fonctionnelle d'un solveur #SAT? Je suis intéressé par ceux qui renvoient le nombre exact de solutions, pas une approximation.

ds.algorithms sat software Giorgio Camerani
la source
2
Salut Walter, votre question est proche de la frontière de ce qui serait officiellement "sur le sujet" pour ce site. Cependant, si vous n'avez nulle part ailleurs pour poser cette question et que nous pouvons y répondre, ce n'est peut-être pas si mal ... (Étant donné que le site est encore en cours de développement, je pense que nous sommes plus ouverts que d'autres sites.) Rassurez-vous que le but de ce commentaire n'est pas de "gronder" ou "d'avertir", c'est juste un avis amical.
Ryan Williams
Salut Ryan, merci pour ton avis. Je suis désolé si cette question est proche de la frontière. J'ai cherché sur le web et je n'ai rien trouvé: seulement quelques solveurs SAT, mais pas de solveurs #SAT. C'est pourquoi j'ai demandé ici. Bien sûr, je sais que je peux écrire mon propre code qui utilise un solveur SAT comme moteur pour compter les solutions, mais je cherchais quelque chose de déjà fait et prêt à l'emploi.
Giorgio Camerani,
12
Je ne suis pas d'accord. Je pense que de telles questions sont à la portée et devraient l'être!
Suresh Venkat
convenir de sa portée. fyi / imho ce n'est pas trop pratique pour construire un solveur #SAT à partir d'un solveur SAT à moins que l'on ait le code source et même dans ce cas, pas si pratique, sauf pour les très petites formules, à cause d'une très mauvaise explosion exponentielle. généralement des techniques spéciales propres à #SAT et non à SAT seraient nécessaires ...
vzn

Réponses:

16

Vous pouvez le faire avec SAT4J , simplement en itérant sur tous les modèles: http://www.sat4j.org/howto.php#models . J'imagine que la plupart des solveurs SAT ont cette capacité.

Dave Clarke
la source
Salut supercooldave, merci pour votre pointeur. Je ne savais pas que SAT4J avait cette capacité.
Giorgio Camerani,
16

Vous pouvez également essayer le solveur #SAT "sharpSAT" ( site Web , github ) pour compter le nombre d'affectations satisfaisantes des formules CNF.

Holger
la source
11

Une option consiste à utiliser une bibliothèque BDD, telle que JavaBDD . Toutes ces bibliothèques ont une fonction qui compte rapidement les solutions ou, au moins, elles facilitent l'écriture d'une telle fonction. L'inconvénient, cependant, est que la construction du BDD sera lente dans de nombreux cas et peut nécessiter beaucoup de mémoire.

mnO(mn)∼m+n

Radu GRIGore
la source
7

Rubrique connexe: Meilleur solveur SAT .

MS Dousti
la source
1
Merci Sadeq. Le sujet que vous avez indiqué semble être théorique. Il répertorie plusieurs articles sur la diminution de la limite supérieure. C'est très intéressant, mais je cherchais une implémentation fonctionnelle prête à l'emploi.
Giorgio Camerani
2
De rien. Parmi les liens cités ici, il y en avait un qui était purement pratique: satcompetition.org . Je pense que vous pouvez y trouver de très bonnes implémentations.
MS Dousti
7

Le meilleur que j'ai trouvé est "compilateur c2d". http://reasoning.cs.ucla.edu/c2d/

Il utilise d-DNNF et vous avez besoin de l' option -count .

Leon Leon
la source
c2d résout beaucoup plus de CNF que sharpsat. À des fins de jouets , le solveur sat "relsat" fera aussi l'affaire.
Leon Leon
7

Le solveur MBound présenté ici http://www.cs.cornell.edu/~sabhar/ peut donner des décomptes de modèles avec des garanties probabilistes. C'est beaucoup plus rapide que d'énumérer toutes les solutions.

Opter
la source
5

J'ai écrit un petit énumérateur implicant modèle / principal . Cela peut déjà être utilisé pour le comptage de modèles avec l'énumération du modèle, mais ce n'est pas très pratique. Si quelqu'un est intéressé, je peux l'étendre pour qu'il compte les modèles des principaux implicants.

Mikolas
la source
2

Le site Web BeyondNP contient un bon inventaire des outils existants pour résoudre #SAT (et d'autres problèmes difficiles liés aux formules CNF). Vous pouvez également trouver une liste d'outils pour le comptage approximatif de modèles et la compilation de connaissances (la tâche de transformer le CNF en une structure de données succincte qui, souvent, prend en charge le comptage de modèles temporels polynomiaux).

Vous pouvez également trouver une liste d'outils pour le prétraitement des formules CNF qui peuvent être utiles pour améliorer les performances des compteurs de modèles et divers benchmarks .

loup
la source