Etude des transformations liées à l'utilisation des solveurs SAT

13

Je commence à étudier la possibilité de compter sur un solveur SAT pour résoudre un problème d'optimisation qui m'intéresse, et je suis actuellement à la recherche d'une enquête qui présenterait des exemples de transformations "intelligentes" vers des variantes de SAT (c'est-à-dire des transformations qui en résultent dans un problème de taille raisonnable, car je ne suis pas intéressé à prouver les résultats de dureté mais à résoudre réellement le problème), approximativement dans l'esprit de ce qui peut être trouvé dans l'enquête sur les graphiques cubiques de Greenlaw et Petreschi , si une comparaison peut être fait entre les deux.

Un tel sondage m'a-t-il échappé parce qu'il n'existe pas ou parce que je l'ai raté?

ds.algorithms reference-request sat optimization Anthony Labarre
la source
Qu'entendez-vous exactement par "variantes de SAT"?
Giorgio Camerani
@Walter: Désolé si ce n'est pas le bon mot, je voulais dire des choses comme -SAT, Planar-SAT, NAE-SAT, et ainsi de suite ... mais je devrais probablement mettre ces deux mots entre parenthèses, car je ne le fais pas savoir si cela est important lors de l'utilisation de solveurs SAT. k
Anthony Labarre
4
Ne vous inquiétez pas, c'est le bon mot, j'aurais dû le comprendre. D'un point de vue purement pratique, cependant, je ne pense pas que cela soit important (ce qui importe le plus, c'est la parcimonie de votre encodage). Pourriez-vous fournir plus de détails sur le problème d'optimisation que vous essayez de résoudre? Je suis très intéressé par les applications pratiques de SAT et par les aspects techniques de la résolution de SAT.
Giorgio Camerani
Cela peut sembler un peu déroutant que vous parliez d'un problème d'optimisation mais en même temps de SAT. Généralement, pour une optimalité, vous avez besoin de quelque chose de plus solide, par exemple MAX-SAT. Vous pourriez peut-être clarifier cela.
Mikolas
cette question pourrait être quelque peu liée: cstheory.stackexchange.com/q/4314/4506
Mikolas

Réponses:

9

Je ne sais pas si c'est ce que vous cherchez, mais en voici un: JM Silva, Applications pratiques de la satisfaction booléenne .

Mikolas
la source
2
Je n'ai pas pu y accéder via votre lien, en voici un autre . À première vue, le document semble assez intéressant, mais plus axé sur les applications que ce que je recherche.
Anthony Labarre
@Anthony vous avez bien dit que vous étiez intéressé par l'aspect pratique :-) Quoi qu'il en soit, les solveurs traditionnels existants ne différencient pas vraiment les différents types de SAT. Par le passé, il y a eu des travaux sur l'exploitation des clauses binaires, par exemple. Mais les solveurs existants utilisent simplement l'apprentissage DPLL + unit prop + clause. Cependant, certains des préprocesseurs exploitent la structure. Mais encore une fois, pas vraiment du point de vue de la complexité th. classification.
Mikolas
8

Le chapitre 2 du Manuel de satisfaction examine les aspects à prendre en compte lors de la conception de ces transformations, ainsi qu'une liste de références qui répondent à ma question. Cela m'a aidé à trouver quelques exemples que l'on peut consulter pour se familiariser avec ces transformations:

Anthony Labarre
la source