37 citations · 71 across the 9 of their papers we have counts for
9 papers
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
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 th…
Hard QBFs for Merge Resolution
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan +2
We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantifi…
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs
Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
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…
Feasible Interpolation for QBF Resolution Calculi
Olaf Beyersdorff, Leroy Chew, Meena Mahajan +1
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation techni…
Lifting QBF Resolution Calculi to DQBF
Olaf Beyersdorff, Leroy Chew, Renate Schmidt +1
We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (…
Tableau vs. Sequent Calculi for Minimal Entailment
Olaf Beyersdorff, Leroy Chew
In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (1992). Our main result shows that O…
Model Checking CTL is Almost Always Inherently Sequential
Olaf Beyersdorff, Arne Meier, Martin Mundhenk +3
The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the…
The Complexity of Propositional Implication
Olaf Beyersdorff, Arne Meier, Michael Thomas +1
The question whether a set of formulae G implies a formula f is fundamental. The present paper studies the complexity of the above implication problem for propositional formulae th…
The Complexity of Reasoning for Fragments of Default Logic
Olaf Beyersdorff, Arne Meier, Michael Thomas +1
Default logic was introduced by Reiter in 1980. In 1992, Gottlob classified the complexity of the extension existence problem for propositional default logic as $\SigmaPtwo$-comple…