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

Mikolas Janota, Joao Marques-Silva

Over the years, proof systems for propositional satisfiability (SAT)

have been extensively studied. Recently, proof systems for

quantified Boolean formulas (QBFs) have also been gaining attention.

Q-resolution is a calculus enabling producing proofs from

DPLL-based QBF solvers. While DPLL has become a dominating technique

for SAT, QBF has been tackled ...
more >>>

Rahul Santhanam, Ryan Williams

We revisit the complexity of the satisfiability problem for quantified Boolean formulas. We show that satisfiability

of quantified CNFs of size $\poly(n)$ on $n$ variables with $O(1)$

quantifier blocks can be solved in time $2^{n-n^{\Omega(1)}}$ by zero-error

randomized algorithms. This is the first known improvement over brute force search in ...
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 >>>

Ryan Williams

We present an efficient proof system for Multipoint Arithmetic Circuit Evaluation: for every arithmetic circuit $C(x_1,\ldots,x_n)$ of size $s$ and degree $d$ over a field ${\mathbb F}$, and any inputs $a_1,\ldots,a_K \in {\mathbb F}^n$,

$\bullet$ the Prover sends the Verifier the values $C(a_1), \ldots, C(a_K) \in {\mathbb F}$ and ...
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, 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, 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, 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, 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, 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 >>>