Ryan Williams

We prove a model-independent non-linear time lower bound for a slight generalization of the quantified Boolean formula problem (QBF). In particular, we give a reduction from arbitrary languages in alternating time t(n) to QBFs describable in O(t(n)) bits by a reasonable (polynomially) succinct encoding. The reduction works for many reasonable ... more >>>

Rahul Santhanam, Ryan Williams

We explore the relationships between circuit complexity, the complexity of generating circuits, and circuit-analysis algorithms. Our results can be roughly divided into three parts:

1. Lower Bounds Against Medium-Uniform Circuits. Informally, a circuit class is ``medium uniform'' if it can be generated by an algorithmic process that is somewhat complex ... more >>>

Albert Atserias, Sergi Oliva

Tree-width is a well-studied parameter of structures that measures their similarity to a tree. Many important NP-complete problems, such as Boolean satisfiability (SAT), are tractable on bounded tree-width instances. In this paper we focus on the canonical PSPACE-complete problem QBF, the fully-quantified version of SAT. It was shown by Pan ... 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 >>>

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

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

Mikolas Janota

Q-resolution and its variations provide the underlying proof

systems for the DPLL-based QBF solvers. While (long-distance) Q-resolution

models a conflict driven clause learning (CDCL) QBF solver, it is not

known whether the inverse is also true. This paper provides a negative

answer to this question. This contrasts with SAT solving, ...
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, 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, 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 >>>

Leroy Chew

Quantified Boolean Formulas (QBFs) extend propositional formulas with Boolean quantifiers. Working with QBF differs from propositional logic in its quantifier handling, but as propositional satisfiability (SAT) is a subproblem of QBF, all SAT hardness in solving and proof complexity transfers to QBF. This makes it difficult to analyse efforts dealing ... more >>>

Leroy Chew, Judith Clymo

In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial-time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a ... more >>>

Joshua Blinkhorn

Dependency quantified Boolean formulas (DQBF) describe an NEXPTIME-complete generalisation of QBF, which in turn generalises SAT. QRAT is a recently proposed proof system for quantified Boolean formulas (QBF), which simulates the full suite of QBF preprocessing techniques and thus forms a uniform proof checking format for solver verification.

In this ... more >>>

Leroy Chew, Marijn Heule

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, Gaurav Sood

We prove the first proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together ... more >>>

Sravanthi Chede, Anil Shukla

Merge Resolution (MRes [Beyersdorff et al. J. Autom. Reason.'2021] ) is a refutational proof system for quantified Boolean formulas (QBF). Each line of MRes consists of clauses with only existential literals, together with information of countermodels stored as merge maps. As a result, MRes has strategy extraction by design. The ... more >>>

Olaf Beyersdorff, Joshua Blinkhorn, Tomáš Peitl

We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new infinite collection of implication-free DQBF dependency schemes that generalise the reflexive resolution path dependency scheme. We establish soundness of all these schemes, implying that they can be ... more >>>

Leroy Chew, Friedrich Slivovsky

We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution.

These results are obtained by taking a technique ...
more >>>

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 and QU, and only one specific QBF family to separate Q and QU.

Here we provide a general method to construct hard formulas for Q and ... more >>>

Benjamin Böhm, Tomáš 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 ...
more >>>

Leroy Chew

The proof complexity of Quantified Boolean Formulas (QBF) relates to both QBF solving and OBF certification. One method to p-simulate a QBF proof system is by formalising the soundness of its strategy extraction in propositional logic. In this work we illustrate how to use extended QBF Frege to simulate LD-Q(Drrs)-Res, ... more >>>

Abhimanyu Choudhury, Meena Mahajan

We formalize the notion of proof systems obtained by adding normal dependency schemes into the QCDCL proof system underlying algorithms for solving Quantified Boolean Formulas, by exploring the addition of the dependency schemes via two approaches: one as a preprocessing tool, and second in propagation and learnings in the QCDCL ... more >>>

Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla

QBF proof systems are routinely adapted from propositional logic along with adjustments for the new quantifications. Existing are two main successful frameworks, the reduction and expansion frameworks, inspired by QCDCL [Zhang et al. ICCAD.'2002] and CEGAR solving [Janota et al. Artif. Intell.'2016] respectively. However, the reduction framework, while immensely useful ... more >>>

Olaf Beyersdorff, Kaspar Kasche, Luc Nicolas Spachmann

We initiate an in-depth proof-complexity analysis of polynomial calculus (Q-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of Q-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for Q-PC, similar in ... more >>>