Various encodings have been proposed to convert Constraint Satisfaction Problems (CSP) into Boolean Satisfiability problems (SAT). Some of them use a logical variable for each element in each domain: among these very successful are the direct and the support encodings. Other methods, such as the log-encoding, 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 poorly on log-encoded CSPs. In this paper, we propose a new encoding, called log-support, that combines the log and support encodings. It has a logarithmic number of variables, and uses support clauses to improve propagation. We also extend the encoding using a Gray code. We provide experimental results on Job-Shop scheduling and randomly-generated problems. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Gavanelli, M. (2007). The log-support encoding of CSP into SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4741 LNCS, pp. 815–822). Springer Verlag. https://doi.org/10.1007/978-3-540-74970-7_59
Mendeley helps you to discover research relevant for your work.