Olaf Beyersdorff

According to our database, Olaf Beyersdorff authored at least 92 papers between 2004 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Polynomial Calculus for Quantified Boolean Logic: Lower Bounds through Circuits and Degree.

Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann

Electron. Colloquium Comput. Complex., 2024

Proof Complexity of Propositional Model Counting.

Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann

Electron. Colloquium Comput. Complex., 2024

Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs.

Olaf Beyersdorff, Benjamin Böhm, Meena Mahajan

Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023

Lower Bounds for QCDCL via Formula Gauge.

Benjamin Böhm, Olaf Beyersdorff

J. Autom. Reason., December, 2023

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution.

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl

ACM Trans. Comput. Log., April, 2023

Classes of Hard Formulas for QBF Resolution.

Agnes Schleitzer, Olaf Beyersdorff

J. Artif. Intell. Res., 2023

QCDCL vs QBF Resolution: Further Insights.

Benjamin Böhm, Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2023

2022

Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411).

Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, Andy Oertel

Dagstuhl Reports, October, 2022

Proof Complexity of Modal Resolution.

Sarah Sigley, Olaf Beyersdorff

J. Autom. Reason., 2022

Should decisions in QCDCL follow prefix order?

Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2022

QCDCL with Cube Learning or Pure Literal Elimination - What is Best?

Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

2021

Quantified Boolean Formulas.

Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

A simple proof of QBF hardness.

Olaf Beyersdorff, Joshua Blinkhorn

Inf. Process. Lett., 2021

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

Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl

Electron. Colloquium Comput. Complex., 2021

QCDCL with Cube Learning or Pure Literal Elimination - What is best?

Olaf Beyersdorff, Benjamin Böhm

Electron. Colloquium Comput. Complex., 2021

QBFFam: A Tool for Generating QBF Families from Proof Complexity.

Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

2020

Dynamic QBF Dependencies in Reduction and Expansion.

Olaf Beyersdorff, Joshua Blinkhorn

ACM Trans. Comput. Log., 2020

Lower Bound Techniques for QBF Expansion.

Olaf Beyersdorff, Joshua Blinkhorn

Theory Comput. Syst., 2020

Frege Systems for Quantified Boolean Logic.

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, Ján Pich

J. ACM, 2020

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

Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl

Electron. Colloquium Comput. Complex., 2020

Hard QBFs for Merge Resolution.

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood

Electron. Colloquium Comput. Complex., 2020

Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution.

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Electron. Colloquium Comput. Complex., 2020

Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution.

Olaf Beyersdorff, Benjamin Böhm

Electron. Colloquium Comput. Complex., 2020

SAT and Interactions (Dagstuhl Seminar 20061).

Olaf Beyersdorff, Uwe Egly, Meena Mahajan, Cláudia Nalon

Dagstuhl Reports, 2020

2019

New Resolution-Based QBF Calculi and Their Proof Complexity.

Olaf Beyersdorff, Leroy Chew, Mikolás Janota

ACM Trans. Comput. Theory, 2019

A game characterisation of tree-like Q-Resolution size.

Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah

J. Comput. Syst. Sci., 2019

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.

Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda

J. Autom. Reason., 2019

Characterising tree-like Frege proofs for QBF.

Olaf Beyersdorff, Luke Hinde

Inf. Comput., 2019

Proof Complexity of Symmetry Learning in QBF.

Olaf Beyersdorff, Joshua Blinkhorn

Electron. Colloquium Comput. Complex., 2019

Proof Complexity of QBF Symmetry Recomputation.

Joshua Blinkhorn, Olaf Beyersdorff

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

2018

Are Short Proofs Narrow? QBF Resolution Is <i>Not</i> So Simple.

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

ACM Trans. Comput. Log., 2018

Relating size and width in variants of Q-resolution.

Judith Clymo, Olaf Beyersdorff

Inf. Process. Lett., 2018

The Riis Complexity Gap for QBF Resolution.

