Search Results

Documents authored by Böhm, Benjamin

Document
DOI: 10.4230/LIPIcs.SAT.2023.4
QCDCL vs QBF Resolution: Further Insights

Authors: Benjamin Böhm and Olaf Beyersdorff

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions - lead to incomparable systems for almost all choices of these policies.
Cite as

Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF Resolution: Further Insights. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bohm_et_al:LIPIcs.SAT.2023.4,
  author =	{B\"{o}hm, Benjamin and Beyersdorff, Olaf},
  title =	{{QCDCL vs QBF Resolution: Further Insights}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.4},
  URN =		{urn:nbn:de:0030-drops-184660},
  doi =		{10.4230/LIPIcs.SAT.2023.4},
  annote =	{Keywords: QBF, CDCL, resolution, proof complexity, simulations, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.11
Should Decisions in QCDCL Follow Prefix Order?

Authors: Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.
Cite as

Benjamin Böhm, Tomáš Peitl, and Olaf Beyersdorff. Should Decisions in QCDCL Follow Prefix Order?. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SAT.2022.11},
  URN =		{urn:nbn:de:0030-drops-166850},
  doi =		{10.4230/LIPIcs.SAT.2022.11},
  annote =	{Keywords: QBF, CDCL, proof complexity, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2021.12
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

Authors: Olaf Beyersdorff and Benjamin Böhm

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)

Abstract
QBF solvers implementing the QCDCL paradigm are powerful algorithms that successfully tackle many computationally complex applications. However, our theoretical understanding of the strength and limitations of these QCDCL solvers is very limited. In this paper we suggest to formally model QCDCL solvers as proof systems. We define different policies that can be used for decision heuristics and unit propagation and give rise to a number of sound and complete QBF proof systems (and hence new QCDCL algorithms). With respect to the standard policies used in practical QCDCL solving, we show that the corresponding QCDCL proof system is incomparable (via exponential separations) to Q-resolution, the classical QBF resolution system used in the literature. This is in stark contrast to the propositional setting where CDCL and resolution are known to be p-equivalent. This raises the question what formulas are hard for standard QCDCL, since Q-resolution lower bounds do not necessarily apply to QCDCL as we show here. In answer to this question we prove several lower bounds for QCDCL, including exponential lower bounds for a large class of random QBFs. We also introduce a strengthening of the decision heuristic used in classical QCDCL, which does not necessarily decide variables in order of the prefix, but still allows to learn asserting clauses. We show that with this decision policy, QCDCL can be exponentially faster on some formulas. We further exhibit a QCDCL proof system that is p-equivalent to Q-resolution. In comparison to classical QCDCL, this new QCDCL version adapts both decision and unit propagation policies.
Cite as

Olaf Beyersdorff and Benjamin Böhm. Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.ITCS.2021.12,
  author =	{Beyersdorff, Olaf and B\"{o}hm, Benjamin},
  title =	{{Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.12},
  URN =		{urn:nbn:de:0030-drops-135519},
  doi =		{10.4230/LIPIcs.ITCS.2021.12},
  annote =	{Keywords: CDCL, QBF, QCDCL, proof complexity, resolution, Q-resolution}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact