The Log-Support Encoding of CSP into SAT

It is known that Constraint Satisfaction Problems (CSP) can be converted into Boolean Satisfiability problems (SAT); however how to encode a CSP into a SAT problem such that a SAT solver will efficiently find a solution is still an open question. Various encodings have been proposed in the literature. Some of them use a logical variable for each element in each domain: among these very successful are the direct and the support encodings. It is known that a SAT solver based on the DPLL procedure obtains a propagation similar to Forward Checking on a directencoded CSP, and to Maintaining Arc-Consistency on a support-encoded CSP. Other methods, such as the log-encoding, are more compact, and use a logarithmic number of logical variables to encode domains. However, they lack the propagation power of the direct and support encodings, so many SAT solvers perform better on direct/support encodings than in the log-encoding, as witnessed by many works in the literature. In this paper, we prop...

• Type: Conference
• Year: 2007
• Where: CP
• Authors: Marco Gavanelli
• Keywords: CP 2007, Logical Variables, Programming Languages, SAT Solvers, Support Encodings