Local Consistencies in SAT - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Conference Papers Year : 2004

Local Consistencies in SAT


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.
Fichier principal
Vignette du fichier
ark__67375_HCB-3GPW4NQV-Z.pdf (282.76 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive

Dates and versions

lirmm-00109164 , version 1 (18-09-2019)



Christian Bessiere, 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⟩
161 View
127 Download



Gmail Facebook X LinkedIn More