Publications

• A simple proof of QBF hardness [pdf, 244 kb] de
  Olaf Beyersdorff, Joshua Blinkhorn
  Inf. Process. Lett. 168: 106093 (2021)
  
  
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution.
  Olaf Beyersdorff, Benjamin Böhm
  ITCS 2021: 12:1-12:20
  
  
• QBFFam: A Tool for Generating QBF Families from Proof Complexity [pdf, 276 kb] de.
  Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla
  SAT 2021: 21-29
  
  
• Building Strategies into QBF Proofs.
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
  J. Autom. Reason. 65(1): 125-154 (2021)

• Lower Bounds for QCDCL via Formula Gauge [pdf, 586 kb] de.
  Benjamin Böhm, Olaf Beyersdorff
  SAT 2021: 47-63
  
  
• Hard QBFs for Merge Resolution
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl and Gaurav Sood FSTTCS 2020, pages 12:1–12:15
  
  
• Frege Systems for Quantified Boolean Logic [pdf, 541 kb] deOlaf Beyersdorff, Ilario Bonacina, Leroy  Chew, Ján Pich
  Journal of the ACM April 2020 Article No.: 9
  
  
• Lower Bound Techniques for QBF Expansion
  Olaf Beyersdorff, Joshua Blinkhorn
  Theory Comput. Syst. 64(3): 400-421 (2020)
  
  
• Dynamic QBF Dependencies in Reduction and Expansion
  Olaf Beyersdorff, Joshua Blinkhorn
  ACM Trans. Comput. Log. 21(2): 8:1-8:27 (2020)
  
  
• Reasons for Hardness in QBF Proof Systems
  Olaf Beyersdorff, Luke Hinde, Ján Pich
  TOCT 12(2): 10:1-10:27 (2020)
  
  
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution [pdf, 713 kb] de
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
  LICS 2020: 209-223
  
  
• Olaf Beyersdorff, Joshua Blinkhorn, Tomás Peitl
  Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths.
  SAT 2020: 394-411

• Characterising tree-like Frege proofs for QBF [pdf, 309 kb] de
  Olaf Beyersdorff, Luke Hinde
  Inf. Comput. 268 (2019)
  
  
• Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF
  Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda
  Autom. Reasoning 63(3): 597-623 (2019)
  
  
• A Game Characterisation of Tree-like Q-resolution Size
  Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
  J. Comput. Syst. Sci. 104: 82-101 (2019)
  
  
• Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs
  Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
  Logical Methods in Computer Science 15(1) (2019)
  
  
• Short Proofs in QBF Expansion [pdf, 368 kb] de
  Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
  SAT2019: 19-35
  
  
• Proof Complexity of QBF Symmetry Recomputation [pdf, 277 kb] de
  Joshua Blinkhorn, Olaf Beyersdorff
  SAT 2019: 36-52
  
  
• Building Strategies into QBF Proofs
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
  STACS 2019: 14:1-14:18
  
  
• Understanding cutting planes for QBFs
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Inf. Comput., 262: 141-161, 2018.
  
  
• Genuine Lower Bounds for QBF Expansion
  Olaf Beyersdorff, Joshua Blinkhorn
  STACS, pages 12:1-15, 2018.
  
  
• Relating Size and Width in Variants of Q-Resolution [pdf, 207 kb] de
  Judith Clymo, Olaf Beyersdorff
  Inf. Process. Lett. (IPL), 138:1-6, 2018.
  
  
• Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs
  Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
  ITCS 2018, pages 9:1-18
  
  
• Reasons for Hardness in QBF Proof Systems
  Olaf Beyersdorff, Luke Hinde, Ján Pich
  FSTTCS, pages 14:1-15, 2017.
  
  
• Shortening QBF Proofs with Dependency Schemes [pdf, 316 kb] de
  Joshua Blinkhorn, Olaf Beyersdorff
  SAT, pages 263-280, 2017. Best paper award.
  
  
• Feasible Interpolation for QBF Resolution Calculi
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Logical Methods in Computer Science, 13(2), 2017.
  
  
• Understanding Cutting Planes for QBFs [pdf, 628 kb] de
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  FSTTCS, pages 40:1-15, 2016.
  
  
• Understanding Gentzen and Frege Systems for QBF
  Olaf Beyersdorff, Jan Pich
  LICS, pages 146-155, 2016.
  
  
