Journal Article.:
Samuel R. Buss, Jan Hoffmann, and Jan Johannsen.
"Resolution Trees with Lemmas - Resolution Refinements that Characterize DLL-Algorithms with Clause Learning "
In Logical Methods in Computer Science, 2008, vol 4, 4:13.
doi:10.2168/LMCS-4(4:13)2008.
Download paper: PDF.
Abstract: Resolution refinements called w-resolution trees with
lemmas (WRTL) and with input lemmas (WRTI) are introduced.
Dag-like resolution is equivalent to both WRTL and WRTI when there
is no regularity condition. For regular proofs, an exponential
separation between regular dag-like resolution and both regular WRTL
and regular WRTI is given.
It is proved that DLL proof search algorithms that use clause
learning based on unit propagation can be polynomially simulated by
regular WRTI. More generally, non-greedy DLL algorithms with
learning by unit propagation are equivalent to regular WRTI. A
general form of clause learning, called DLL-Learn, is defined that
is equivalent to regular WRTL.
A variable extension method is used to give simulations of
resolution by regular WRTI, using a simplified form of proof trace
extensions. DLL-Learn and non-greedy DLL algorithms with learning
by unit propagation can use variable extensions to simulate general
resolution without doing restarts.
Finally, an exponential lower bound for WRTL where the lemmas are
restricted to short clauses is shown.
Back to Sam Buss's publications page.