| ||||
| ||||
![]() Title:Extended Resolution Simulates DRAT Conference:IJCAR-2018 Tags:blocked clauses, drat, extended resolution, proof complexity, propositional logic and sat Abstract: 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. Extended Resolution Simulates DRAT ![]() Extended Resolution Simulates DRAT | ||||
Copyright © 2002 – 2025 EasyChair |