• Dependency Schemes in QBF Calculi: Semantics and Soundness
  Olaf Beyersdorff, Joshua Blinkhorn
  CP, pages 96-112, 2016.
  
  
• Lifting QBF Resolution Calculi to DQBF [pdf, 303 kb] de
  Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
  SAT, pages 490-499, 2016.
  
  
• Are Short Proofs Narrow? QBF Resolution is not Simple [pdf, 444 kb] de
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  STACS, pages 15:1-14, 2016.
  
  
• Lower bounds: from circuits to QBF proof systems
  Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
  ITCS, pages 249-260, ACM, 2016.
  
  
• Extension Variables in QBF Resolution [pdf, 214 kb] de
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  AAAI-16 workshop on Beyond NP, 2016.
  
  
• Feasible Interpolation for QBF Resolution Calculi
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  ICALP, pages 180-192, 2015.
  
  
• Proof Complexity of Resolution-based QBF Calculi
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  STACS, pages 76-89, 2015.
  
  
• A Game Characterisation of Tree-like Q-resolution Size
  Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
  LATA, pages 486-498, 2015.
  
  
• On Unification of QBF Resolution-Based Calculi
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  MFCS, pages 81-93, 2014.
  
  
• Unified Characterisations of Resolution Hardness Measures
  Olaf Beyersdorff, Oliver Kullmann
  SAT, pages 170-187, 2014.
  
  
• Tableau vs. Sequent Calculi for Minimal Entailment
  Olaf Beyersdorff, Leroy Chew
  NMR, 2014.
  
  
• The Complexity of Theorem Proving in Circumscription and Minimal Entailment
  Olaf Beyersdorff, Leroy Chew
  IJCAR, pages 403-417, 2014.
  
  
• The Complexity of Theorem Proving in Autoepistemic Logic
  Olaf Beyersdorff
  SAT, pages 365-376, 2013.
  
  
• Parameterized Complexity of DPLL Search Procedures
  Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
  ACM Trans. Comput. Log. (TOCL), 14(3):20, 2013.
  A preliminary version appeared in
  SAT, pages 5-18, 2011. (nominated for the best paper award)
  
  
• A characterization of tree-like Resolution size
  Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
  Inf. Process. Lett. (IPL), 113(18):666-671, 2013.
  
  
• Verifying proofs in constant depth
  Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer
  ACM Transactions on Computation Theory (TOCT), 5(1):2, 2013.
  A preliminary version appeared in
  MFCS, pages 630-641, 2011.
  
  
• The complexity of reasoning for fragments of default logic
  Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer
  J. Log. Comput., 22(3):587-604, 2012.
  A preliminary version appeared in
  SAT, pages 51-64, 2009.
  
  
• Parameterized Bounded-Depth Frege Is not Optimal
  Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander A. Razborov
  ACM Transactions on Computation Theory (TOCT) , 4(3):7, 2012.
  Notable papers
  A preliminary version appeared in
  ICALP, pages 630-641, 2011.
  
  
• Proof complexity of propositional default logic
  Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, Heribert Vollmer
  Arch. Math. Log., 50(7-8):727-742, 2011.
  A preliminary version appeared in
  SAT, pages 30-43, 2010.
  
  
• Proof systems that take advice
  Olaf Beyersdorff, Johannes Köbler, Sebastian Müller
  Inf. Comput. , 209(3):320-332, 2011.
  Combined journal version of the conference papers
  Olaf Beyersdorff, Sebastian Müller
  Does Advice Help to Prove Propositional Tautologies?
  SAT, pages 65-72, 2009.
  Olaf Beyersdorff, Johannes Köbler, Sebastian Müller
  Nondeterministic Instance Complexity and Proof Systems with Advice
  LATA, pages 164-175, 2009.
  
  
• Model Checking CTL is Almost Always Inherently Sequential
  Olaf Beyersdorff, Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Heribert Vollmer
  Logical Methods in Computer Science, 7(2), 2011.
  A preliminary version appeared in
  TIME, pages 21-28, 2009.
  
  
• Do there exist complete sets for promise classes? [pdf, 370 kb] de
  Olaf Beyersdorff, Zenon Sadowski
  Math. Log. Q. (MLQ), 57(6):535-550, 2011.
  Combined journal version of the conference papers
  Olaf Beyersdorff, Zenon Sadowski
  Characterizing the Existence of Optimal Proof Systems and Complete Sets for Promise Classes
  CSR, pages 47-58, 2009.
  Olaf Beyersdorff
  On the Existence of Complete Disjoint NP-Pairs
  SYNASC, pages 282-289, 2009.
  
  
