Extended Resolution Simulates DRAT

摘要

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.