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

Local Consistencies in SAT

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.
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
Loading...

Dates and versions

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

Identifiers

Cite

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⟩
169 View
142 Download

Altmetric

Share

More