TítolMapping CSP into Many-Valued SAT
Publication TypeConference Paper
Year of Publication2007
AuthorsAnsótegui C, Bonet MLuisa, Levy J, Manyà F
Conference NameProc. of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT'07
Volume4501
EditorSpringer
Paginació10-15
Resum

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.