Jinbo Huang and Adnan Darwiche|
Computer Science Department
University of California, Los Angeles
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.