Representative Encodings to Translate Finite CSPs into SAT

Pedro Manuel Corrêa Calvente de Barahona, Steffen Hölldobler, Nguyen Van-Hau

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding. Compared to the sparse and order encodings, two widely used and efficient encodings, these representative encodings require a smaller number of variables and longer clauses to express complex CSP constraints. The paper shows that, concerning unit propagation, these encodings are incomparable. Nevertheless, the preliminary experimental results show that the new representative encodings are clearly competitive with the original sparse and order encodings, but further studies are needed to better understand the trading between fewer variables and longer clauses of the representative encodings.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science
PublisherAssociation for Computing Machinery (ACM)
Pages251-267
Volume8451
ISBN (Electronic)978-3-319-07046-9
ISBN (Print)978-3-319-07045-2
DOIs
Publication statusPublished - Jan 2014
EventCPAIOR 2014 - 11th International Conference on Integration of AI and OR Techniques in Constraint Programming -
Duration: 1 Jan 2014 → …

Conference

ConferenceCPAIOR 2014 - 11th International Conference on Integration of AI and OR Techniques in Constraint Programming
Period1/01/14 → …

Fingerprint Dive into the research topics of 'Representative Encodings to Translate Finite CSPs into SAT'. Together they form a unique fingerprint.

  • Cite this

    Barahona, P. M. C. C. D., Hölldobler, S., & Van-Hau, N. (2014). Representative Encodings to Translate Finite CSPs into SAT. In Lecture Notes in Computer Science (Vol. 8451, pp. 251-267). Association for Computing Machinery (ACM). https://doi.org/10.1007/978-3-319-07046-9_18