Arrow Research search

Author name cluster

Olaf Beyersdorff

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

38 papers
2 author rows

Possible papers

38

AAAI Conference 2026 Conference Paper

Proof Systems for Tensor-based Model Counting

  • Olaf Beyersdorff
  • Joachim Giesen
  • Andreas Goral
  • Tim Hoffmann
  • Kaspar Kasche
  • Christoph Staudt

Solving the model counting problem #SAT, asking for the number of satisfying assignments of a propositional formula, has been explored intensively and has gathered its own community. While most existing solvers are based on knowledge compilation, another promising approach is through contraction in tensor hypernetworks. We perform a theoretical proof-complexity analysis of this approach. For this, we design two new tensor-based proof systems that we show to tightly correspond to tensor-based #SAT solving. We determine the simulation order of #SAT proof systems and prove exponential separations between the systems. This sheds light on the relative performance of different #SAT solving approaches.

PDF Details DOI

AAAI Conference 2026 Conference Paper

Proof Systems That Tightly Characterise Model Counting Algorithms

  • Olaf Beyersdorff
  • Tim Hoffmann
  • Kaspar Kasche

Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that: (i) with moderate adaptations, the conceptually quite different proof models of the dynamic system MICE and the static system of annotated Decision-DNNFs are equivalent and (ii) they tightly characterise state-of-the-art #SAT solving. Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting. We also propose new strengthenings of these proof systems that might lead to stronger model counters.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Computationally Hard Problems Are Hard for QBF Proof Systems Too

  • Agnes Schleitzer
  • Olaf Beyersdorff

There has been tremendous progress in the past decade in the field of quantified Boolean formulas (QBF), both in practical solving as well as in creating a theory of corresponding proof systems and their proof complexity analysis. Both for solving and for proof complexity, it is important to have interesting formula families on which we can test solvers and gauge the strength of the proof systems. There are currently few such formula families in the literature. We initiate a general programme how to transform computationally hard problems (located in the polynomial hierarchy) into QBFs hard for the main QBF resolution systems Q-Res and QU-Res that relate to core QBF solvers. We illustrate this general approach on three problems from graph theory and logic. This yields QBF families that are provably hard for Q-Res and QU-Res (without any complexity assumptions).

PDF Details DOI

NeurIPS Conference 2025 Conference Paper

Exploiting Dynamic Sparsity in Einsum

  • Christoph Staudt
  • Mark Blacher
  • Tim Hoffmann
  • Lea Kasche
  • Olaf Beyersdorff
  • Joachim Giesen

Einsum expressions specify an output tensor in terms of several input tensors. They offer a simple yet expressive abstraction for many computational tasks in artificial intelligence and beyond. However, evaluating einsum expressions poses hard algorithmic problems that depend on the representation of the tensors. Two popular representations are multidimensional arrays and coordinate lists. The latter is a more compact representation for sparse tensors, that is, tensors where a significant proportion of the entries are zero. So far, however, most of the popular einsum implementations use the multidimensional array representation for tensors. Here, we show on a non-trivial example that, when evaluating einsum expressions, coordinate lists can be exponentially more efficient than multidimensional arrays. In practice, however, coordinate lists can also be significantly less efficient than multidimensional arrays, but it is hard to decide from the input tensors whether this will be the case. Sparsity evolves dynamically in intermediate tensors during the evaluation of an einsum expression. Therefore, we introduce a hybrid solution where the representation is switched on the fly from multidimensional arrays to coordinate lists depending on the sparsity of the remaining tensors. In our experiments on established benchmark einsum expressions, the hybrid solution is consistently competitive with or outperforms the better of the two static representations.

PDF Details

SAT Conference 2025 Conference Paper

Semi-Algebraic Proof Systems for QBF

  • Olaf Beyersdorff
  • Ilario Bonacina
  • Kaspar Kasche
  • Meena Mahajan
  • Luc Nicolas Spachmann

We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We transfer to this setting techniques both from the QBF literature (strategy extraction) and from propositional proof complexity (size-degree relations and pseudo-expectation). We obtain a number of strong QBF lower bounds and separations between these systems, even when disregarding propositional hardness.

Details

MFCS Conference 2024 Conference Paper

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

  • Olaf Beyersdorff
  • Tim Hoffmann
  • Kaspar Kasche
  • Luc Nicolas Spachmann

