# Local Consistency and SAT-Solvers

arXiv: https://arxiv.org/abs/1401.4613 · HTML: https://mlsanity.com/paper/1401.4613/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Jan 2014.

## Built on by (most cited first, 1 of 1)

- [Modeling and Solving Graph Synthesis Problems Using SAT-Encoded Reachability Constraints in Picat](https://mlsanity.com/paper/2109.08293/) (2021)

## Abstract (arXiv)

Local consistency techniques such as k-consistency are a key component of specialised solvers for constraint satisfaction problems. In this paper we show that the power of using k-consistency techniques on a constraint satisfaction problem is precisely captured by using a particular inference rule, which we call negative-hyper-resolution, on the standard direct encoding of the problem into Boolean clauses. We also show that current clause-learning SAT-solvers will discover in expected polynomial time any inconsistency that can be deduced from a given set of clauses using negative-hyper-resolvents of a fixed size. 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 fixed 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 constraint problems which are challenging for conventional constraint-programming solvers.