Search Results

Documents authored by Beyersdorff, Olaf

Document
DOI: 10.4230/LIPIcs.MFCS.2024.27
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree

Authors: Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999). We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields.
Cite as

Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann. Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.MFCS.2024.27,
  author =	{Beyersdorff, Olaf and Hoffmann, Tim and Kasche, Kaspar and Spachmann, Luc Nicolas},
  title =	{{Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.27},
  URN =		{urn:nbn:de:0030-drops-205834},
  doi =		{10.4230/LIPIcs.MFCS.2024.27},
  annote =	{Keywords: proof complexity, QBF, polynomial calculus, circuits, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.5
The Relative Strength of #SAT Proof Systems

Authors: Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.
Cite as

Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche. The Relative Strength of #SAT Proof Systems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2024.5,
  author =	{Beyersdorff, Olaf and Fichte, Johannes K. and Hecher, Markus and Hoffmann, Tim and Kasche, Kaspar},
  title =	{{The Relative Strength of #SAT Proof Systems}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.5},
  URN =		{urn:nbn:de:0030-drops-205276},
  doi =		{10.4230/LIPIcs.SAT.2024.5},
  annote =	{Keywords: Model Counting, #SAT, Proof Complexity, Proof Systems, Lower Bounds, Knowledge Compilation}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.STACS.2024
LIPIcs, Volume 289, STACS 2024, Complete Volume

Authors: Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
LIPIcs, Volume 289, STACS 2024, Complete Volume
Cite as

41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 1-1048, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{beyersdorff_et_al:LIPIcs.STACS.2024,
  title =	{{LIPIcs, Volume 289, STACS 2024, Complete Volume}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{1--1048},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024},
  URN =		{urn:nbn:de:0030-drops-197098},
  doi =		{10.4230/LIPIcs.STACS.2024},
  annote =	{Keywords: LIPIcs, Volume 289, STACS 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.STACS.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2024.0,
  author =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.0},
  URN =		{urn:nbn:de:0030-drops-197108},
  doi =		{10.4230/LIPIcs.STACS.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.2
Proof Complexity of Propositional Model Counting

Authors: Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann

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

Abstract
Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT'22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE' that is polynomially equivalent to MICE. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs.
Cite as

Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof Complexity of Propositional Model Counting. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2023.2,
  author =	{Beyersdorff, Olaf and Hoffmann, Tim and Spachmann, Luc Nicolas},
  title =	{{Proof Complexity of Propositional Model Counting}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{2:1--2:18},
  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.2},
  URN =		{urn:nbn:de:0030-drops-184647},
  doi =		{10.4230/LIPIcs.SAT.2023.2},
  annote =	{Keywords: model counting, #SAT, proof complexity, proof systems, lower bounds}
}
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/DagRep.12.10.84
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)

Authors: Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel

Published in: Dagstuhl Reports, Volume 12, Issue 10 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22411 "Theory and Practice of SAT and Combinatorial Solving". The purpose of this workshop was to explore the Boolean satisfiability (SAT) problem, which plays a fascinating dual role in computer science. By the theory of NP-completeness, this problem captures thousands of important applications in different fields, and a rich mathematical theory has been developed showing that all these problems are likely to be infeasible to solve in the worst case. But real-world problems are typically not worst-case, and in recent decades exceedingly efficient algorithms based on so-called conflict-driven clause learning (CDCL) have turned SAT solvers into highly practical tools for solving large-scale real-world problems in a wide range of application areas. Analogous developments have taken place for problems beyond NP such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, satisfiability modulo theories (SMT) solving, quantified Boolean formula (QBF) solving, constraint programming, and mixed integer programming, where the conflict-driven paradigm has sometimes been added to other powerful techniques. The current state of the art in combinatorial solving presents a host of exciting challenges at the borderline between theory and practice. Can we gain a deeper scientific understanding of the techniques and heuristics used in modern combinatorial solvers and why they are so successful? Can we develop tools for rigorous analysis of the potential and limitations of these algorithms? Can computational complexity theory be extended to shed light on real-world settings that go beyond worst case? Can more powerful methods of reasoning developed in theoretical research be harnessed to yield improvements in practical performance? And can state-of-the-art combinatorial solvers be enhanced to not only solve problems, but also provide verifiable proofs of correctness for the solutions they produce? This workshop gathered leading applied and theoretical researchers working on SAT and combinatorial optimization more broadly in order to stimulate an exchange of ideas and techniques. We see great opportunities for fruitful interplay between theory and practice in these areas, as well as for technology transfer between different paradigms in combinatorial optimization, and our assessment is that this workshop demonstrated very convincingly that a more vigorous interaction has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel. Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). In Dagstuhl Reports, Volume 12, Issue 10, pp. 84-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.12.10.84,
  author =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  title =	{{Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)}},
  pages =	{84--105},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.10.84},
  URN =		{urn:nbn:de:0030-drops-178212},
  doi =		{10.4230/DagRep.12.10.84},
  annote =	{Keywords: Boolean satisfiability (SAT), SAT solving, computational complexity, proof complexity, combinatorial solving, combinatorial optimization, constraint programming, mixed integer linear programming}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.5
Classes of Hard Formulas for QBF Resolution

Authors: Agnes Schleitzer and Olaf Beyersdorff

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

Abstract
To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q-Res and QU-Res, and only one specific QBF family to separate Q-Res and QU-Res. Here we provide a general method to construct hard formulas for Q-Res and QU-Res. The construction uses simple propositional formulas (e.g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Σ₂^b formulas without constant winning strategies). This leads to a host of new hard formulas, including new classes of hard random QBFs. We further present generic constructions for formulas separating Q-Res and QU-Res, and for separating Q-Res and LD-Q-Res.
Cite as

Agnes Schleitzer and Olaf Beyersdorff. Classes of Hard Formulas for QBF Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{schleitzer_et_al:LIPIcs.SAT.2022.5,
  author =	{Schleitzer, Agnes and Beyersdorff, Olaf},
  title =	{{Classes of Hard Formulas for QBF Resolution}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{5:1--5:18},
  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.5},
  URN =		{urn:nbn:de:0030-drops-166792},
  doi =		{10.4230/LIPIcs.SAT.2022.5},
  annote =	{Keywords: QBF, proof complexity, resolution, separations}
}
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}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.12
Hard QBFs for Merge Resolution

Authors: Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, and Gaurav Sood

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
We prove the first proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems. Here we show the first exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems ∀Exp+Res and IR.
Cite as

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, and Gaurav Sood. Hard QBFs for Merge Resolution. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2020.12,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua and Mahajan, Meena and Peitl, Tom\'{a}\v{s} and Sood, Gaurav},
  title =	{{Hard QBFs for Merge Resolution}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.12},
  URN =		{urn:nbn:de:0030-drops-132530},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.12},
  annote =	{Keywords: QBF, resolution, proof complexity, lower bounds}
}
Document
DOI: 10.4230/DagRep.10.2.1
SAT and Interactions (Dagstuhl Seminar 20061)

