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.
展开▼
