Skip to main content

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.

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