Boosting Chaff's performance by incorporating CSP heuristics

Abstract

Identifying CSP variables in SAT encodings of combinatorial problems allows one to incorporate CSP-like variable selection heuristics into SAT solvers. We show that such heuristics turn out to be more powerful than the best performing state-of-the-art variable selection heuristics for SAT. In particular, we define five novel CSP-like variable selection heuristics for Chaff - one of the most modern, powerful and robust SAT solvers - and provide experimental evidence that Chaff augmented with those heuristics outperforms the original Chaff solver one order of magnitude on difficult SAT-encoded problems like random binary CSPs, pigeon hole, and graph coloring. © Springer-Verlag 2003.