Local Consistency and SAT-Solvers

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

• Type: Journal
• Year: 2010
• Where: CP
• Authors: Justyna Petke, Peter Jeavons
• Keywords: Artificial Intelligence, CP 2010, Csp Instances, K-consistency Techniques, Particular Inference Rule