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.
CITATION STYLE
Lardeux, F., & Monfroy, E. (2014). From declarative set constraint models to “good” SAT instances. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8884, pp. 76–87). Springer Verlag. https://doi.org/10.1007/978-3-319-13770-4_8
Mendeley helps you to discover research relevant for your work.