37 citations · 71 across the 9 of their papers we have counts for
5 papers · 1 filter
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…
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…
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…