All reports by Author Olaf Beyersdorff:

__
TR18-172
| 11th October 2018
__

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan#### Building Strategies into QBF Proofs

__
TR18-102
| 15th May 2018
__

Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan#### Short Proofs in QBF Expansion

__
TR18-025
| 1st February 2018
__

Olaf Beyersdorff, Judith Clymo#### More on Size and Width in QBF Resolution

__
TR18-024
| 1st February 2018
__

Olaf Beyersdorff, Judith Clymo, Stefan Dantchev, Barnaby Martin#### The Riis Complexity Gap for QBF Resolution

__
TR17-137
| 11th September 2017
__

Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde#### Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

__
TR17-044
| 21st February 2017
__

Olaf Beyersdorff, Luke Hinde, Ján Pich#### Reasons for Hardness in QBF Proof Systems

Revisions: 1

__
TR17-037
| 25th February 2017
__

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla#### Understanding Cutting Planes for QBFs

__
TR17-032
| 17th February 2017
__

Olaf Beyersdorff, Joshua Blinkhorn#### Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds

__
TR16-048
| 11th March 2016
__

Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda#### Lifting QBF Resolution Calculi to DQBF

__
TR16-028
| 29th February 2016
__

Olaf Beyersdorff, Joshua Blinkhorn#### Dependency Schemes in QBF Calculi:Semantics and Soundness

Revisions: 1

__
TR16-011
| 27th January 2016
__

Olaf Beyersdorff, Ján Pich#### Understanding Gentzen and Frege systems for QBF

__
TR16-005
| 22nd January 2016
__

Olaf Beyersdorff, Leroy Chew, Mikolas Janota#### Extension Variables in QBF Resolution

__
TR15-152
| 16th September 2015
__

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla#### Are Short Proofs Narrow? QBF Resolution is not Simple.

__
TR15-133
| 12th August 2015
__

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew#### Lower bounds: from circuits to QBF proof systems

__
TR15-059
| 10th April 2015
__

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla#### Feasible Interpolation for QBF Resolution Calculi

__
TR14-131
| 7th October 2014
__

Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah#### A game characterisation of tree-like Q-Resolution size

__
TR14-120
| 16th September 2014
__

Olaf Beyersdorff, Leroy Chew, Mikolas Janota#### Proof Complexity of Resolution-based QBF Calculi

__
TR14-036
| 8th March 2014
__

Mikolas Janota, Leroy Chew, Olaf Beyersdorff#### On Unification of QBF Resolution-Based Calculi

Revisions: 1

__
TR14-032
| 8th March 2014
__

Olaf Beyersdorff, Leroy Chew#### Tableau vs. Sequent Calculi for Minimal Entailment

__
TR14-014
| 28th January 2014
__

Olaf Beyersdorff, Leroy Chew#### The Complexity of Theorem Proving in Circumscription and Minimal Entailment

__
TR13-016
| 17th January 2013
__

Olaf Beyersdorff#### The Complexity of Theorem Proving in Autoepistemic Logic

Revisions: 1

__
TR12-161
| 20th November 2012
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### A Characterization of Tree-Like Resolution Size

__
TR12-079
| 14th June 2012
__

Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer#### Verifying Proofs in Constant Depth

__
TR10-198
| 13th December 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander Razborov#### Parameterized Bounded-Depth Frege is Not Optimal

__
TR10-081
| 10th May 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### A Lower Bound for the Pigeonhole Principle in Tree-like Resolution by Asymmetric Prover-Delayer Games

__
TR10-059
| 8th April 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### Hardness of Parameterized Resolution

__
TR09-092
| 8th October 2009
__

Olaf Beyersdorff, Johannes Köbler, Sebastian Müller#### Proof Systems that Take Advice

__
TR09-081
| 27th August 2009
__

Olaf Beyersdorff, Zenon Sadowski#### Characterizing the Existence of Optimal Proof Systems and Complete Sets for Promise Classes

__
TR08-075
| 7th July 2008
__

Olaf Beyersdorff, Johannes Köbler, Sebastian Müller#### Nondeterministic Instance Complexity and Proof Systems with Advice

__
TR06-142
| 26th October 2006
__

Olaf Beyersdorff#### On the Deduction Theorem and Complete Disjoint NP-Pairs

__
TR05-123
| 25th October 2005
__

Olaf Beyersdorff#### Tuples of Disjoint NP-Sets

__
TR05-083
| 24th July 2005
__

Olaf Beyersdorff#### Disjoint NP-Pairs from Propositional Proof Systems

__
TR04-082
| 9th September 2004
__

Olaf Beyersdorff#### Representable Disjoint NP-Pairs

Revisions: 1

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan

Strategy extraction is of paramount importance for quantified Boolean formulas (QBF), both in solving and proof complexity. It extracts (counter)models for a QBF from a run of the solver resp. the proof of the QBF, thereby allowing to certify the solver's answer resp. establish soundness of the system. So far ... more >>>

Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan

For quantified Boolean formulas (QBF) there are two main different approaches to solving: QCDCL and expansion solving. In this paper we compare the underlying proof systems and show that expansion systems admit strictly shorter proofs than CDCL systems for formulas of bounded quantifier complexity, thus pointing towards potential advantages of ... more >>>

Olaf Beyersdorff, Judith Clymo

