Dtree-SAT is an implementation of a

*variable group ordering* heuristic for Propositional Satisfiability (SAT), proposed in

[IJCAI03:HD], which exploits the structure of CNF formulas via their

*decomposition trees* (dtrees). zChaff is used as the underlying SAT solver.