Downloads for A Structure-Based Variable Ordering Heuristic for SAT

Jinbo Huang and Adnan Darwiche
Computer Science Department
University of California, Los Angeles
jinbo,darwiche@cs.ucla.edu

Abstract. 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 DPLL 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 DPLL 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.

A copy of the paper (in IJCAI-03) can be downloaded in pdf or ps.

The original zChaff source code and executable are available from zChaff at Princeton University.

Linux and Solaris executables of dtree-SAT are available for download. To obtain and compile the source code, click here.

Running the program without any option (i.e., dtree_sat cnf_file) corresponds to what is described in the paper (i.e., dtrees generated by hypergraph partitioning with two trials and two trial partitions per cut).

We have experimented with alternative dtree generation methods. In particular, dtrees generated by variable elimination sometimes lead to further reduction of dtree-SAT's running time. This option is available by running "dtree_sat cnf_file f". Run "dtree_sat" without arguments to see the full list of options supported.