Authors: Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Cláudia Nalon

Published in: Dagstuhl Reports, Volume 10, Issue 2 (2020)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 20061 "SAT and Interactions". The seminar brought together theoreticians and practitioners from the areas of proof complexity and proof theory, SAT and QBF solving, MaxSAT, and modal logics, who discussed recent developments in their fields and embarked on an interdisciplinary exchange of ideas and techniques between these neighbouring subfields of SAT.
Cite as

Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Cláudia Nalon. SAT and Interactions (Dagstuhl Seminar 20061). In Dagstuhl Reports, Volume 10, Issue 2, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.10.2.1,
  author =	{Beyersdorff, Olaf and Egly, Uwe and Mahajan, Meena and Nalon, Cl\'{a}udia},
  title =	{{SAT and Interactions (Dagstuhl Seminar 20061)}},
  pages =	{1--18},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{10},
  number =	{2},
  editor =	{Beyersdorff, Olaf and Egly, Uwe and Mahajan, Meena and Nalon, Cl\'{a}udia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.10.2.1},
  URN =		{urn:nbn:de:0030-drops-130576},
  doi =		{10.4230/DagRep.10.2.1},
  annote =	{Keywords: SAT, MaxSAT, QBF, proof complexity, deep inference, modal logic, solving}
}
Document
DOI: 10.4230/LIPIcs.STACS.2019.14
Building Strategies into QBF Proofs

Authors: Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
Strategy extraction is of paramount importance for quantified Boolean formulas (QBF), both in solving and proof complexity. It extracts (counter)models for a QBF from a run of the solver resp. the proof of the QBF, thereby allowing to certify the solver’s answer resp. establish soundness of the system. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the first QBF system where (partial) strategies are built into the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus, introduced to model QCDCL solving. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-type calculus for DQBF, thus opening future avenues into DQBF CDCL solving.
Cite as

Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building Strategies into QBF Proofs. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2019.14,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua and Mahajan, Meena},
  title =	{{Building Strategies into QBF Proofs}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.14},
  URN =		{urn:nbn:de:0030-drops-102538},
  doi =		{10.4230/LIPIcs.STACS.2019.14},
  annote =	{Keywords: QBF, DQBF, resolution, proof complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.12
Genuine Lower Bounds for QBF Expansion

Authors: Olaf Beyersdorff and Joshua Blinkhorn

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
We propose the first general technique for proving genuine lower bounds in expansion-based QBF proof systems. We present the technique in a framework centred on natural properties of winning strategies in the 'evaluation game' interpretation of QBF semantics. As applications, we prove an exponential proof-size lower bound for a whole class of formula families, and demonstrate the power of our approach over existing methods by providing alternative short proofs of two known hardness results. We also use our technique to deduce a result with manifest practical import: in the absence of propositional hardness, formulas separating the two major QBF expansion systems must have unbounded quantifier alternations.
Cite as

Olaf Beyersdorff and Joshua Blinkhorn. Genuine Lower Bounds for QBF Expansion. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2018.12,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua},
  title =	{{Genuine Lower Bounds for QBF Expansion}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.12},
  URN =		{urn:nbn:de:0030-drops-85174},
  doi =		{10.4230/LIPIcs.STACS.2018.12},
  annote =	{Keywords: QBF, proof complexity, lower-bound techniques, resolution}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.14
