- 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.