A structure-based variable ordering heuristic for SAT
Jinbo Huang, Adnan Y. Darwiche · 2003
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. 1