A Compact and Efficient SAT-Encoding of Finite Domain CSP
Description
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.
Journal
-
- Lecture Notes in Computer Science
-
Lecture Notes in Computer Science 375-376, 2011
Springer Berlin Heidelberg
- Tweet
Details 詳細情報について
-
- CRID
- 1360004230675217280
-
- ISSN
- 16113349
- 03029743
-
- Data Source
-
- Crossref
- KAKEN
- OpenAIRE