Abstract:

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.

• Tagged
• XML
• BibTex