Conversion de problèmes (mathématiques) en instances SAT

Ce que je veux faire, c'est transformer un problème mathématique que j'ai en un problème de satiabilité booléenne (SAT), puis le résoudre à l'aide d'un solveur SAT. Je me demande si quelqu'un connaît un manuel, un guide ou quelque chose qui m'aidera à convertir mon problème en une instance SAT.

Aussi, je veux résoudre ce problème en un temps meilleur que exponentiel. J'espère qu'un solveur SAT m'aidera.

Le chapitre 2 du manuel SAT (par Steven Prestwich) explique comment transformer en profondeur les problèmes de décision discrets en CNF. (Malheureusement, je ne pense pas qu'il existe une version provisoire en ligne - il est probablement préférable de consulter votre bibliothèque locale.) Plusieurs des autres références citées dans l'aperçu original de Magnus Björk Les techniques d'encodage SAT réussies sont également utiles.

Si vos problèmes sont continus ou si vous êtes particulièrement intéressé par les systèmes d'inégalités, d'autres types de solveurs sont plus susceptibles d'être utiles. Comme le souligne Kyle, les solveurs SMT (tels que Z3 , Yices ou OpenSMT ) peuvent être utiles, bien que les théories SMT aient tendance à se concentrer sur la vérification des logiciels, de sorte que les solveurs SMT prennent généralement en charge des éléments tels que les expressions impliquant des intervalles d'entiers , mais peut mal fonctionner avec des contraintes d'injectivité. Pour les problèmes qui s'expriment naturellement comme des systèmes d'inégalités, CPLEX est le seul à battre (il était disponible gratuitement pour une utilisation académique, et il pourrait l'être encore). Pour certains problèmes de décision combinatoire (comme trouveremballages de rectangles dans un carré ), les solveurs de contraintes tels que Minion surpassent les solveurs SAT et sont souvent plus faciles à utiliser.

À moins que vous ne traduisiez des problèmes mathématiques en instances SAT comme un exercice d'apprentissage, votre temps sera beaucoup plus fructueusement consacré à l'apprentissage des théories de la modulo de la satisfiabilité . SMT vous permettra d'exprimer des équations et d'autres contraintes beaucoup plus naturellement qu'en tant qu'instances SAT booléennes. Certains solveurs SMT prennent en charge les quantificateurs existentiels et universels, vous permettant d'aller au-delà du NP et d'exprimer les problèmes PSPACE.

En plus d'être plus expressifs, les solveurs SMT sont plus rapides. Pas P = NP plus rapide, mais plus efficace dans la mesure où un bon solveur SMT ne rejette pas les informations structurelles spécifiques à la théorie qui aident à guider le solveur à travers l'espace de recherche. Faire une réduction de Karp directement sur une instance SAT force le solveur SAT à réapprendre toute cette structure, souvent à un coût exponentiel. Par exemple, le fait que l'addition est commutative est perdu sur les solveurs SAT basés sur DPLL et sur la recherche locale; le solveur ne sait pas du tout qu'il traite des nombres! Pour éviter d'essayer toutes les permutations de x + y + z = 10, un solveur SAT a besoin d'un code de rupture de symétrie, qui nécessite une détection d'automorphisme de graphe. Les meilleurs algorithmes de reconnaissance d'automorphisme de graphes actuels nécessitent une exponentielle temporelle au nombre de sommets dans le pire des cas,

Deux outils qui convertissent les langages de haut niveau en SMT ou CNF.

CVC La syntaxe est proche de CAS.

CBMC Il convertit un programme C en CNF, permettant des assertions. Les assertions sont toujours vraies ou, si elles sont fausses, une entrée de contre-exemple est trouvée. CBMC déroule les boucles, donc certains programmes C ont une CNF / SMT exponentiellement grande.