All reports by Author Olaf Beyersdorff:

__
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?

__
TR20-188
| 12th December 2020
__

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

__
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, 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 >>>