Livre de recettes pour les encodages SAT?

Les solveurs SAT sont de plus en plus efficaces dans la résolution de grandes instances et sont utilisés comme back-end dans divers contextes. Chaque fois que l'on veut les utiliser pour résoudre un problème dans un domaine spécifique, il / elle doit proposer un encodage ad hoc qui a non seulement le bon ensemble de solutions mais met également les contraintes (même redondantes) sous une forme qui aide l'heuristique des solveurs à trouver une solution plus rapidement.

Beaucoup de tels encodages me semblent très courants, par exemple: affirmer qu'un ensemble fini de nœuds est lié comme un arbre, ou comme un DAG, ou qu'une liste est triée ...

Existe-t-il un référentiel / livre de recettes d'encodages courants pour les problèmes courants avec des solutions optimisées?

Il y a quelques années, j'ai lu un document d'enquête qui semble pertinent, " Successful SAT Encoding Techniques " de Magnus Björk.

Abstrait:

Cet article identifie les bonnes pratiques pour les encodages SAT en analysant les entretiens avec un certain nombre d'experts SAT bien connus. Le but est à la fois de déterminer la confiance dans les différentes stratégies d'encodage en analysant s'il existe un consensus parmi les experts ou non, ainsi que de révéler des connaissances cachées aux utilisateurs SAT.

Il existe un consensus sur le fait que les techniques de codage ont généralement un impact dramatique sur l'efficacité du solveur SAT, qu'il faut souvent beaucoup de travail pour trouver un bon codage et que la taille d'une liaison n'est que très faiblement liée à la dureté de trouver une solution. . Les sujets sur lesquels les personnes interrogées ne sont pas d'accord comprennent la faisabilité d'inclure l'arithmétique dans les problèmes SAT et la nécessité de formuler les problèmes sous forme de clauses ou de circuits.

L'article décrit un certain nombre de stratégies qui sont bonnes dans différentes situations, telles que différentes manières de représenter des nombres et comment utiliser l'incrémentalité.

C'est toujours une bonne idée de consulter d'abord le Manuel de satisfaction [1] (je suppose qu'il n'est pas disponible gratuitement, désolé). Ici, le chapitre 2 est intitulé "Encodages CNF". À tout le moins, le livre fournit des références bibliographiques sur l'état de l'art au moment de la rédaction, et vous pouvez élargir votre recherche à travers elles.

De plus, voici et voici deux diapositives récentes sur le prétraitement SAT. Les diapositives donnent un aperçu concis des techniques de prétraitement, ainsi que d'autres références. L'idée est qu'au lieu d'essayer de modéliser "manuellement" le problème de manière efficace, vous le modélisez simplement de la manière la plus simple, appuyez sur OK, et un logiciel vous offre un encodage efficace.

[1] Biere, Armin, Marijn Heule et Hans van Maaren, éd. Manuel de satisfiabilité. Vol. 185. IOS Press, 2009.

pas exactement une réponse directe mais un autre angle de plus en plus étroitement lié: une partie de cela est couverte par un domaine de recherche relativement nouveau connu sous le nom de SMT, Satisfiability Modulo Theories . l'idée de base est de combiner des encodages de problèmes (par exemple, arithmétique entière, graphiques, etc.) dans le solveur SAT, mais également d'utiliser / tirer parti des connaissances supplémentaires qui découlent de ce couplage pour créer des algorithmes de solution plus avancés. voici une enquête. comme indiqué, ils peuvent être beaucoup plus efficaces que de combiner un mécanisme de codage ad hoc avec des solveurs SAT standard.

• Théories de Modulo de satisfaction: un apéritif / Leonardo de Moura et Nikolaj Bjørner

  Satisfibility Modulo Theories (SMT) consiste à vérifier la satisfiabilité des formules logiques sur une ou plusieurs théories. Le problème repose sur une combinaison de certains des domaines les plus fondamentaux de l'informatique. Il combine le problème de la satisfiabilité booléenne avec des domaines tels que ceux étudiés en optimisation convexe et en terme de manipulation de systèmes symboliques. Il s'appuie également sur les problèmes les plus prolifiques du siècle dernier de la logique symbolique: le problème de la décision, l'exhaustivité et l'incomplétude des théories logiques, et enfin la théorie de la complexité. Le problème de la combinaison modulaire d'algorithmes spéciaux pour chaque domaine est aussi profond et intrigant que la recherche de nouveaux algorithmes qui fonctionnent particulièrement bien dans le contexte d'une combinaison. SMT jouit également d'un rôle très utile en génie logiciel. Logiciel moderne, l'analyse matérielle et les outils basés sur des modèles sont des systèmes logiciels de plus en plus complexes et à multiples facettes. Cependant, leur noyau est invariablement un composant utilisant une logique symbolique pour décrire les états et les transformations entre eux. Un solveur SMT bien réglé qui prend en compte les avancées les plus récentes fait généralement évoluer les ordres de grandeur au-delà des solveurs ad-hoc personnalisés.