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. © Springer-Verlag 2004.
CITATION STYLE
Bessière, C., Hebrard, E., & Walsh, T. (2004). Local consistencies in SAT. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2919, 299–314. https://doi.org/10.1007/978-3-540-24605-3_23
Mendeley helps you to discover research relevant for your work.