We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999). We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields.

Details

JAIR Journal 2024 Journal Article

QCDCL vs QBF Resolution: Further Insights

  • Benjamin Böhm
  • Olaf Beyersdorff

We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants – parameterised by different policies for decisions, unit propagations and reductions – lead to incomparable systems for almost all choices of these policies.

PDF Details DOI

AIJ Journal 2024 Journal Article

QCDCL with cube learning or pure literal elimination – What is best?

  • Benjamin Böhm
  • Tomáš Peitl
  • Olaf Beyersdorff

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving variants via proof complexity techniques. Our results show that almost all of the QCDCL variants are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.

Details DOI

AAAI Conference 2024 Conference Paper

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

  • Olaf Beyersdorff
  • Benjamin Böhm
  • Meena Mahajan

Conflict-driven clause learning (CDCL) is the dominating algorithmic paradigm for SAT solving and hugely successful in practice. In its lifted version QCDCL, it is one of the main approaches for solving quantified Boolean formulas (QBF). In both SAT and QBF, proofs can be efficiently extracted from runs of (Q)CDCL solvers. While for CDCL, it is known that the proof size in the underlying proof system propositional resolution matches the CDCL runtime up to a polynomial factor, we show that in QBF there is an exponential gap between QCDCL runtime and the size of the extracted proofs in QBF resolution systems. We demonstrate that this is not just a gap between QCDCL runtime and the size of any QBF resolution proof, but even the extracted proofs are exponentially smaller for some instances. Hence searching for a small proof via QCDCL (even with non-deterministic decision policies) will provably incur an exponential overhead for some instances.

PDF Details DOI

SAT Conference 2024 Conference Paper

The Relative Strength of #SAT Proof Systems

  • Olaf Beyersdorff
  • Johannes Klaus Fichte
  • Markus Hecher
  • Tim Hoffmann
  • Kaspar Kasche

The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.

Details

JAIR Journal 2023 Journal Article

Classes of Hard Formulas for QBF Resolution

  • Agnes Schleitzer
  • Olaf Beyersdorff

To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q-Res and QU-Res, and only one specific QBF family to separate Q-Res and QU-Res. Here we provide a general method to construct hard formulas for Q-Res and QU-Res. The construction uses simple propositional formulas (e.g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Σb2 formulas without constant winning strategies). This leads to a host of new hard formulas, including new classes of hard random QBFs. We further present generic constructions for formulas separating Q-Res and QU-Res, and for separating Q-Res and LD-Q-Res.

PDF Details DOI

SAT Conference 2023 Conference Paper

Proof Complexity of Propositional Model Counting

  • Olaf Beyersdorff
  • Tim Hoffmann
  • Luc Nicolas Spachmann

Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT'22). As demonstrated by Fichte et al. , the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE' that is polynomially equivalent to MICE. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs.

Details

SAT Conference 2023 Conference Paper

QCDCL vs QBF Resolution: Further Insights

  • Benjamin Böhm 0001
  • Olaf Beyersdorff

We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions - lead to incomparable systems for almost all choices of these policies.

Details

SAT Conference 2022 Conference Paper

Classes of Hard Formulas for QBF Resolution

  • Agnes Schleitzer
  • Olaf Beyersdorff

To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q-Res and QU-Res, and only one specific QBF family to separate Q-Res and QU-Res. Here we provide a general method to construct hard formulas for Q-Res and QU-Res. The construction uses simple propositional formulas (e. g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Σ₂^b formulas without constant winning strategies). This leads to a host of new hard formulas, including new classes of hard random QBFs. We further present generic constructions for formulas separating Q-Res and QU-Res, and for separating Q-Res and LD-Q-Res.

Details

IJCAI Conference 2022 Conference Paper

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

  • Benjamin Böhm
  • Tomáš Peitl
  • Olaf Beyersdorff

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of the QCDCL models are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.

PDF Details DOI

SAT Conference 2022 Conference Paper

Should Decisions in QCDCL Follow Prefix Order?

  • Benjamin Böhm 0001
  • Tomás Peitl
  • Olaf Beyersdorff

Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions. We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system QCDCL^ANY is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses (QCDCL^UNI-ANI) and asserting cubes (QCDCL^EXI-ANY), respectively. We model all four approaches by formal proof systems and show that QCDCL^UNI-ANY is exponentially better than QCDCL on false formulas, whereas QCDCL^EXI-ANY is exponentially better than QCDCL on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems. We complement our theoretical study with some initial experiments that confirm our theoretical findings.

