Publications

• A simple proof of QBF hardnesspdf, 244 kb · de
  Olaf Beyersdorff, Joshua Blinkhorn
  Inf. Process. Lett. 168: 106093 (2021)
  
  
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution.External link
  Olaf Beyersdorff, Benjamin Böhm
  ITCS 2021: 12:1-12:20
  
  
• 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)

• Lower Bounds for QCDCL via Formula Gaugepdf, 586 kb · de.
  Benjamin Böhm, Olaf Beyersdorff
  SAT 2021: 47-63
  
  
• 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 · deOlaf 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
  
  
• Building Strategies into QBF ProofsExternal link
  Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan
  STACS 2019: 14:1-14:18
  
  
• 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.

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, to appear in 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.