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.
展开▼
