The log-support encoding of CSP into SAT
M Gavanelli - Principles and Practice of Constraint Programming–CP …, 2007 - Springer
Principles and Practice of Constraint Programming–CP 2007: 13th International …, 2007•Springer
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 …
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 …
Abstract
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
以上显示的是最相近的搜索结果。 查看全部搜索结果