A compact and efficient SAT-encoding of finite domain CSP
International Conference on Theory and Applications of Satisfiability Testing, 2011•Springer
Abstract A (finite) Constraint Satisfaction Problem (CSP) is a combinatorial problem to find
an assignment which satisfies all given constraints over finite domains. A SAT-based CSP
solver is a program which solves a CSP by encoding it to SAT and searching solutions by
SAT solvers. Remarkable improvements in the efficiency of SAT solvers make SAT-based
CSP solvers applicable for solving hard and practical problems. A number of SAT encoding
methods have been therefore proposed: direct encoding, support encoding, log encoding …
an assignment which satisfies all given constraints over finite domains. A SAT-based CSP
solver is a program which solves a CSP by encoding it to SAT and searching solutions by
SAT solvers. Remarkable improvements in the efficiency of SAT solvers make SAT-based
CSP solvers applicable for solving hard and practical problems. A number of SAT encoding
methods have been therefore proposed: direct encoding, support encoding, log encoding …
Abstract
A (finite) Constraint Satisfaction Problem (CSP) is a combinatorial problem to find an assignment which satisfies all given constraints over finite domains. A SAT-based CSP solver is a program which solves a CSP by encoding it to SAT and searching solutions by SAT solvers. Remarkable improvements in the efficiency of SAT solvers make SAT-based CSP solvers applicable for solving hard and practical problems. A number of SAT encoding methods have been therefore proposed: direct encoding, support encoding, log encoding, log-support encoding, and order encoding.
Springer
以上显示的是最相近的搜索结果。 查看全部搜索结果