Reasons for Hardness in QBF Proof Systems

Authors: Olaf Beyersdorff, Luke Hinde, and Ján Pich

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
We aim to understand inherent reasons for lower bounds for QBF proof systems, and revisit and compare two previous approaches in this direction. The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via strategy extraction (Beyersdorff & Pich, LICS'16). Here we show a refined version of strategy extraction and thereby for any QBF proof system obtain a trichotomy for hardness: (1) via circuit lower bounds, (2) via propositional Resolution lower bounds, or (3) `genuine' QBF lower bounds. The second approach tries to explain QBF lower bounds through quantifier alternations in a system called relaxing QU-Res (Chen, ICALP'16). We prove a strong lower bound for relaxing QU-Res, which also exhibits significant shortcomings of that model. Prompted by this we propose an alternative, improved version, allowing more flexible oracle queries in proofs. We show that lower bounds in our new model correspond to the trichotomy obtained via strategy extraction.
Cite as

Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for Hardness in QBF Proof Systems. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2017.14,
  author =	{Beyersdorff, Olaf and Hinde, Luke and Pich, J\'{a}n},
  title =	{{Reasons for Hardness in QBF Proof Systems}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.14},
  URN =		{urn:nbn:de:0030-drops-83824},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.14},
  annote =	{Keywords: proof complexity, quantified Boolean formulas, resolution, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2018.9
Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs

Authors: Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde

Published in: LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)

Abstract
As a natural extension of the SAT problem, an array of proof systems for quantified Boolean formulas (QBF) have been proposed, many of which extend a propositional proof system to handle universal quantification. By formalising the construction of the QBF proof system obtained from a propositional proof system by adding universal reduction (Beyersdorff, Bonacina & Chew, ITCS'16), we present a new technique for proving proof-size lower bounds in these systems. The technique relies only on two semantic measures: the cost of a QBF, and the capacity of a proof. By examining the capacity of proofs in several QBF systems, we are able to use the technique to obtain lower bounds based on cost alone. As applications of the technique, we first prove exponential lower bounds for a new family of simple QBFs representing equality. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first 'genuine' lower bounds of this kind, which apply to the QBF analogues of resolution, Cutting Planes, and Polynomial Calculus. Finally, we employ the technique to give a simple proof of hardness for a prominent family of QBFs.
Cite as

Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.ITCS.2018.9,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua and Hinde, Luke},
  title =	{{Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs}},
  booktitle =	{9th Innovations in Theoretical Computer Science Conference (ITCS 2018)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-060-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{94},
  editor =	{Karlin, Anna R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.9},
  URN =		{urn:nbn:de:0030-drops-83228},
  doi =		{10.4230/LIPIcs.ITCS.2018.9},
  annote =	{Keywords: quantified Boolean formulas, proof complexity, lower bounds}
}
Document
DOI: 10.4230/DagRep.6.9.74
SAT and Interactions (Dagstuhl Seminar 16381)

Authors: Olaf Beyersdorff, Nadia Creignou, Uwe Egly, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 6, Issue 9 (2017)

Abstract
This report documents the programme and outcomes of Dagstuhl Seminar 16381 "SAT and Interactions". The seminar brought together researchers from different areas from theoretical computer science involved with various aspects of satisfiability. A key objective of the seminar has been to initiate or consolidate discussions among the different groups for a fresh attack on one of the most important problems in theoretical computer science and mathematics.
Cite as

Olaf Beyersdorff, Nadia Creignou, Uwe Egly, and Heribert Vollmer. SAT and Interactions (Dagstuhl Seminar 16381). In Dagstuhl Reports, Volume 6, Issue 9, pp. 74-93, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.6.9.74,
  author =	{Beyersdorff, Olaf and Creignou, Nadia and Egly, Uwe and Vollmer, Heribert},
  title =	{{SAT and Interactions (Dagstuhl Seminar 16381)}},
  pages =	{74--93},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{9},
  editor =	{Beyersdorff, Olaf and Creignou, Nadia and Egly, Uwe and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.9.74},
  URN =		{urn:nbn:de:0030-drops-69116},
  doi =		{10.4230/DagRep.6.9.74},
  annote =	{Keywords: Combinatorics, Computational Complexity, P vs. NP, Proof Complexity, Quantified Boolean formulas, SAT-solvers, satisfiability problem}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.40
Understanding Cutting Planes for QBFs

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res. Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.
Cite as

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2016.40,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
  title =	{{Understanding Cutting Planes for QBFs}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.40},
  URN =		{urn:nbn:de:0030-drops-68758},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.40},
  annote =	{Keywords: proof complexity, QBF, cutting planes, resolution, simulations}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.15
Are Short Proofs Narrow? QBF Resolution is not Simple

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
The groundbreaking paper 'Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that space lower bounds again can be obtained via width lower bounds. Here we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBF). A mixed picture emerges. Our main results show that both the relations between size and width as well as between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems Forall-Exp+Res and IR-calc, however only in the weak tree-like models. Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results we exhibit space and width-preserving simulations between QBF resolution calculi.
Cite as

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are Short Proofs Narrow? QBF Resolution is not Simple. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2016.15,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
  title =	{{Are Short Proofs Narrow? QBF Resolution is not Simple}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.15},
  URN =		{urn:nbn:de:0030-drops-57164},
  doi =		{10.4230/LIPIcs.STACS.2016.15},
  annote =	{Keywords: proof complexity, QBF, resolution, lower bound techniques, simulations}
}
Document
DOI: 10.4230/LIPIcs.STACS.2015.76
Proof Complexity of Resolution-based QBF Calculi