• A tight Karp-Lipton collapse result in bounded arithmetic [pdf, 291 kb] de
  Olaf Beyersdorff, Sebastian Müller
  ACM Trans. Comput. Log. (TOCL), 11(4), 2010.
  A preliminary version appeared in
  CSL, pages 199-214, 2008.
  
  
• 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. (IPL), 110(23):1074-1077, 2010.
  
  
• The Deduction Theorem for Strong Propositional Proof Systems
  Olaf Beyersdorff
  Theory Comput. Syst., 47(1):162-178, 2010.
  A preliminary version appeared in
  FSTTCS, pages 241-252, 2007.
  
  
• Comparing axiomatizations of free pseudospaces
  Olaf Beyersdorff
  Arch. Math. Log. (AML), 48(7):625-641, 2009.
  
  
• Edges as Nodes - a New Approach to Timetable Information
  Olaf Beyersdorff, Yevgen Nebesov
  ATMOS, 2009.
  
  
• The complexity of propositional implication
  Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer
  Inf. Process. Lett. (IPL) , 109(18):1071-1077, 2009.
  
  
• On the correspondence between arithmetic theories and propositional proof systems - a survey
  Olaf Beyersdorff
  Math. Log. Q. (MLQ) , 55(2):116-137, 2009.
  A preliminary version appeared as
  Logical Closure Properties of Propositional Proof Systems
  TAMC, pages 318-329, 2008.
  
  
• Nondeterministic functions and the existence of optimal proof systems
  Olaf Beyersdorff, Johannes Köbler, Jochen Messner
  Theor. Comput. Sci. (TCS), 410(38-40):3839-3855, 2009.
  
  
• Tuples of Disjoint NP-Sets
  Olaf Beyersdorff
  Theory Comput. Syst., 43(2):118-135, 2008.
  A preliminary version appeared in
  CSR, pages 80-91, 2006.
  
  
• Classes of representable disjoint NP-pairs
  Olaf Beyersdorff
  Theor. Comput. Sci. (TCS) , 377(1-3):93-109, 2007.
  Combined journal version of the conference papers
  Disjoint NP-Pairs from Propositional Proof Systems
  TAMC, pages 236-247, 2006.
  Representable Disjoint NP-Pairs
  FSTTCS, pages 122-134, 2004.

• Dynamic Dependency Awareness for QBF
  Joshua Blinkhorn, Olaf Beyersdorff
  IJCAI, pages 5224-5228, 2018.
  
  
• Proof Complexity of Non-classical Logics
  Olaf Beyersdorff
  TAMC , pages 15-27, 2010.
  
  
• Different Approaches to Proof Systems
  Olaf Beyersdorff, Sebastian Müller
  TAMC , pages 50-59, 2010.

Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference
Olaf Beyersdorff, Christoph M. Wintersteiger (editors),
SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Lecture Notes in Computer Science 10929, Springer 2018

• Quantified Boolean formulas [pdf, 638 kb] de
  Olaf Beyersdorff, Mikolas Janota, Florian Lonsing, and Martina Seidl In A. Biere, M. Heule, H. van Maaren, and T. Walsh, eds., Handbook of Satisfiability, 2nd edition, Frontiers in Artificial Intelligence and Applications. IOS press, to appear in 2021.
  
  
• Non-classical Aspects in Proof Complexity [pdf, 784 kb] de
  Olaf Beyersdorff
  Habilitation Thesis, Leibniz University Hanover, 2011
  Cuvillier Verlag, 2012.
  
  
• Proof Complexity of Non-classical Logics
  Olaf Beyersdorff, Oliver Kutz
  Lectures on Logic and Computation - ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011, Selected Lecture Notes , pages 1-54, Springer, 2012.
  
  
• Von der Turingmaschine zum Quantencomputer - ein Gang durch die Geschichte der Komplexitätstheorie [pdf, 848 kb] de
  Olaf Beyersdorff, Johannes Köbler
  In W. Reisig and J.-C. Freytag, eds., Informatik - Aktuelle Themen im historischen Kontext, pages 165-195, Springer, 2006.
  
  
• Disjoint NP-pairs and propositional proof systems
  Olaf Beyersdorff
  Dissertation, Humboldt University Berlin, 2006.