Alexander Nadel

We present a new decision heuristic for DPLL-based propositional SAT
solvers.  Its essence is that both the initial and the conflict clauses
are arranged in a list and the next decision variable is chosen from the
top-most unsatisfied clause.  Various methods of initially organizing
the list and moving the clauses within it are studied.  Our approach is
an extension of one used in Berkmin, and adopted by other modern
solvers, according to which only conflict clauses are organized in a
list, and a literal-scoring-based secondary heuristic is used when there
are no more unsatisfied conflict clauses.  Our approach, implemented in
the 2004 version of zChaff solver and in a generic Chaff-based SAT
solver, results in a significant performance boost on hard industrial
benchmarks. This is a joint work with Nachum Dershowitz and Ziyad Hanna.