Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT

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

8 Citations (Scopus)

Abstract

Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that can not only be efficiently generated, but also efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, namely a previously proposed log-direct encoding, as well as a new combination, the log-order encoding. Experiments conducted on different domain problems with these hierarchical encodings demonstrate their significant promise in practice ... the log-direct encoding significantly outperforms the direct encoding (typically by one or two orders of magnitude) ... the log-order encoding is clearly competitive with the order encoding although more studies are required to clearly understand the tradeoff between the fewer variables and longer clauses in the former when expressing complex CSP constraints.
Original languageUnknown
Title of host publicationInternational Conference on Tools with Artificial Intelligence
Pages1028-1035
DOIs
Publication statusPublished - 1 Jan 2013
EventICTAI - IEEE 25th International Conference on Tools with Artificial Intelligence -
Duration: 1 Jan 2013 → …

Conference

ConferenceICTAI - IEEE 25th International Conference on Tools with Artificial Intelligence
Period1/01/13 → …

Cite this