In their influential paper `Short proofs are narrow -- resolution made simple', Ben-Sasson and Wigderson introduced a crucial tool for proving lower bounds on the lengths of proofs in the resolution calculus. Over a decade later their technique for showing lower bounds on the size of proofs, by examining the ... more >>>

Olaf Beyersdorff, Judith Clymo, Stefan Dantchev, Barnaby Martin

We give an analogue of the Riis Complexity Gap Theorem for Quanti fied Boolean Formulas (QBFs). Every fi rst-order sentence $\phi$ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like Q-Resolution are either of polynomial size (if $\phi$ has no models) or at least ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde

As a natural extension of the SAT problem, different proof systems for quantified Boolean formulas (QBF) have been proposed. Many of these extend a propositional system to handle universal quantifiers.

By formalising the construction of the QBF proof system from a propositional proof system, by the addition of the ... more >>>

Olaf Beyersdorff, Luke Hinde, Ján Pich

We aim to understand inherent reasons for lower bounds for QBF proof systems and revisit and compare two previous approaches in this direction.

The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via strategy extraction (Beyersdorff & Pich, LICS'16). Here we ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

We define a cutting planes system CP+$\forall$red for quantified Boolean formulas (QBF) 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 ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn

We devise a new technique to prove lower bounds for the proof size in resolution-type calculi for quantified Boolean formulas (QBF). The new technique applies to the strong expansion system IR-calc and thereby also to the most studied QBF system Q-Resolution.

Our technique exploits a clear semantic paradigm, showing the ... more >>>

Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

We examine the 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 Q-Resolution < IR-calc < IRM-calc, the ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn

We study the parametrization of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use ... more >>>

Olaf Beyersdorff, Ján Pich

Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from Beyersdorff et al., denoted EF+$\forall$red, which is a ... more >>>

Olaf Beyersdorff, Leroy Chew, Mikolas Janota

We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Jussila et al. '07 who ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

The groundbreaking paper `Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in ... more >>>

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from ... more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF ... more >>>

Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah

We provide a characterisation for the size of proofs in tree-like Q-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives the first successful transfer of one of the lower bound techniques for classical proof systems to QBF ... more >>>

Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important

QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular

lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique ...
more >>>

Mikolas Janota, Leroy Chew, Olaf Beyersdorff

Several calculi for quantified Boolean formulas (QBFs) exist, but

relations between them are not yet fully understood.

This paper defines a novel calculus, which is resolution-based and

enables unification of the principal existing resolution-based QBF

calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based

calculus ...
more >>>

Olaf Beyersdorff, Leroy Chew

In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (J. Autom. Reasoning, 1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e., MLK p-simulates OTAB. The simulation is technically very involved ... more >>>

Olaf Beyersdorff, Leroy Chew

Circumscription is one of the main formalisms for non-monotonic reasoning. It uses reasoning with minimal models, the key idea being that minimal models have as few exceptions as possible. In this contribution we provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate ... more >>>

Olaf Beyersdorff

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 (ACM ToCL, 2002). We show that the calculus for credulous reasoning obeys almost ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

We explain an asymmetric Prover-Delayer game which precisely characterizes proof size in tree-like Resolution. This game was previously described in a parameterized complexity context to show lower bounds for parameterized formulas and for the classical pigeonhole principle. The main point of this note is to show that the asymmetric game ... more >>>

Olaf Beyersdorff, Samir Datta, Andreas Krebs, Meena Mahajan, Gido Scharfenberger-Fabian, Karteek Sreenivasaiah, Michael Thomas, Heribert Vollmer

In this paper we initiate the study of proof systems where verification of proofs proceeds by NC0 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 NC0 functions. Our results show that the answer ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander Razborov

A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that framework the parameterized version of any proof system is not fpt-bounded for some technical reasons, but we remark that this question becomes much more interesting if we restrict ourselves to those parameterized contradictions ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

In this note we show that the asymmetric Prover-Delayer game developed by Beyersdorff, Galesi, and Lauria (ECCC TR10-059) for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover-Delayer game to show a lower bound of the form $2^{\Omega(n\log n)}$ for the pigeonhole ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles.

We broadly investigate Parameterized Resolution obtaining the following ...
more >>>

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 (JSL 79), 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 Krajicek (JSL 07) have ...
more >>>

Olaf Beyersdorff, Zenon Sadowski

In this paper we investigate the following two questions:

Q1: Do there exist optimal proof systems for a given language L?

Q2: Do there exist complete problems for a given promise class C?

For concrete languages L (such as TAUT or SAT and concrete promise classes C (such as NP ... more >>>

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

Motivated by strong Karp-Lipton collapse results in bounded arithmetic, Cook and Krajicek have recently introduced the notion of propositional proof systems with advice.

In this paper we investigate the following question: Do there exist polynomially bounded proof systems with advice for arbitrary languages?

Depending on the complexity of the ...
more >>>

Olaf Beyersdorff

In this paper we ask the question whether the extended Frege proof

system EF satisfies a weak version of the deduction theorem. We

prove that if this is the case, then complete disjoint NP-pairs

exist. On the other hand, if EF is an optimal proof system, ...
more >>>

Olaf Beyersdorff

Disjoint NP-pairs are a well studied complexity theoretic concept with

important applications in cryptography and propositional proof

complexity.

In this paper we introduce a natural generalization of the notion of

disjoint NP-pairs to disjoint k-tuples of NP-sets for k>1.

We define subclasses of ...
more >>>

Olaf Beyersdorff

For a 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 the

previously defined canonical NP-pairs of these proof systems hard ...
more >>>

Olaf Beyersdorff

We investigate the class of disjoint NP-pairs under different reductions.

The structure of this class is intimately linked to the simulation order

of propositional proof systems, and we make use of the relationship between

propositional proof systems and theories of bounded arithmetic as the main

tool of our analysis.

more >>>