(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
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Cas Cremers (CC) |
| Conference: | SAT International Conference on Theory and Applications of Satisfiability Testing |
| Depositing User: | Benjamin Kiesl |
| Date Deposited: | 23 May 2019 18:00 |
| Last Modified: | 18 Jun 2020 09:11 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2881 |
Actions
Actions (login required)
 |
View Item |