Extended Resolution Simulates DRAT.
Lecture Notes in Artificial Intelligence(2018)
摘要
We prove that extended resolution-a well-known proof system introduced by Tseitin-polynomially simulates DRAT, the standard proof system in modern SAT solving. Our simulation procedure takes as input a DRAT proof and transforms it into an extended-resolution proof whose size is only polynomial with respect to the original proof. Based on our simulation, we implemented a tool that transforms DRAT proofs into extended-resolution proofs. We ran our tool on several benchmark formulas to estimate the increase in size caused by our simulation in practice. Finally, as a side note, we show how blocked-clause addition-a generalization of the extension rule from extended resolution-can be used to replace the addition of resolution asymmetric tautologies in DRAT without introducing new variables.
更多查看译文
关键词
Extension Rule, Proof System, Tseitin Formulas, Clause Deletion, Pigeonhole Formulas
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络