Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Olaf Beyersdorff:

TR20-188 | 12th December 2020
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood

Hard QBFs for Merge Resolution

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

TR20-053 | 16th April 2020
Olaf Beyersdorff, Benjamin Böhm

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution

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

TR20-036 | 9th March 2020
Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths

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

TR20-005 | 17th January 2020
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

Revisions: 1

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

TR19-057 | 6th April 2019
Olaf Beyersdorff, Joshua Blinkhorn

Proof Complexity of Symmetry Learning in QBF

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

ISSN 1433-8092 | Imprint