SAT Encodings of Finite-CSP Domains
Van-Hau Nguyen · 2017
Many real-world applications can be expressed as constraint satisfaction problems (CSPs), although hardly any problems are originally given by SAT formulas. Nevertheless, to benefit from powerful SAT solvers, many SAT encodings of CSPs have been studied recently. Such encodings should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this survey we present a novel approach on how to encode a finite-CSP domains into a SAT instance in a comprehensive and precise way. The paper also provides a informative comparison among SAT encodings in term of the number of variables and clauses required, and the strength of consistency achieved by unit propagation.