Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2022.22
URN: urn:nbn:de:0030-drops-158326
URL: https://drops.dagstuhl.de/opus/volltexte/2022/15832/
Chew, Leroy ; Slivovsky, Friedrich
Towards Uniform Certification in QBF
| pdf-format: |
|
Abstract
We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution. These results are obtained by taking a technique of Beyersdorff et al. (JACM 2020) that turns strategy extraction into simulation and combining it with new local strategy extraction arguments.This approach leads to simulations that are carried out mainly in propositional logic, with minimal use of the QBF rules. Our proofs therefore provide a new, largely propositional interpretation of the simulated systems. We argue that these results strengthen the case for uniform certification in QBF solving, since many QBF proof systems now fall into place underneath extended QBF Frege.
BibTeX - Entry
@InProceedings{chew_et_al:LIPIcs.STACS.2022.22,
author = {Chew, Leroy and Slivovsky, Friedrich},
title = {{Towards Uniform Certification in QBF}},
booktitle = {39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
pages = {22:1--22:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-222-8},
ISSN = {1868-8969},
year = {2022},
volume = {219},
editor = {Berenbrink, Petra and Monmege, Benjamin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15832},
URN = {urn:nbn:de:0030-drops-158326},
doi = {10.4230/LIPIcs.STACS.2022.22},
annote = {Keywords: QBF, Proof Complexity, Verification, Frege, Extended Frege, Strategy Extraction}
}
| Keywords: | QBF, Proof Complexity, Verification, Frege, Extended Frege, Strategy Extraction | |
| Seminar: | 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 09.03.2022 |
