Publications

• Computationally Hard Problems Are Hard for QBF Proof Systems Too.External link
  Agnes Schleitzer, Olaf Beyersdorff
  AAAI 2025: 11336-11344
  
  
• QCDCL with cube learning or pure literal elimination - What is best?External link
  Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
  Artif. Intell. 336: 104194 (2024). Preliminary version at IJCAI 2022: 1781-1787.
  
  
• QCDCL vs QBF Resolution: Further Insights.External link
  Benjamin Böhm, Olaf Beyersdorff
  J. Artif. Intell. Res. 81: 741-769 (2024). Preliminary version at SAT 2023: 4:1-4:17
  
  
• Should Decisions in QCDCL Follow Prefix Order?External link
  Benjamin Böhm, Tomás Peitl, Olaf Beyersdorff
  J. Autom. Reason. 68(1): 5 (2024). Preliminary version at SAT 2022: 11:1-11:19
  
  
• The Riis Complexity Gap for QBF Resolution.External link
  Olaf Beyersdorff, Judith Clymo, Stefan S. Dantchev, Barnaby Martin
  J. Satisf. Boolean Model. Comput. 15(1): 9-25 (2024)
  
  
• Proof Complexity of Propositional Model Counting.External link
  Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann
  J. Satisf. Boolean Model. Comput. 15(1): 27-59 (2024). Preliminary version at SAT 2023: 2:1-2:18
  
  
• Hard QBFs for Merge Resolution.
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood
  ACM Trans. Comput. Theory 16(2): 6:1-6:24 (2024). Preliminary version at FSTTCS 2020: 12:1-12:15
  
  
• Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths.
  Olaf Beyersdorff, Joshua Lewis Blinkhorn, Tomás Peitl
  ACM Trans. Comput. Theory 16(4): 22:1-22:25 (2024). Preliminary version at SAT 2020: 394-411
  
  
• Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs.External link
  Olaf Beyersdorff, Benjamin Böhm, Meena Mahajan
  AAAI 2024: 7943-7951
  
  
• Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree.External link
  Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, Luc Nicolas Spachmann
  MFCS 2024: 27:1-27:15
  
  
• The Relative Strength of #SAT Proof Systems.External link
  Olaf Beyersdorff, Johannes Klaus Fichte, Markus Hecher, Tim Hoffmann, Kaspar Kasche
  SAT 2024: 5:1-5:19
  
  
• Classes of Hard Formulas for QBF Resolution.External link
  Agnes Schleitzer, Olaf Beyersdorff
  J. Artif. Intell. Res. 77: 1455-1487 (2023). Preliminary version at SAT 2022: 5:1-5:18
  
  
• Lower Bounds for QCDCL via Formula Gauge.External link
  Benjamin Böhm, Olaf Beyersdorff
  J. Autom. Reason. 67(4): 35 (2023). Preliminary version at SAT 2021: 47-63
  
  
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution.External link
  Olaf Beyersdorff, Benjamin Böhm
  Log. Methods Comput. Sci. 19(2) (2023). Preliminary version at ITCS 2021: 12:1-12:20
  
  
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution.
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl
  ACM Trans. Comput. Log. 24(2): 10:1-10:30 (2023). Preliminary version at LICS 2020: 209-223
  
  
• Proof complexity of modal resolution.External link
  Sarah Sigley, Olaf Beyersdorff
  J. Autom. Reason. 66(1): 1–41 (2022).
  
  
• A simple proof of QBF hardnesspdf, 244 kb · de
  Olaf Beyersdorff, Joshua Blinkhorn
  Inf. Process. Lett. 168: 106093 (2021).
  
  
• QBFFam: A Tool for Generating QBF Families from Proof Complexitypdf, 276 kb · de.
  Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla
  SAT 2021: 21-29
  
  
• Building Strategies into QBF Proofs.External link
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
  J. Autom. Reason. 65(1): 125-154 (2021). Preliminary version at STACS 2019: 14:1-14:18

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

• Characterising tree-like Frege proofs for QBFpdf, 309 kb · de
  Olaf Beyersdorff, Luke Hinde
  Inf. Comput. 268 (2019)
  
  
• Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBFExternal link
  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 SizeExternal link
  Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
  J. Comput. Syst. Sci. 104: 82-101 (2019)
  
  
• Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFsExternal link
  Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
  Logical Methods in Computer Science 15(1) (2019)
  
  
• Short Proofs in QBF Expansionpdf, 368 kb · de
  Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
  SAT2019: 19-35
  
  
• Proof Complexity of QBF Symmetry Recomputationpdf, 277 kb · de
  Joshua Blinkhorn, Olaf Beyersdorff
  SAT 2019: 36-52
  
  
• Understanding cutting planes for QBFsExternal link
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Inf. Comput., 262: 141-161, 2018.
  
  
• Genuine Lower Bounds for QBF ExpansionExternal link
  Olaf Beyersdorff, Joshua Blinkhorn
  STACS, pages 12:1-15, 2018.
  
  
• Relating Size and Width in Variants of Q-Resolutionpdf, 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 QBFsExternal link
  Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
  ITCS 2018, pages 9:1-18
  
  
• Reasons for Hardness in QBF Proof SystemsExternal link
  Olaf Beyersdorff, Luke Hinde, Ján Pich
  FSTTCS, pages 14:1-15, 2017.
  
  
• Shortening QBF Proofs with Dependency Schemespdf, 316 kb · de
  Joshua Blinkhorn, Olaf Beyersdorff
  SAT, pages 263-280, 2017. Best paper award.
  
  
