Mapping CSP into Many-Valued SAT

We first define a mapping from CSP to many-valued SAT which allows to solve CSP instances with many-valued SAT solvers. Second, we define a new many-valued resolution rule and prove that it is refutation complete for many-valued CNF formulas and, moreover, enforces CSP (i, j)-consistency when applied to a many-valued SAT encoding of a CSP. Instances of our rule enforce well-known local consistency properties such as arc consistency and path consistency.

• Type: Conference
• Year: 2007
• Where: SAT
• Authors: Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, Felip Manyà
• Keywords: Many-valued Resolution Rule, Many-valued Sat, Many-valued Sat Solvers, SAT 2007