Abstract : We introduce some new mappings of constraint satisfaction problems into propositional satisfiability. These encodings generalize most of the existing encodings. Unit propagation on those encodings is the same as establishing relational k-arc consistency on the original problem. They can also be used to establish (i,j)-consistency on binary constraints. Experiments show that these encodings are an effective method for enforcing such consistencies, that can lead to a reduction in runtimes at the phase transition in most cases. Compared to the more traditional (direct) encoding, the search tree can be greatly pruned.
https://hal-lirmm.ccsd.cnrs.fr/lirmm-00269776
Contributor : Christine Carvalho de Matos <>
Submitted on : Saturday, October 12, 2019 - 6:17:43 PM Last modification on : Monday, January 11, 2021 - 5:24:09 PM Long-term archiving on: : Monday, January 13, 2020 - 2:03:21 PM
Christian Bessière, Emmanuel Hébrard, Toby Walsh. Local Consistencies in SAT. SAT: Theory and Applications of Satisfiability Testing, May 2003, Santa Margherita Ligure, Italy. pp.400-407. ⟨lirmm-00269776⟩