Details

SAT Conference 2021 Conference Paper

Lower Bounds for QCDCL via Formula Gauge

  • Benjamin Böhm 0001
  • Olaf Beyersdorff

Abstract QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). We design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call gauge. We show that for a large class of QBFs, large (e. g. linear) gauge implies exponential lower bounds for QCDCL proof size. We illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL.

Details

SAT Conference 2021 Conference Paper

QBFFam: A Tool for Generating QBF Families from Proof Complexity

  • Olaf Beyersdorff
  • Luca Pulina
  • Martina Seidl
  • Ankit Shukla 0003

Abstract We present QBFFam, a tool for the generation of formula families originating from the field of proof complexity. Such formula families are used to investigate the strength of proof systems and to show how they relate to each other in terms of simulations and separations. Furthermore, these proof systems underlie the reasoning power of QBF solvers. With our tool, it is possible to generate informative and scalable benchmarks that help to analyse the behavior of solvers. As we will see in this paper, runtime behavior predicted by proof complexity is indeed reflected by recent solver implementations.

Details

SAT Conference 2020 Conference Paper

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

  • Olaf Beyersdorff
  • Joshua Blinkhorn
  • Tomás Peitl

Abstract We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any DQBF proof system. We further explore the power of DQBF resolution systems parameterised by dependency schemes and show that our new scheme results in exponentially shorter proofs in comparison to the reflexive resolution path dependency scheme when used in the expansion DQBF system \(\mathsf {\forall {Exp{\text{+ }}Res}}\). On QBFs, we demonstrate that our new scheme is exponentially stronger than the reflexive resolution path dependency scheme when used in Q-resolution, thus resulting in the strongest QBF dependency scheme known to date.

Details

I&C Journal 2019 Journal Article

Characterising tree-like Frege proofs for QBF

  • Olaf Beyersdorff
  • Luke Hinde

We examine the tree-like versions of QBF Frege and extended Frege systems. While in the propositional setting, tree-like and dag-like Frege are equivalent, we show that this is not the case for QBF Frege, where tree-like systems are exponentially weaker. This applies to the version of QBF Frege where the universal reduction rule substitutes universal variables by 0/1 constants. To show lower bounds for tree-like QBF Frege we devise a general technique that provides lower bounds for all tree-like QBF systems of the form P+∀red, where P is a propositional system. The lower bound is based on the semantic measure of strategy size corresponding to the size of countermodels for false QBFs. We also obtain a full characterisation of hardness for tree-like QBF Frege. Lower bounds for this system either arise from a lower bound to propositional Frege, from a circuit lower bound, or from a lower bound to strategy size.

Details DOI

SAT Conference 2019 Conference Paper

Proof Complexity of QBF Symmetry Recomputation

  • Joshua Blinkhorn
  • Olaf Beyersdorff

Abstract For quantified Boolean formulas (QBF), a resolution system with a symmetry rule was recently introduced by Kauers and Seidl (Inf. Process. Lett. 2018). In this system, many formulas hard for QBF resolution admit short proofs. Kauers and Seidl apply the symmetry rule on symmetries of the original formula. Here we propose a new formalism where symmetries are dynamically recomputed during the proof on restrictions of the original QBF. This presents a theoretical model for the potential use of symmetry recomputation as an inprocessing rule in QCDCL solving. We demonstrate the power of symmetry recomputation by proving an exponential separation between Q-resolution with the symmetry rule and Q-resolution with our new symmetry recomputation rule. In fact, we show that bounding the number of symmetry recomputations gives rise to a hierarchy of QBF resolution systems of strictly increasing strength.

Details

SAT Conference 2019 Conference Paper

Short Proofs in QBF Expansion

  • Olaf Beyersdorff
  • Leroy Chew
  • Judith Clymo
  • Meena Mahajan

