[PDF][PDF] System description of a SAT-based CSP solver Sugar
Proceedings of the Third International CSP Solver Competition, 2008•cril.univ-artois.fr
This paper gives the system description of a SAT-based CSP solver Sugar submitted to the
Third International CSP Solver Competition. The Sugar solver solves a finite linear CSP and
MAX-CSP by translating it into a SAT problem using the order encoding method and then
solving the translated SAT problem with an external SAT solver (eg MiniSat). In the order
encoding method, a comparison x≤ a is encoded by a different Boolean variable for each
integer variable x and integer value a.
Third International CSP Solver Competition. The Sugar solver solves a finite linear CSP and
MAX-CSP by translating it into a SAT problem using the order encoding method and then
solving the translated SAT problem with an external SAT solver (eg MiniSat). In the order
encoding method, a comparison x≤ a is encoded by a different Boolean variable for each
integer variable x and integer value a.
Abstract
This paper gives the system description of a SAT-based CSP solver Sugar submitted to the Third International CSP Solver Competition. The Sugar solver solves a finite linear CSP and MAX-CSP by translating it into a SAT problem using the order encoding method and then solving the translated SAT problem with an external SAT solver (eg MiniSat). In the order encoding method, a comparison x≤ a is encoded by a different Boolean variable for each integer variable x and integer value a.
cril.univ-artois.fr
以上显示的是最相近的搜索结果。 查看全部搜索结果