Publication Type: Conference Paper
Source: Lecture Notes in Computer Science, Springer, Volume 4501, p.10-15 (2007)
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 enforces (i,j)-consistency when applied to a many-valued SAT encoding of a CSP. Third, we define a number of derived rules of our many-valued resolution rule and show that they enforce well-known local consistency properties such as arc consistency and path consistency. As a result we define a logical framework for studying and analysing CSP inference, which could provide a better understanding of CSP inference to the SAT community, as well as insights into the relationship among SAT, many-valued SAT and CSP.