改进的正则归结与子句学习分离证明系统
Improved Separations of Regular Resolution from Clause Learning Proof Systems
摘要：
我们证明了Alekhnovich，Johannsen，Pitassi和Urquhart的图重言式公式具有多项式大小的池分辨率反驳，仅使用输入引理作为学习子句，并且没有退化的分辨率推断。我们还证明，这些图重言式公式可以反驳多项式大小的DPLL证明与子句学习，即使限制在贪婪，单位传播的DPLL搜索。我们证明了类似的结果的守护，xorfed卵石重言式厄克特证明是很难定期决议。
英文摘要：
We prove that the graph tautology formulas of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses and without degenerate resolution inferences. We also prove that these graph tautology formulas can be refuted by polynomial size DPLL proofs with clause learning, even when restricted to greedy, unit-propagating DPLL search. We prove similar results for the guarded, xor-fied pebbling tautologies which Urquhart proved are hard for regular resolution.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
