|Título||Mapping CSP into Many-Valued SAT|
|Publication Type||Conference Paper|
|Year of Publication||2007|
|Authors||Ansótegui C, Bonet MLuisa, Levy J, Manyà F|
|Conference Name||Proc. of the 10th International Conference on Theory and Applications of Satisfiability Testing, SAT'07|
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.
- Acerca del IIIA