Abstract For quantified Boolean formulas (QBF) there are two main different approaches to solving: conflict-driven clause learning (QCDCL) and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than QCDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of expansion solving techniques over QCDCL solving. Our first result shows that tree-like expansion systems allow short proofs of QBFs that are a source of hardness for QCDCL, i. e. tree-like \(\forall \textsf {Exp{+}Res}\) is strictly stronger than tree-like Q-Resolution. In our second result we efficiently transform dag-like Q-Resolution proofs of QBFs with bounded quantifier complexity into \(\forall \textsf {Exp{+}Res}\) proofs. This is theoretical confirmation of experimental findings by Lonsing and Egly, who observed that expansion QBF solvers often outperform QCDCL solvers on instances with few quantifier alternations.

Details

IJCAI Conference 2018 Conference Paper

Dynamic Dependency Awareness for QBF

  • Joshua Blinkhorn
  • Olaf Beyersdorff

We provide the first proof complexity results for QBF dependency calculi. By showing that the reflexive resolution path dependency scheme admits exponentially shorter Q-resolution proofs on a known family of instances, we answer a question first posed by Slivovsky and Szeider (SAT 2014). Further, we introduce a new calculus in which a dependency scheme is applied dynamically. We demonstrate the further potential of this approach beyond that of the existing static system with an exponential separation.

PDF Details

I&C Journal 2018 Journal Article

Understanding cutting planes for QBFs

  • Olaf Beyersdorff
  • Leroy Chew
  • Meena Mahajan
  • Anil Shukla

We study the cutting planes system CP+∀red for quantified Boolean formulas (QBF), obtained by augmenting propositional Cutting Planes with a universal reduction rule, and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+∀red is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ∀Exp+Res. A similar picture holds for a semantic version semCP+∀red. Technically, our results establish the effectiveness of two lower bound techniques for CP+∀red: via strategy extraction and via monotone feasible interpolation.

Details DOI

SAT Conference 2017 Conference Paper

Shortening QBF Proofs with Dependency Schemes

  • Joshua Blinkhorn
  • Olaf Beyersdorff

Abstract We provide the first proof complexity results for QBF dependency calculi. By showing that the reflexive resolution path dependency scheme admits exponentially shorter Q-resolution proofs on a known family of instances, we answer a question first posed by Slivovsky and Szeider in 2014 [ 30 ]. Further, we conceive a method of QBF solving in which dependency recomputation is utilised as a form of inprocessing. Formalising this notion, we introduce a new calculus in which a dependency scheme is applied dynamically. We demonstrate the further potential of this approach beyond that of the existing static system with an exponential separation.

Details

SAT Conference 2016 Conference Paper

Lifting QBF Resolution Calculi to DQBF

  • Olaf Beyersdorff
  • Leroy Chew
  • Renate A. Schmidt
  • Martin Suda 0001

Abstract We examine existing resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems \(\textsf {Q-Res}< \textsf {IR-calc} < \textsf {IRM-calc} \), the situation is quite different in DQBF. The obvious adaptations of Q-Res and likewise universal resolution are too weak: they are not complete. The obvious adaptation of IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance resolution. Conceptually, we use the relation of DQBF to effectively propositional logic ( EPR ) and explain our new DQBF calculus based on IR-calc as a subsystem of first-order resolution.

Details

SAT Conference 2014 Conference Paper

Unified Characterisations of Resolution Hardness Measures

  • Olaf Beyersdorff
  • Oliver Kullmann

Abstract Various “hardness” measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size of resolution proofs. Our main contribution is a unified game-theoretic characterisation of these measures. As consequences we obtain new relations between the different hardness measures. In particular, we prove a generalised version of Atserias and Dalmau’s result on the relation between resolution width and space from [5].

Details

SAT Conference 2013 Conference Paper

The Complexity of Theorem Proving in Autoepistemic Logic

  • Olaf Beyersdorff

Abstract Autoepistemic logic is one of the most successful formalisms for nonmonotonic reasoning. In this paper we provide a proof-theoretic analysis of sequent calculi for credulous and sceptical reasoning in propositional autoepistemic logic, introduced by Bonatti and Olivetti [5]. We show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen’s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. This contrasts with the situation in sceptical autoepistemic reasoning where we obtain an exponential lower bound to the proof length in Bonatti and Olivetti’s calculus.

Details

SAT Conference 2011 Conference Paper

Parameterized Complexity of DPLL Search Procedures

  • Olaf Beyersdorff
  • Nicola Galesi
  • Massimo Lauria

