Skip to Main content Skip to Navigation
Conference papers

Local Consistencies in SAT

Christian Bessière 1 Emmanuel Hébrard 2 Toby Walsh 2
1 COCONUT - Agents, Apprentissage, Contraintes
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Christine Carvalho de Matos Connect in order to contact the contributor
Submitted on : Wednesday, September 18, 2019 - 10:50:42 AM
Last modification on : Monday, October 11, 2021 - 1:24:09 PM
Long-term archiving on: : Saturday, February 8, 2020 - 9:15:36 PM


Publisher files allowed on an open archive




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.299-314, ⟨10.1007/978-3-540-24605-3_23⟩. ⟨lirmm-00109164⟩



Record views


Files downloads