ECAI-2002 Conference Paper

[full paper]

Arc Consistency in SAT

Ian P Gent

I introduce a new encoding of binary constraint satisfaction problems (CSPs) into boolean satisfiability (SAT). It is the first encoding which enables arc consistency in the original CSP to be established by unit propagation in the translated SAT instance. With the curent generation of highly effective SAT solvers, I show that the encoding can be used to solve hard instances of random binary CSPs. I also show that translation and solution in SAT is about an order of magnitude slower for the establishment of arc consitency in binary CSPs. Finally, I show experimentally that local search algorithms such as WalkSAT perform much better on the new encoding than on the standard encoding.

Keywords: Satisfiability Testing, Constraint Satisfaction, Search

Citation: Ian P Gent: Arc Consistency in SAT. In F. van Harmelen (ed.): ECAI2002, Proceedings of the 15th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2002, pp.121-125.