From Declarative Set Constraint Models to “Good” SAT Instances

TitreFrom Declarative Set Constraint Models to “Good” SAT Instances
Type de publicationCommunication
TypeCommunication avec actes dans un congrès
Année2014
LangueAnglais
Titre du colloqueArtificial Intelligence and Symbolic Computation
Titre des actes ou de la revueLecture Notes in Computer Science
Volume8884
Auteur secondaireAranda-Corral, Gonzalo A, Calmet, Jacques, Martín-Mateos, Francisco J
AuteurLardeux, Frédéric , Monfroy, Eric
ISBN978-3-319-13769-8
Résumé en anglais

On the one hand, Constraint Satisfaction Problems allow one to declaratively model problems. On the other hand, propositional satisfiability problem (SAT) solvers can handle huge SAT instances. We thus present a technique to declaratively model set constraint problems, to reduce them, and to encode them into ”good” SAT instances. We illustrate our technique on the well-known nqueens problem. Our technique is simpler, more expressive, and less error-prone than direct hand modeling. The SAT instances that we automatically generate are rather small w.r.t. hand-written instances.

URL de la noticehttp://okina.univ-angers.fr/publications/ua8015
DOI10.1007/978-3-319-13770-4_8