• Feasible Interpolation for QBF Resolution CalculiExternal link
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Logical Methods in Computer Science, 13(2), 2017.
  
  
• Understanding Cutting Planes for QBFspdf, 628 kb · de
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  FSTTCS, pages 40:1-15, 2016.
  
  
• Understanding Gentzen and Frege Systems for QBFExternal link
  Olaf Beyersdorff, Jan Pich
  LICSExternal link, pages 146-155, 2016.
  
  
• Dependency Schemes in QBF Calculi: Semantics and SoundnessExternal link
  Olaf Beyersdorff, Joshua Blinkhorn
  CP, pages 96-112, 2016.
  
  
• Lifting QBF Resolution Calculi to DQBFpdf, 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 Simplepdf, 444 kb · de
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  STACS, pages 15:1-14, 2016.
  
  
• Lower bounds: from circuits to QBF proof systemsExternal link
  Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
  ITCSExternal link, pages 249-260, ACM, 2016.
  
  
• Extension Variables in QBF Resolutionpdf, 214 kb · de
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  AAAI-16 workshop on Beyond NP, 2016.
  
  
• Feasible Interpolation for QBF Resolution CalculiExternal link
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  ICALP, pages 180-192, 2015.
  
  
• Proof Complexity of Resolution-based QBF CalculiExternal link
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  STACS, pages 76-89, 2015.
  
  
• A Game Characterisation of Tree-like Q-resolution SizeExternal link
  Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
  LATA, pages 486-498, 2015.
  
  
• On Unification of QBF Resolution-Based CalculiExternal link
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  MFCS, pages 81-93, 2014.
  
  
• Unified Characterisations of Resolution Hardness MeasuresExternal link
  Olaf Beyersdorff, Oliver Kullmann
  SAT, pages 170-187, 2014.
  
  
• Tableau vs. Sequent Calculi for Minimal EntailmentExternal link
  Olaf Beyersdorff, Leroy Chew
  NMR, 2014.
  
  
• The Complexity of Theorem Proving in Circumscription and Minimal EntailmentExternal link
  Olaf Beyersdorff, Leroy Chew
  IJCAR, pages 403-417, 2014.
  
  
• The Complexity of Theorem Proving in Autoepistemic LogicExternal link
  Olaf Beyersdorff
  SAT, pages 365-376, 2013.
  
  
• Parameterized Complexity of DPLL Search ProceduresExternal link
  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 sizeExternal link
  Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
  Inf. Process. Lett. (IPL), 113(18):666-671, 2013.
  
  
• Verifying proofs in constant depthExternal link
  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 logicExternal link
  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 OptimalExternal link
  Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander A. Razborov
  ACM Transactions on Computation Theory (TOCT) , 4(3):7, 2012.
  Notable papersExternal link
  A preliminary version appeared in
  ICALP, pages 630-641, 2011.
  
  
• Proof complexity of propositional default logicExternal link
  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 adviceExternal link
  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 SequentialExternal link
  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 arithmeticpdf, 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 gamesExternal link
  Olaf Beyersdorff, Nicola Galesi, Massimo Lauria
  Inf. Process. Lett. (IPL), 110(23):1074-1077, 2010.
  
  
• The Deduction Theorem for Strong Propositional Proof SystemsExternal link
  Olaf Beyersdorff
  Theory Comput. Syst., 47(1):162-178, 2010.
  A preliminary version appeared in
  FSTTCS, pages 241-252, 2007.
  
  
• Comparing axiomatizations of free pseudospacesExternal link
  Olaf Beyersdorff
  Arch. Math. Log. (AML), 48(7):625-641, 2009.
  
  
• Edges as Nodes - a New Approach to Timetable InformationExternal link
  Olaf Beyersdorff, Yevgen Nebesov
  ATMOS, 2009.
  
  
• The complexity of propositional implicationExternal link
  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 surveyExternal link
  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 systemsExternal link
  Olaf Beyersdorff, Johannes Köbler, Jochen Messner
  Theor. Comput. Sci. (TCS), 410(38-40):3839-3855, 2009.
  
  
• Tuples of Disjoint NP-SetsExternal link
  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-pairsExternal link
  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 QBFExternal link
  Joshua Blinkhorn, Olaf Beyersdorff
  IJCAI, pages 5224-5228, 2018.
  
  
• Proof Complexity of Non-classical LogicsExternal link
  Olaf Beyersdorff
  TAMC , pages 15-27, 2010.
  
  
• Different Approaches to Proof SystemsExternal link
  Olaf Beyersdorff, Sebastian Müller
  TAMC , pages 50-59, 2010.

• 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)External link
  Olaf Beyersdorff, Michal Pilipczuk, Elaine Pimentel, Kim Thang Nguyen (editors),
  STACS 2025, March 4-7, 2025, Jena, Germany. LIPIcs 327, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2025
  
  
• 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)External link
  Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, Daniel Lokshtanov (editors),
  STACS 2024, March 12-14, 2024, Clermont-Ferrand, France. LIPIcs 289, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024
  
  
• Mathematics for Computation (M4C)
  Marco Benini, Olaf Beyersdorff, Michael Rathjen, Peter Michael Schuster (editors),
  World Scientific Publishing Company Pte. Limited, 2023
  
  
• Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International ConferenceExternal link
  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 formulaspdf, 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, 2021.
  
  
• Non-classical Aspects in Proof Complexitypdf, 784 kb · de
  Olaf Beyersdorff
  Habilitation Thesis, Leibniz University Hanover, 2011
  Cuvillier Verlag, 2012.
  
  
• Proof Complexity of Non-classical LogicsExternal link
  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ätstheoriepdf, 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 systemsExternal link
  Olaf Beyersdorff
  Dissertation, Humboldt University Berlin, 2006.