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 metadatas
Contributor : Christine Carvalho de Matos <>
Submitted on : Saturday, October 12, 2019 - 6:17:43 PM
Last modification on : Monday, June 15, 2020 - 1:38:03 PM
Long-term archiving on: : Monday, January 13, 2020 - 2:03:21 PM


Files produced by the author(s)


  • HAL Id : lirmm-00269776, version 1



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⟩



Record views


Files downloads