Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Leroy Chew:

TR18-102 | 15th May 2018
Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan

Short Proofs in QBF Expansion

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

TR17-037 | 25th February 2017
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Understanding Cutting Planes for QBFs

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

TR16-048 | 11th March 2016
Olaf Beyersdorff, Leroy Chew, Renate Schmidt, Martin Suda

Lifting QBF Resolution Calculi to DQBF

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

TR16-005 | 22nd January 2016
Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Extension Variables in QBF Resolution

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

TR15-152 | 16th September 2015
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Are Short Proofs Narrow? QBF Resolution is not Simple.

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

TR15-133 | 12th August 2015
Olaf Beyersdorff, Ilario Bonacina, Leroy Chew

Lower bounds: from circuits to QBF proof systems

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

TR15-059 | 10th April 2015
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

Feasible Interpolation for QBF Resolution Calculi

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

TR14-131 | 7th October 2014
Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah

A game characterisation of tree-like Q-Resolution size

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

TR14-120 | 16th September 2014
Olaf Beyersdorff, Leroy Chew, Mikolas Janota

Proof Complexity of Resolution-based QBF Calculi

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

TR14-036 | 8th March 2014
Mikolas Janota, Leroy Chew, Olaf Beyersdorff

On Unification of QBF Resolution-Based Calculi

Revisions: 1

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

TR14-032 | 8th March 2014
Olaf Beyersdorff, Leroy Chew

Tableau vs. Sequent Calculi for Minimal Entailment

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

TR14-014 | 28th January 2014
Olaf Beyersdorff, Leroy Chew

The Complexity of Theorem Proving in Circumscription and Minimal Entailment

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

ISSN 1433-8092 | Imprint