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

Cited literature [17 references]  Display  Hide  Download

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00109164
Contributor : Christine Carvalho de Matos <>
Submitted on : Wednesday, September 18, 2019 - 10:50:42 AM
Last modification on : Monday, June 15, 2020 - 1:38:03 PM
Document(s) archivé(s) le : Saturday, February 8, 2020 - 9:15:36 PM

File

ark__67375_HCB-3GPW4NQV-Z.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

257

Files downloads

63