Abstract We study the performance of DPLL algorithms on parameterized problems. In particular, we investigate how difficult it is to decide whether small solutions exist for satisfiability and other combinatorial problems. For this purpose we develop a Prover-Delayer game which models the running time of DPLL procedures and we establish an information-theoretic method to obtain lower bounds to the running time of parameterized DPLL procedures. We illustrate this technique by showing lower bounds to the parameterized pigeonhole principle and to the ordering principle. As our main application we study the DPLL procedure for the problem of deciding whether a graph has a small clique. We show that proving the absence of a k -clique requires n Ω( k ) steps for a non-trivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked in [11] of understanding the Resolution complexity of this family of formulas.

Details

I&C Journal 2011 Journal Article

Proof systems that take advice

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

One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [J. Symbolic Logic, 1979], where they defined propositional proof systems as poly-time computable functions which have all propositional tautologies as their range. Motivated by provability consequences in bounded arithmetic, Cook and Krajı´ček [J. Symbolic Logic, 2007] have recently started the investigation of proof systems which are computed by poly-time functions using advice. In this paper we concentrate on three fundamental questions regarding this new model. First, we investigate whether a given language L admits a polynomially bounded proof system with advice. Depending on the complexity of the underlying language L and the amount and type of the advice used by the proof system, we obtain different characterizations for this problem. In particular, we show that this question is tightly linked with the question whether L has small nondeterministic instance complexity. The second question concerns the existence of optimal proof systems with advice. For propositional proof systems, Cook and Krajı´ček gave a surprising positive answer which we extend to all languages. These results show that providing proof systems with advice yields a more powerful model, but this model is also less directly applicable in practice. Our third question therefore asks whether the usage of advice in propositional proof systems can be simplified or even eliminated. While in principle, the advice can be very complex, we show that propositional proof systems with logarithmic advice are also computable in poly-time with access to a sparse NP-oracle. Employing a recent technique of Buhrman and Hitchcock [CCC, 2008] we also manage to transfer the advice from the proof to the proven formula, which leads to a more practical computational model.

Details DOI

MFCS Conference 2011 Conference Paper

Verifying Proofs in Constant Depth

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

Abstract In this paper we initiate the study of proof systems where verification of proofs proceeds by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages can be enumerated by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) functions. Our results show that the answer to this problem is not determined by the complexity of the language. On the one hand, we construct \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for a variety of languages ranging from regular to \(\protect{\ensuremath{\mathsf{NP}}}\) -complete. On the other hand, we show by combinatorial methods that even easy regular languages such as Exact-OR do not admit \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems. We also present a general construction of \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for regular languages with strongly connected NFA’s.

Details

SAT Conference 2010 Conference Paper

Proof Complexity of Propositional Default Logic

  • Olaf Beyersdorff
  • Arne Meier
  • Sebastian Müller 0003
  • Michael Thomas 0001
  • Heribert Vollmer

Abstract Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen’s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti’s enhanced calculus for skeptical default reasoning.

Details

SAT Conference 2009 Conference Paper

Does Advice Help to Prove Propositional Tautologies?

  • Olaf Beyersdorff
  • Sebastian Müller 0003

Abstract One of the starting points of propositional proof complexity is the seminal paper by Cook and Reckhow [6], where they defined propositional proof systems as poly-time computable functions which have all propositional tautologies as their range. Motivated by provability consequences in bounded arithmetic, Cook and Krajíček [5] have recently started the investigation of proof systems which are computed by poly-time functions using advice. While this yields a more powerful model, it is also less directly applicable in practice. In this note we investigate the question whether the usage of advice in propositional proof systems can be simplified or even eliminated. While in principle, the advice can be very complex, we show that proof systems with logarithmic advice are also computable in poly-time with access to a sparse NP -oracle. In addition, we show that if advice is ”not very helpful” for proving tautologies, then there exists an optimal propositional proof system without advice. In our main result, we prove that advice can be transferred from the proof to the formula, leading to an easier computational model. We obtain this result by employing a recent technique by Buhrman and Hitchcock [4].

Details

TIME Conference 2009 Conference Paper

Model Checking CTL is Almost Always Inherently Sequential

  • Olaf Beyersdorff
  • Arne Meier
  • Michael Thomas 0001
  • Heribert Vollmer
  • Martin Mundhenk
  • Thomas Schneider 0002