Olaf Beyersdorff, Judith Clymo, Stefan S. Dantchev, Barnaby Martin

Electron. Colloquium Comput. Complex., 2018

Short Proofs in QBF Expansion.

Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan

Electron. Colloquium Comput. Complex., 2018

More on Size and Width in QBF Resolution.

Olaf Beyersdorff, Judith Clymo

Electron. Colloquium Comput. Complex., 2018

Building Strategies into QBF Proofs.

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Electron. Colloquium Comput. Complex., 2018

Genuine Lower Bounds for QBF Expansion.

Olaf Beyersdorff, Joshua Blinkhorn

Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science, 2018

Dynamic Dependency Awareness for QBF.

Joshua Blinkhorn, Olaf Beyersdorff

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

2017

Reasons for Hardness in QBF Proof Systems.

Olaf Beyersdorff, Luke Hinde, Ján Pich

Electron. Colloquium Comput. Complex., 2017

Understanding Cutting Planes for QBFs.

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Electron. Colloquium Comput. Complex., 2017

Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs.

Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde

Electron. Colloquium Comput. Complex., 2017

Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds.

Olaf Beyersdorff, Joshua Blinkhorn

Electron. Colloquium Comput. Complex., 2017

Shortening QBF Proofs with Dependency Schemes.

Joshua Blinkhorn, Olaf Beyersdorff

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

2016

Understanding Gentzen and Frege systems for QBF.

Olaf Beyersdorff, Ján Pich

Electron. Colloquium Comput. Complex., 2016

Lifting QBF Resolution Calculi to DQBF.

Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda

Electron. Colloquium Comput. Complex., 2016

Extension Variables in QBF Resolution.

Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Electron. Colloquium Comput. Complex., 2016

Dependency Schemes in QBF Calculi: Semantics and Soundness.

Olaf Beyersdorff, Joshua Blinkhorn

Electron. Colloquium Comput. Complex., 2016

SAT and Interactions (Dagstuhl Seminar 16381).

Olaf Beyersdorff, Nadia Creignou, Uwe Egly, Heribert Vollmer

Dagstuhl Reports, 2016

2015

Are Short Proofs Narrow? QBF Resolution is not Simple.

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Electron. Colloquium Comput. Complex., 2015

Feasible Interpolation for QBF Resolution Calculi.

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Electron. Colloquium Comput. Complex., 2015

Lower bounds: from circuits to QBF proof systems.

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew

Electron. Colloquium Comput. Complex., 2015

2014

On Unification of QBF Resolution-Based Calculi.

Mikolas Janota, Leroy Chew, Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2014

Proof Complexity of Resolution-based QBF Calculi.

Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Electron. Colloquium Comput. Complex., 2014

Tableau vs. Sequent Calculi for Minimal Entailment.

Olaf Beyersdorff, Leroy Chew

Electron. Colloquium Comput. Complex., 2014

The Complexity of Theorem Proving in Circumscription and Minimal Entailment.

Olaf Beyersdorff, Leroy Chew

Electron. Colloquium Comput. Complex., 2014

Optimal algorithms and proofs (Dagstuhl Seminar 14421).

Olaf Beyersdorff, Edward A. Hirsch, Jan Krajícek, Rahul Santhanam

Dagstuhl Reports, 2014

Unified Characterisations of Resolution Hardness Measures.

Olaf Beyersdorff, Oliver Kullmann

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 2014

2013

Parameterized Complexity of DPLL Search Procedures.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

ACM Trans. Comput. Log., 2013

A characterization of tree-like Resolution size.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Inf. Process. Lett., 2013

The Complexity of Theorem Proving in Autoepistemic Logic.

Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2013

2012

The complexity of reasoning for fragments of default logic.

Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer

J. Log. Comput., 2012

Verifying Proofs in Constant Depth.

Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer

Electron. Colloquium Comput. Complex., 2012

Non-classical Aspects in Proof Complexity.

Olaf Beyersdorff

