Local consistency and SAT−solvers
Peter Jeavons and Justyna Petke
Abstract
In this paper we show that the power of using k-consistency techniques in a constraint problem is precisely captured by using a particular inference rule, which we call positive-hyper-resolution, on the direct Boolean encoding of the CSP instance. We also show that current clause-learning SAT-solvers will deduce any positive-hyper-resolvent of a fixed size from a given set of clauses in polynomial expected time. We combine these two results to show that, without being explicitly designed to do so, current clause-learning SAT-solvers efficiently simulate k-consistency techniques, for all values of k. We then give some experimental results to show that this feature allows clause-learning SAT-solvers to efficiently solve certain families of CSP instances which are challenging for conventional CP solvers.
Details
| Book Title |
Proceedings of the 16th International Conference on Principles and Practice of Constraint Programming − CP 2010 |
| Pages |
398−413 |
| Publisher |
Springer |
| Series |
Lecture Notes in Computer Science |
| Volume |
6308 |
| Year |
2010 |
Links
DOI (10.1007/978-3-642-15396-9_33)
Related pages
|
People |
|
|
Activities |