Authors: Olaf Beyersdorff, Leroy Chew, and Mikolás Janota

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems as long-distance Q-resolution and extensions. With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Büning et al. [34] for the strong expansion-based calculus IR-calc. Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers (forallExp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two different classes were not known before.
Cite as

Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof Complexity of Resolution-based QBF Calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 76-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2015.76,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Janota, Mikol\'{a}s},
  title =	{{Proof Complexity of Resolution-based QBF Calculi}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{76--89},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.76},
  URN =		{urn:nbn:de:0030-drops-49057},
  doi =		{10.4230/LIPIcs.STACS.2015.76},
  annote =	{Keywords: proof complexity, QBF, lower bound techniques, separations}
}
Document
DOI: 10.4230/DagRep.4.10.51
Optimal algorithms and proofs (Dagstuhl Seminar 14421)

Authors: Olaf Beyersdorff, Edward A. Hirsch, Jan Krajicek, and Rahul Santhanam

Published in: Dagstuhl Reports, Volume 4, Issue 10 (2015)

Abstract
This report documents the programme and the outcomes of the Dagstuhl Seminar 14421 "Optimal algorithms and proofs". The seminar brought together researchers working in computational and proof complexity, logic, and the theory of approximations. Each of these areas has its own, but connected notion of optimality; and the main aim of the seminar was to bring together researchers from these different areas, for an exchange of ideas, techniques, and open questions, thereby triggering new research collaborations across established research boundaries.
Cite as

