Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning

Resolution refinements called w-resolution trees with lemmas (WRTL) and withinput lemmas (WRTI) are introduced. Dag-like resolution is equivalent to bothWRTL and WRTI when there is no regularity condition. For regular proofs, anexponential separation between regular dag-like resolution and both regularWRTL and regular WRTI is given. It is proved that DLL proof search algorithms that use clause learning basedon unit propagation can be polynomially simulated by regular WRTI. Moregenerally, non-greedy DLL algorithms with learning by unit propagation areequivalent to regular WRTI. A general form of clause learning, calledDLL-Learn, is defined that is equivalent to regular WRTL. A variable extension method is used to give simulations of resolution byregular WRTI, using a simplified form of proof trace extensions. DLL-Learn andnon-greedy DLL algorithms with learning by unit propagation can use variableextensions to simulate general resolution without doing restarts. Finally, an exponential lower bound for WRTL where the lemmas are restrictedto short clauses is shown