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.11
URN: urn:nbn:de:0030-drops-166850
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16685/
Böhm, Benjamin ;
Peitl, Tomáš ;
Beyersdorff, Olaf
Should Decisions in QCDCL Follow Prefix Order?
Abstract
Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions.
We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system QCDCL^ANY is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses (QCDCL^UNI-ANI) and asserting cubes (QCDCL^EXI-ANY), respectively.
We model all four approaches by formal proof systems and show that QCDCL^UNI-ANY is exponentially better than QCDCL on false formulas, whereas QCDCL^EXI-ANY is exponentially better than QCDCL on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems.
We complement our theoretical study with some initial experiments that confirm our theoretical findings.
BibTeX - Entry
@InProceedings{bohm_et_al:LIPIcs.SAT.2022.11,
author = {B\"{o}hm, Benjamin and Peitl, Tom\'{a}\v{s} and Beyersdorff, Olaf},
title = {{Should Decisions in QCDCL Follow Prefix Order?}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {11:1--11:19},
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/16685},
URN = {urn:nbn:de:0030-drops-166850},
doi = {10.4230/LIPIcs.SAT.2022.11},
annote = {Keywords: QBF, CDCL, proof complexity, lower bounds}
}
