Livre de recettes pour les encodages SAT?

17

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?

Bordaigorl
la source
1. Cette question semble très utile, mais aussi potentiellement trop large. Je pense que ce serait une meilleure question si vous vous concentrez sur un seul domaine (oui, cela peut impliquer plusieurs questions, une par domaine - mais assurez-vous de faire des recherches avant de nous demander et de nous montrer ce que vous avez fait).
DW
2. De plus, quelles recherches avez-vous faites? Avez-vous examiné les frontaux SAT, tels que STP, Alloy et Minion? Avez-vous consulté cs.stackexchange.com/q/12087/755 , cs.stackexchange.com/q/13188/755 , cs.stackexchange.com/a/6522/755 , cs.stackexchange.com/a/12153/ 755 ? aux questions marquées sat-solveurs ou satisfiabilité ?
DW
Oui, la question peut être un peu large. @DW merci pour les liens dont certains sont directement pertinents. J'aurais dû mentionner que je ne suis pas intéressé par la résolution d'un problème particulier, ni par les méthodes générales pour des encodages plus efficaces; l'expression "meilleures pratiques" que j'ai utilisée est probablement trompeuse, je vais la modifier. Je suis intéressé par un livre de recettes =)
Bordaigorl
Concernant le domaine je dirais (hyper) graph théorie mais c'est probablement encore très large ...
Bordaigorl
Voir aussi la question connexe cs.stackexchange.com/q/12087
András Salamon

Réponses:

9

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é.

Kyle Jones
la source
4

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.

Juho
la source
3

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.

vzn
la source
C'est un très bon point. Mais même lorsque vous utilisez un solveur SMT, il existe une partie purement basée sur SAT de la recherche qui peut bénéficier de "recettes" réussies ...
Bordaigorl
il n'est pas tout à fait exact de dire qu'il s'agit d'une "partie purement SAT de la recherche", car (comme indiqué / à ma connaissance), il utilise la structure spéciale connue / construite des instances générées dans ses heuristiques qu'un solveur "vanille" ne ferait pas "reconnaître". en d'autres termes, il (c'est-à-dire la combinaison ) n'est pas "réductible / séparable" aux parties constituantes (c'est-à-dire codeur plus solveur) ou simplement à un autre système de codage normalisé.
vzn
Je vois. Je vais en savoir plus à ce sujet merci!
Bordaigorl
sûr. Notez également que la programmation des jeux de réponses est quelque peu similaire.
vzn