QRAT Polynomially Simulates \forall-Exp+Res

Kiesl, Benjamin and Seidl, Martina
(2019) QRAT Polynomially Simulates \forall-Exp+Res.
In: International Conference on Theory and Applications of Satisfiability Testing, July 7 - 12, Lisbon.
Conference: SAT International Conference on Theory and Applications of Satisfiability Testing
(In Press)

Full text not available from this repository. (Request a copy)

Abstract

The proof system \forall-Exp+Res formally captures expansion-based solving of quantified Boolean formulas (QBFs) whereas the QRAT proof system captures QBF preprocessing. From previous work it is known that certain families of formulas have short proofs in QRAT, but not in \forall-Exp+Res. However, it was not known if the two proof systems were incomparable (i.e., if there also existed formulas with short \forall-Exp+Res proofs but without short QRAT proofs), or if QRAT polynomially simulates \forall-Exp+Res. We close this gap of the QBF proof-complexity landscape by presenting a polynomial simulation of \forall-Exp+Res in QRAT.