License:
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.10
URN: urn:nbn:de:0030-drops-166845
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16684/
Chew, Leroy ;
Heule, Marijn J. H.
Relating Existing Powerful Proof Systems for QBF
Abstract
We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not have strategy extraction. Because EUR heavily uses resolution paths our technique also brings resolution path dependency and sequent systems closer together. While we do not recommend G for practical applications this work can potentially show what features are needed for a new QBF checking format stronger than QRAT.
BibTeX - Entry
@InProceedings{chew_et_al:LIPIcs.SAT.2022.10,
author = {Chew, Leroy and Heule, Marijn J. H.},
title = {{Relating Existing Powerful Proof Systems for QBF}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {10:1--10:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16684},
URN = {urn:nbn:de:0030-drops-166845},
doi = {10.4230/LIPIcs.SAT.2022.10},
annote = {Keywords: QBF, Proof Complexity, Verification, Strategy Extraction, Sequent Calculus}
}
Keywords: |
|
QBF, Proof Complexity, Verification, Strategy Extraction, Sequent Calculus |
Collection: |
|
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) |
Issue Date: |
|
2022 |
Date of publication: |
|
28.07.2022 |