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, 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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Ansótegui, C., Bonet, M. L., Levy, J., & Manyà, F. (2007). Mapping CSP into many-valued SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4501 LNCS, pp. 10–15). Springer Verlag. https://doi.org/10.1007/978-3-540-72788-0_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