The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of negations---restrictions already studied for LTL by Sistla and Clarke (1985) and Markey (2004). For all these fragments, except for the trivial case without any temporal operator, we systematically prove model checking to be either inherently sequential (P-complete) or very efficiently parallelizable (LOGCFL-complete). For most fragments, however, model checking for CTL is already P-complete. Hence our results indicate that in most applications, approaching CTL model checking by parallelism will not result in the desired speed up. We also completely determine the complexity of the model checking problem for all fragments of the extensions ECTL, CTL+, and ECTL+.

Details

TCS Journal 2009 Journal Article

Nondeterministic functions and the existence of optimal proof systems

  • Olaf Beyersdorff
  • Johannes Köbler
  • Jochen Messner

We provide new characterizations of two previously studied questions on nondeterministic function classes: Q1: Do nondeterministic functions admit efficient deterministic refinements? Q2: Do nondeterministic function classes contain complete functions? We show that Q1 for the class NPMV t is equivalent to the question whether the standard proof system for SAT is p-optimal, and to the assumption that every optimal proof system is p-optimal. Assuming only the existence of a p-optimal proof system for SAT, we show that every set with an optimal proof system has a p-optimal proof system. Under the latter assumption, we also obtain a positive answer to Q2 for the class NPMV t. An alternative view on nondeterministic functions is provided by disjoint sets and tuples. We pursue this approach for disjoint NP -pairs and its generalizations to tuples of sets from NP and co NP with disjointness conditions of varying strength. In this way, we obtain new characterizations of Q2 for the class NPSV. Question Q1 for NPSV is equivalent to the question of whether every disjoint NP -pair is easy to separate. In addition, we characterize this problem by the question of whether every propositional proof system has the effective interpolation property. Again, these interpolation properties are intimately connected to disjoint NP -pairs, and we show how different interpolation properties can be modeled by NP -pairs associated with the underlying proof system.

Details DOI

SAT Conference 2009 Conference Paper

The Complexity of Reasoning for Fragments of Default Logic

  • Olaf Beyersdorff
  • Arne Meier
  • Michael Thomas 0001
  • Heribert Vollmer

Abstract Default logic was introduced by Reiter in 1980. In 1992, Gottlob classified the complexity of the extension existence problem for propositional default logic as \(\Sigma^{\rm P}_2\) -complete, and the complexity of the credulous and skeptical reasoning problem as \(\Sigma^{\rm P}_2\) -complete, resp. \(\Pi^{\rm P}_2\) -complete. Additionally, he investigated restrictions on the default rules, i. e. , semi-normal default rules. Selman made in 1992 a similar approach with disjunction-free and unary default rules. In this paper we systematically restrict the set of allowed propositional connectives. We give a complete complexity classification for all sets of Boolean functions in the meaning of Post’s lattice for all three common decision problems for propositional default logic. We show that the complexity is a trichotomy ( \(\Sigma^{\rm P}_2\) -, NP-complete, trivial) for the extension existence problem, whereas for the credulous and sceptical reasoning problem we get a finer classification down to NL-complete cases.

Details

CSL Conference 2008 Conference Paper

A Tight Karp-Lipton Collapse Result in Bounded Arithmetic

  • Olaf Beyersdorff
  • Sebastian Müller 0003

Abstract Cook and Krajíček [9] have obtained the following Karp-Lipton result in bounded arithmetic: if the theory proves, then collapses to, and this collapse is provable in. Here we show the converse implication, thus answering an open question from [9]. We obtain this result by formalizing in a hard/easy argument of Buhrman, Chang, and Fortnow [3]. In addition, we continue the investigation of propositional proof systems using advice, initiated by Cook and Krajíček [9]. In particular, we obtain several optimal and even p-optimal proof systems using advice. We further show that these p-optimal systems are equivalent to natural extensions of Frege systems.

Details

TCS Journal 2007 Journal Article

Classes of representable disjoint NP-pairs

  • Olaf Beyersdorff

For a propositional proof system P we introduce the complexity class DNPP ( P ) of all disjoint NP -pairs for which the disjointness of the pair is efficiently provable in the proof system P. We exhibit structural properties of proof systems which make canonical NP -pairs associated with these proof systems hard or complete for DNPP ( P ). Moreover, we demonstrate that non-equivalent proof systems can have equivalent canonical pairs and that depending on the properties of the proof systems different scenarios for DNPP ( P ) and the reductions between the canonical pairs exist.

Details DOI
v2026.09.13