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

Local Consistencies in SAT

Emmanuel Hébrard
Toby Walsh
  • Function : Author
  • PersonId : 1055916


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
sat03.pdf (2.12 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

lirmm-00269776 , version 1 (12-10-2019)


  • HAL Id : lirmm-00269776 , version 1


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.400-407. ⟨lirmm-00269776⟩
146 View
8 Download


Gmail Facebook X LinkedIn More