Olaf Beyersdorff, Edward A. Hirsch, Jan Krajicek, and Rahul Santhanam. Optimal algorithms and proofs (Dagstuhl Seminar 14421). In Dagstuhl Reports, Volume 4, Issue 10, pp. 51-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.4.10.51,
  author =	{Beyersdorff, Olaf and Hirsch, Edward A. and Krajicek, Jan and Santhanam, Rahul},
  title =	{{Optimal algorithms and proofs (Dagstuhl Seminar 14421)}},
  pages =	{51--68},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Hirsch, Edward A. and Krajicek, Jan and Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.10.51},
  URN =		{urn:nbn:de:0030-drops-48923},
  doi =		{10.4230/DagRep.4.10.51},
  annote =	{Keywords: computational complexity, proof complexity, approximation algorithms, optimal algorithms, optimal proof systems, speedup theorems}
}
Document
DOI: 10.4230/DagSemProc.10061.4
Hardness of Parameterized Resolution

Authors: Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)

Abstract
Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles. We broadly investigate Parameterized Resolution obtaining the following main results: 1) We introduce a purely combinatorial approach to obtain lower bounds to the proof size in tree-like Parameterized Resolution. For this we devise a new asymmetric Prover-Delayer game which characterizes proofs in (parameterized) tree-like Resolution. By exhibiting good Delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. 2) Interpreting a well-known FPT algorithm for vertex cover as a DPLL procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized Resolution and show that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. 3) We answer a question posed by Dantchev, Martin, and Szeider showing that dag-like Parameterized Resolution is not fpt-bounded. We obtain this result by proving that the pigeonhole principle requires proofs of size $n^{Omega(k)}$ in dag-like Parameterized Resolution. For this lower bound we use a different Prover-Delayer game which was developed for Resolution by Pudlák.
Cite as

Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Hardness of Parameterized Resolution. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.4,
  author =	{Beyersdorff, Olaf and Galesi, Nicola and Lauria, Massimo},
  title =	{{Hardness of Parameterized Resolution}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--28},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.4},
  URN =		{urn:nbn:de:0030-drops-25254},
  doi =		{10.4230/DagSemProc.10061.4},
  annote =	{Keywords: Proof complexity, parameterized complexity, Resolution, Prover-Delayer Games}
}
Document
DOI: 10.4230/DagSemProc.10061.5
Proof Complexity of Propositional Default Logic

Authors: Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)

Abstract
Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen's system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti's enhanced calculus for skeptical default reasoning.
Cite as

Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer. Proof Complexity of Propositional Default Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.5,
  author =	{Beyersdorff, Olaf and Meier, Arne and M\"{u}ller, Sebastian and Thomas, Michael and Vollmer, Heribert},
  title =	{{Proof Complexity of Propositional Default Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.5},
  URN =		{urn:nbn:de:0030-drops-25261},
  doi =		{10.4230/DagSemProc.10061.5},
  annote =	{Keywords: Proof complexity, default logic, sequent calculus}
}
Document
DOI: 10.4230/OASIcs.ATMOS.2009.2147
Edges as Nodes - a New Approach to Timetable Information

Authors: Olaf Beyersdorff and Yevgen Nebesov

Published in: OASIcs, Volume 12, 9th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'09) (2009)

Abstract
In this paper we suggest a new approach to timetable information by introducing the ``edge-converted graph'' of a timetable. Using this model we present simple algorithms that solve the earliest arrival problem (EAP) and the minimum number of transfers problem (MNTP). For constant-degree graphs this yields linear-time algorithms for EAP and MNTP which improves upon the known \emph{Dijkstra}-based approaches. We also test the performance of our algorithms against the classical algorithms for EAP and MNTP in the time-expanded model.
Cite as

Olaf Beyersdorff and Yevgen Nebesov. Edges as Nodes - a New Approach to Timetable Information. In 9th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'09). Open Access Series in Informatics (OASIcs), Volume 12, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:OASIcs.ATMOS.2009.2147,
  author =	{Beyersdorff, Olaf and Nebesov, Yevgen},
  title =	{{Edges as Nodes - a New Approach to Timetable Information}},
  booktitle =	{9th Workshop on Algorithmic Approaches for Transportation Modeling, Optimization, and Systems (ATMOS'09)},
  pages =	{1--12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-11-8},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{12},
  editor =	{Clausen, Jens and Di Stefano, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ATMOS.2009.2147},
  URN =		{urn:nbn:de:0030-drops-21478},
  doi =		{10.4230/OASIcs.ATMOS.2009.2147},
  annote =	{Keywords: Timetable infomation, earliest arrival problem, minimum number of transfers problem, time-expanded model Timetable infomation, earliest arrival problem, minimum number of transfers problem, time-expanded model}
}
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