Local consistency and SAT−solvers

Conference item

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.

Authors: Jeavons, P; Petke, J

• Publisher: Springer
• Host title: Proceedings of the 16th International Conference on Principles and Practice of Constraint Programming − CP 2010
• Volume: 6308
• Publication date: 2010-01-01
• DOI: 10.1007/978-3-642-15396-9_33