All reports by Author Olaf Beyersdorff:

__
TR24-038
| 27th February 2024
__

Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann#### Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree

__
TR24-030
| 22nd February 2024
__

Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann#### Proof Complexity of Propositional Model Counting

__
TR23-051
| 18th April 2023
__

Benjamin Böhm, Olaf Beyersdorff#### QCDCL vs QBF Resolution: Further Insights

__
TR22-040
| 10th March 2022
__

Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff#### Should decisions in QCDCL follow prefix order?

__
TR22-036
| 10th March 2022
__

Agnes Schleitzer, Olaf Beyersdorff#### Classes of Hard Formulas for QBF Resolution

Revisions: 1

__
TR21-135
| 6th September 2021
__

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl#### Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths

__
TR21-131
| 10th September 2021
__

Olaf Beyersdorff, Benjamin Böhm#### QCDCL with Cube Learning or Pure Literal Elimination - What is best?

Revisions: 1

__
TR20-188
| 12th December 2020
__

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood#### Hard QBFs for Merge Resolution

Revisions: 1

__
TR20-053
| 16th April 2020
__

Olaf Beyersdorff, Benjamin Böhm#### Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

__
TR20-036
| 9th March 2020
__

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl#### Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths

__
TR20-005
| 17th January 2020
__

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan#### Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

Revisions: 1

__
TR19-057
| 6th April 2019
__

Olaf Beyersdorff, Joshua Blinkhorn#### Proof Complexity of Symmetry Learning in QBF

Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann

We initiate an in-depth proof-complexity analysis of polynomial calculus (Q-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of Q-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for Q-PC, similar in ... more >>>

Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann

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 ...
more >>>

Benjamin Böhm, Olaf Beyersdorff

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 ... more >>>

Benjamin Böhm, Tomáš Peitl, Olaf Beyersdorff

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 ...
more >>>

Agnes Schleitzer, Olaf Beyersdorff

To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q and QU, and only one specific QBF family to separate Q and QU.

Here we provide a general method to construct hard formulas for Q and ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new infinite collection of implication-free DQBF dependency schemes that generalise the reflexive resolution path dependency scheme. We establish soundness of all these schemes, implying that they can be ... more >>>

Olaf Beyersdorff, Benjamin Böhm

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of ... more >>>

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

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 ... more >>>

Olaf Beyersdorff, Benjamin Böhm

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 ...
more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems (Beyersdorff & Pich, LICS 2016), but leaving open the most important case of QBF resolution. Different from the Frege ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn

For quantified Boolean formulas (QBF), a resolution system with a symmetry rule was recently introduced by Kauers and Seidl (Inf. Process. Lett. 2018). In this system, many formulas hard for QBF resolution admit short proofs.

Kauers and Seidl apply the symmetry rule on symmetries of the original formula. Here we ... more >>>