A Structure-Based Variable Ordering Heuristic for SAT

We propose a variable ordering heuristic for SAT, which is based on a structural analysis of the SAT problem. We show that when the heuristic is used by a Davis-Putnam SAT solver that employs conflict-directed backtracking, it produces a divide-and-conquer behavior in which the SAT problem is recursively decomposed into smaller problems that are solved independently. We discuss the implications of this divide-and-conquer behavior on our ability to provide structure-based guarantees on the complexity of Davis-Putnam SAT solvers. We also report on the integration of this heuristic with ZChaff— a state-of-the-art SAT solver—showing experimentally that it significantly improves performance on a range of benchmark problems that exhibit structure.

Authors

• Jinbo Huang NICTA and Australian National University
• Adnan Darwiche

Keywords

No keywords are indexed for this paper.