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.
International Conference on Theory and Applications of Satisfiability Testing
2019
2020-06-18 09:11:54