Énumérer toutes les solutions d'un problème SAT

11

Tous les solveurs #SAT que je connais, par exemple RelSat, C2D, ne renvoient que le nombre d'instances satisfaisables. Mais je veux connaître chacun de ces cas?

Existe-t-il un tel solveur #SAT ou comment dois-je modifier un solveur #SAT disponible pour ce faire?

Je vous remercie.

lo.logic sat software qsp
la source
7
Ceci est souvent appelé «solveur SAT toutes solutions», mais ne semble pas être disponible sur étagère. Les références que je peux trouver parlent de modifications apportées à MiniSAT et à d'autres solveurs, généralement en ajoutant des clauses de blocage pour exclure une solution lorsqu'elle est trouvée. D'un autre côté, la plupart des solveurs de contraintes prennent en charge la génération de toutes les solutions en standard.
András Salamon
une approche est une conversion CNF → DNF pour laquelle il y a beaucoup de littérature
vzn

Réponses:

13

Vous recherchez un solveur SAT ALL-SAT ou toutes solutions. C'est un problème différent de #SAT. Vous n'avez pas à énumérer toutes les solutions pour les compter.

Je ne connais pas d'outil qui résout votre problème car les gens ajoutent ces algorithmes au-dessus des solveurs SAT existants mais semblent rarement publier ces extensions. Deux articles qui devraient vous aider à modifier un solveur CDCL pour implémenter ALL-SAT sont ci-dessous.

Solveur SAT toutes solutions efficace en mémoire et son application à l'accessibilité , O. Grumberg, A. Schuster, A. Yadgar, FMCAD 2004

Voici un article récent publié sur l'arXiv.

Extension des solveurs SAT modernes pour énumérer tous les modèles , Said Jabbour, Lakhdar Sais, Yakoub Salhi, 2013

Vous pouvez essayer de contacter ces auteurs pour leur implémentation.

Vijay D
la source
Pour le deuxième article, il vous suffit de cliquer sur la première version v1 pour le voir.
Tayfun Payez le
Ce document récent semble lié: homes.cs.washington.edu/~sudeepa/UAI2013-ModelCounting.pdf
Kaveh
1
@Kaveh, je pense que l'OP demande un solveur ALLSAT ou un moyen de transformer un solveur #SAT en solveur ALLSAT. Ceci est un document sur les limites inférieures de #SAT. Je ne suis pas sûr que cela aide le PO.
Vijay D
2

J'ai trouvé un article plus récent (2014) sur All-SAT lors d'une conférence VLSI, donc il est définitivement orienté vers le côté pratique (ce qui semble en accord avec la question du PO ici, bien que moins avec cstheory.SE en général):

  • "All-SAT using Minimal Blocking Clauses" par Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. doi: 10.1109 / VLSID.2014.22 .

Pour ceux sans abonnement IEEE, il y a une copie gratuite sur la page Web de Subramanyan Princeton . (Il utilise un service de partage de fichiers pour stocker / distribuer des copies de ses documents et je ne suis pas sûr de la stabilité de ces URL, d'où ce lien rond-point.)

L'essentiel de cet article semble être:

Notre contribution, l'algorithme Non-Disjoint-Dec, génère des clauses de blocage extrêmement courtes qui ne contiennent aucune des variables implicites dans le solveur. Notez que généralement la majorité des variables dans un terme satisfaisant sont implicites. Les clauses de blocage courtes sont très bénéfiques pour les performances du solveur, comme le montre l'évaluation.

Leur implémentation s'appuie sur MiniSat. Le code source de leur extension ne semble cependant pas être accessible au public. Hélas, cela semble être une habitude dans le domaine de l'All-SAT, donc les articles dans ce domaine qui contiennent des résultats expérimentaux configurent simplement un algorithme plus ou moins simple de type homme de paille à battre et peuvent rarement être directement comparés (en termes d'expérimentation résultats) avec tout autre algorithme publié pour All-SAT. L'article de Jabbour et al. mentionné par Vijay D est également de ce type.

Comme je ne le vois pas mentionné dans l'autre réponse (mais seulement dans le commentaire d'András Salamon), la technique [plutôt populaire] des clauses de blocage a été introduite dans:

Pétiller
la source