Cuvillier, ISBN: 978-3-9540403-6-0, 2012

2011

Do there exist complete sets for promise classes?

Olaf Beyersdorff, Zenon Sadowski

Math. Log. Q., 2011

Model Checking CTL is Almost Always Inherently Sequential

Olaf Beyersdorff, Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Heribert Vollmer

Log. Methods Comput. Sci., 2011

Proof complexity of propositional default logic.

Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, Heribert Vollmer

Arch. Math. Log., 2011

Verifying Proofs in Constant Depth.

Olaf Beyersdorff, Samir Datta, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer

Proceedings of the Mathematical Foundations of Computer Science 2011, 2011

Proof Complexity of Non-classical Logics.

Olaf Beyersdorff, Oliver Kutz

Proceedings of the Lectures on Logic and Computation, 2011

2010

A tight Karp-Lipton collapse result in bounded arithmetic.

Olaf Beyersdorff, Sebastian Müller

ACM Trans. Comput. Log., 2010

The Deduction Theorem for Strong Propositional Proof Systems.

Olaf Beyersdorff

Theory Comput. Syst., 2010

A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover-Delayer games.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Inf. Process. Lett., 2010

Parameterized Bounded-Depth Frege is Not Optimal.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander A. Razborov

Electron. Colloquium Comput. Complex., 2010

Hardness of Parameterized Resolution.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Electron. Colloquium Comput. Complex., 2010

Different Approaches to Proof Systems.

Olaf Beyersdorff, Sebastian Müller

Proceedings of the Theory and Applications of Models of Computation, 7th Annual Conference, 2010

Proof Complexity of Non-classical Logics.

Olaf Beyersdorff

Proceedings of the Theory and Applications of Models of Computation, 7th Annual Conference, 2010

2009

Nondeterministic functions and the existence of optimal proof systems.

Olaf Beyersdorff, Johannes Köbler, Jochen Messner

Theor. Comput. Sci., 2009

On the correspondence between arithmetic theories and propositional proof systems - a survey.

Olaf Beyersdorff

Math. Log. Q., 2009

The complexity of propositional implication.

Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer

Inf. Process. Lett., 2009

Characterizing the Existence of Optimal Proof Systems and Complete Sets for Promise Classes.

Olaf Beyersdorff, Zenon Sadowski

Electron. Colloquium Comput. Complex., 2009

Proof Systems that Take Advice.

Olaf Beyersdorff, Johannes Köbler, Sebastian Müller

Electron. Colloquium Comput. Complex., 2009

Comparing axiomatizations of free pseudospaces.

Olaf Beyersdorff

Arch. Math. Log., 2009

On the Existence of Complete Disjoint NP-Pairs.

Olaf Beyersdorff

Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Does Advice Help to Prove Propositional Tautologies?

Olaf Beyersdorff, Sebastian Müller

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Edges as Nodes - a New Approach to Timetable Information .

Olaf Beyersdorff, Yevgen Nebesov

Proceedings of the ATMOS 2009, 2009

2008

Nondeterministic Instance Complexity and Proof Systems with Advice.

Olaf Beyersdorff, Johannes Köbler, Sebastian Müller

Electron. Colloquium Comput. Complex., 2008

Logical Closure Properties of Propositional Proof Systems.

Olaf Beyersdorff

Proceedings of the Theory and Applications of Models of Computation, 2008

2007

Classes of representable disjoint NP-pairs.

Olaf Beyersdorff

Theor. Comput. Sci., 2007

2006

Disjoint NP-pairs and propositional proof systems.

Olaf Beyersdorff

PhD thesis, 2006

On the Deduction Theorem and Complete Disjoint NP-Pairs.

Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2006

2005

Tuples of Disjoint NP-Sets

Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2005

Disjoint NP-Pairs from Propositional Proof Systems

Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2005

2004

Representable Disjoint NP-Pairs

Olaf Beyersdorff

Electron. Colloquium Comput. Complex., 2004