Olaf Beyersdorff

ORCID

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 84

Top Venues

Electron. Colloquium Comput. Complex.

SAT

CoRR

J. Autom. Reason.

Humboldt University of Berlin, Unter den Linden, Germany (PHD)

Education History

Humboldt University of Berlin, Unter den Linden, Germany

PHD

Publications

Olaf Beyersdorff, Benjamin Böhm, Meena Mahajan
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. AAAI (2024)
Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann
Proof Complexity of Propositional Model Counting. Electron. Colloquium Comput. Complex. (2024)
Olaf Beyersdorff, Johannes Klaus Fichte, Markus Hecher, Tim Hoffmann, Kaspar Kasche
The Relative Strength of #SAT Proof Systems. SAT (2024)
Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
QCDCL with cube learning or pure literal elimination - What is best? Artif. Intell. 336 (2024)
Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
Should Decisions in QCDCL Follow Prefix Order? J. Autom. Reason. 68 (1) (2024)
Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, Luc Nicolas Spachmann
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. MFCS (2024)
Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree. Electron. Colloquium Comput. Complex. (2024)
Olaf Beyersdorff, Benjamin Böhm
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. Log. Methods Comput. Sci. 19 (2) (2023)
Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann
Proof Complexity of Propositional Model Counting. SAT (2023)
Agnes Schleitzer, Olaf Beyersdorff
Classes of Hard Formulas for QBF Resolution. J. Artif. Intell. Res. 77 (2023)
Benjamin Böhm, Olaf Beyersdorff
Lower Bounds for QCDCL via Formula Gauge. J. Autom. Reason. 67 (4) (2023)
Benjamin Böhm, Olaf Beyersdorff
QCDCL vs QBF Resolution: Further Insights. Electron. Colloquium Comput. Complex. (2023)
Benjamin Böhm, Olaf Beyersdorff
QCDCL vs QBF Resolution: Further Insights. SAT (2023)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution. ACM Trans. Comput. Log. 24 (2) (2023)
Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, Andy Oertel
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). Dagstuhl Reports 12 (10) (2022)
Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
QCDCL with Cube Learning or Pure Literal Elimination - What is Best? IJCAI (2022)
Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
Should decisions in QCDCL follow prefix order? Electron. Colloquium Comput. Complex. (2022)
Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
Should Decisions in QCDCL Follow Prefix Order? SAT (2022)
Sarah Sigley, Olaf Beyersdorff
Proof Complexity of Modal Resolution. J. Autom. Reason. 66 (1) (2022)
Agnes Schleitzer, Olaf Beyersdorff
Classes of Hard Formulas for QBF Resolution. Electron. Colloquium Comput. Complex. (2022)
Agnes Schleitzer, Olaf Beyersdorff
Classes of Hard Formulas for QBF Resolution. SAT (2022)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
Building Strategies into QBF Proofs. J. Autom. Reason. 65 (1) (2021)
Olaf Beyersdorff, Joshua Blinkhorn
A simple proof of QBF hardness. Inf. Process. Lett. 168 (2021)
Benjamin Böhm, Olaf Beyersdorff
Lower Bounds for QCDCL via Formula Gauge. SAT (2021)
Olaf Beyersdorff, Benjamin Böhm
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. CoRR (2021)
Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla
QBFFam: A Tool for Generating QBF Families from Proof Complexity. SAT (2021)
Olaf Beyersdorff, Benjamin Böhm
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. ITCS (2021)
Olaf Beyersdorff, Benjamin Böhm
QCDCL with Cube Learning or Pure Literal Elimination - What is best? Electron. Colloquium Comput. Complex. 28 (2021)
Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl
Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths. Electron. Colloquium Comput. Complex. 28 (2021)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood
Hard QBFs for Merge Resolution. CoRR (2020)
Olaf Beyersdorff, Joshua Blinkhorn
Dynamic QBF Dependencies in Reduction and Expansion. ACM Trans. Comput. Log. 21 (2) (2020)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution. LICS (2020)
Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl
Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths. Electron. Colloquium Comput. Complex. 27 (2020)
Olaf Beyersdorff, Benjamin Böhm
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. Electron. Colloquium Comput. Complex. 27 (2020)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution. Electron. Colloquium Comput. Complex. 27 (2020)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood
Hard QBFs for Merge Resolution. Electron. Colloquium Comput. Complex. 27 (2020)
Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl
Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths. SAT (2020)
Olaf Beyersdorff, Luke Hinde, Ján Pich
Reasons for Hardness in QBF Proof Systems. ACM Trans. Comput. Theory 12 (2) (2020)
Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, Ján Pich
Frege Systems for Quantified Boolean Logic. J. ACM 67 (2) (2020)
Olaf Beyersdorff, Uwe Egly, Meena Mahajan, Cláudia Nalon
SAT and Interactions (Dagstuhl Seminar 20061). Dagstuhl Reports 10 (2) (2020)
Olaf Beyersdorff, Joshua Blinkhorn
Lower Bound Techniques for QBF Expansion. Theory Comput. Syst. 64 (3) (2020)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood
Hard QBFs for Merge Resolution. FSTTCS (2020)
Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
Short Proofs in QBF Expansion. SAT (2019)
Joshua Blinkhorn, Olaf Beyersdorff
Proof Complexity of QBF Symmetry Recomputation. SAT (2019)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
Building Strategies into QBF Proofs. STACS (2019)
Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. J. Autom. Reason. 63 (3) (2019)
Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
A game characterisation of tree-like Q-Resolution size. J. Comput. Syst. Sci. 104 (2019)
Olaf Beyersdorff, Joshua Blinkhorn
Proof Complexity of Symmetry Learning in QBF. Electron. Colloquium Comput. Complex. 26 (2019)
Olaf Beyersdorff, Leroy Chew, Mikolás Janota
New Resolution-Based QBF Calculi and Their Proof Complexity. ACM Trans. Comput. Theory 11 (4) (2019)
Olaf Beyersdorff, Luke Hinde
Characterising tree-like Frege proofs for QBF. Inf. Comput. 268 (2019)
Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. Log. Methods Comput. Sci. 15 (1) (2019)
Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
Building Strategies into QBF Proofs. Electron. Colloquium Comput. Complex. 25 (2018)
Olaf Beyersdorff, Judith Clymo
More on Size and Width in QBF Resolution. Electron. Colloquium Comput. Complex. 25 (2018)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Understanding cutting planes for QBFs. Inf. Comput. 262 (2018)
Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
Short Proofs in QBF Expansion. Electron. Colloquium Comput. Complex. 25 (2018)
Joshua Blinkhorn, Olaf Beyersdorff
Dynamic Dependency Awareness for QBF. IJCAI (2018)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
So Simple. ACM Trans. Comput. Log. 19 (1) (2018)
Olaf Beyersdorff, Joshua Blinkhorn
Genuine Lower Bounds for QBF Expansion. STACS (2018)
Olaf Beyersdorff, Judith Clymo, Stefan S. Dantchev, Barnaby Martin
The Riis Complexity Gap for QBF Resolution. Electron. Colloquium Comput. Complex. 25 (2018)
Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs. ITCS (2018)
Judith Clymo, Olaf Beyersdorff
Relating size and width in variants of Q-resolution. Inf. Process. Lett. 138 (2018)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Understanding Cutting Planes for QBFs. Electron. Colloquium Comput. Complex. 24 (2017)
Joshua Blinkhorn, Olaf Beyersdorff
Shortening QBF Proofs with Dependency Schemes. SAT (2017)
Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. Electron. Colloquium Comput. Complex. 24 (2017)
Olaf Beyersdorff, Joshua Blinkhorn
Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds. Electron. Colloquium Comput. Complex. 24 (2017)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Feasible Interpolation for QBF Resolution Calculi. Log. Methods Comput. Sci. 13 (2) (2017)
Olaf Beyersdorff, Luke Hinde, Ján Pich
Reasons for Hardness in QBF Proof Systems. FSTTCS (2017)
Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. CoRR (2017)
Olaf Beyersdorff, Luke Hinde, Ján Pich
Reasons for Hardness in QBF Proof Systems. Electron. Colloquium Comput. Complex. 24 (2017)
Olaf Beyersdorff, Leroy Chew, Mikolas Janota
Extension Variables in QBF Resolution. Electron. Colloquium Comput. Complex. 23 (2016)
Olaf Beyersdorff, Joshua Blinkhorn
Dependency Schemes in QBF Calculi: Semantics and Soundness. Electron. Colloquium Comput. Complex. 23 (2016)
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Lifting QBF Resolution Calculi to DQBF. SAT (2016)
Olaf Beyersdorff, Joshua Blinkhorn
Dependency Schemes in QBF Calculi: Semantics and Soundness. CP (2016)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Understanding Cutting Planes for QBFs. FSTTCS (2016)
Olaf Beyersdorff, Nadia Creignou, Uwe Egly, Heribert Vollmer
SAT and Interactions (Dagstuhl Seminar 16381). Dagstuhl Reports 6 (9) (2016)
Olaf Beyersdorff, Ján Pich
Understanding Gentzen and Frege Systems for QBF. LICS (2016)
Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
Lower Bounds: From Circuits to QBF Proof Systems. ITCS (2016)
Olaf Beyersdorff, Leroy Chew, Mikolas Janota
Extension Variables in QBF Resolution. AAAI Workshop: Beyond NP (2016)
Joshua Blinkhorn, Olaf Beyersdorff
Dependency Schemes in QBF Calculi: Semantics and Soundness. QBF@SAT (2016)
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Lifting QBF Resolution Calculi to DQBF. CoRR (2016)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Are Short Proofs Narrow? QBF Resolution is not Simple. STACS (2016)
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Lifting QBF Resolution Calculi to DQBF. Electron. Colloquium Comput. Complex. 23 (2016)
Olaf Beyersdorff, Ján Pich
Understanding Gentzen and Frege systems for QBF. Electron. Colloquium Comput. Complex. 23 (2016)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Feasible Interpolation for QBF Resolution Calculi. CoRR (2016)
Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
A Game Characterisation of Tree-like Q-resolution Size. LATA (2015)
Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
Lower bounds: from circuits to QBF proof systems. Electron. Colloquium Comput. Complex. 22 (2015)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Feasible Interpolation for QBF Resolution Calculi. Electron. Colloquium Comput. Complex. 22 (2015)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Are Short Proofs Narrow? QBF Resolution is not Simple. Electron. Colloquium Comput. Complex. 22 (2015)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
Feasible Interpolation for QBF Resolution Calculi. ICALP (1) (2015)
Olaf Beyersdorff, Leroy Chew, Mikolás Janota
Proof Complexity of Resolution-based QBF Calculi. STACS (2015)
Olaf Beyersdorff, Leroy Chew, Mikolas Janota
On Unification of QBF Resolution-Based Calculi. MFCS (2) (2014)
Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
A game characterisation of tree-like Q-Resolution size. Electron. Colloquium Comput. Complex. 21 (2014)
Olaf Beyersdorff, Leroy Chew
Tableau vs. Sequent Calculi for Minimal Entailment. CoRR (2014)
Olaf Beyersdorff, Leroy Chew
Tableau vs. Sequent Calculi for Minimal Entailment. Electron. Colloquium Comput. Complex. 21 (2014)
Olaf Beyersdorff, Oliver Kullmann
Unified Characterisations of Resolution Hardness Measures. SAT (2014)
Olaf Beyersdorff, Leroy Chew
The Complexity of Theorem Proving in Circumscription and Minimal Entailment. IJCAR (2014)
Olaf Beyersdorff, Edward A. Hirsch, Jan Krajícek, Rahul Santhanam
Optimal algorithms and proofs (Dagstuhl Seminar 14421). Dagstuhl Reports 4 (10) (2014)
Olaf Beyersdorff, Leroy Chew, Mikolas Janota
Proof Complexity of Resolution-based QBF Calculi. Electron. Colloquium Comput. Complex. 21 (2014)
Olaf Beyersdorff, Leroy Chew
The Complexity of Theorem Proving in Circumscription and Minimal Entailment. Electron. Colloquium Comput. Complex. 21 (2014)
Mikolas Janota, Leroy Chew, Olaf Beyersdorff
On Unification of QBF Resolution-Based Calculi. Electron. Colloquium Comput. Complex. 21 (2014)

Olaf Beyersdorff.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Olaf Beyersdorff