 |
HAL-LIRMM - Open Archive |  |
Conference papers
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.
https://hal-lirmm.ccsd.cnrs.fr/lirmm-00269776
Contributor : Christine Carvalho de Matos <>
Submitted on : Saturday, October 12, 2019 - 6:17:43 PM
Last modification on : Monday, January 11, 2021 - 5:24:09 PM
Long-term archiving on: : Monday, January 13, 2020 - 2:03:21 PM
Contributor : Christine Carvalho de Matos <>
Submitted on : Saturday, October 12, 2019 - 6:17:43 PM
Last modification on : Monday, January 11, 2021 - 5:24:09 PM
Long-term archiving on: : Monday, January 13, 2020 - 2:03:21 PM
File
sat03.pdf
Files produced by the author(s)