带有引理的归结树：表征带有子句学习的DLL算法的归结精化
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
摘要：
介绍了带引理的w-归结树（WRTL）和带输入引理的w-归结树（WRTI）。当不满足正则性条件时，类Dag分解等价于WRTL和WRTI。对于正则证明，给出了正则dag-like归结与正则WRTL和正则WRTI之间的指数分离。证明了使用基于单位传播的子句学习的DLL证明搜索算法可以用正则WRTI多项式模拟。更一般地，通过单元传播学习的非贪婪DLL算法等价于常规WRTI。定义了子句学习的一般形式，称为DLL-Learn，它相当于常规WRTL。一个变量扩展的方法是用来模拟的决议，定期WRTI，使用一种简化形式的证明跟踪扩展。DLL-Learn和非贪婪DLL算法通过单元传播学习，可以使用变量扩展来模拟一般解决方案，而无需重新启动。最后，WRTL的指数下界的引理被限制到短子句。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
