2017 seminar talk: Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness

Talk held by Hubie Chen (Birkbeck, University of London, UK) at the KGRC seminar on 2017-12-07.

Abstract

QBF is the problem of deciding truth/falsity of a quantified propositional formula (assumed to be in prenex CNF form). Recent years have seen focused efforts to understand how QBF can be solved in practice, and to develop theoretical underpinnings for such solving.

If one looks at typical proof systems for certifying QBF falsity, such as Q-resolution, a dilemma is encountered: lower bounds for Q-resolution are implied immediately by lower bounds for resolution, yet this says nothing about Q-resolution's ability to cope with quantifier alternation—and moreover clashes severely with the contemporary QBF view of SAT as “easy”. In this talk, we will discuss this dilemma and present a possible way to escape it.

In particular, we present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified propositional formulas. A key notion in this framework is that of proof system ensemble, which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called relaxing QU-res which is based on the established proof system QU-resolution. Our main technical results include an exponential separation of the tree-like and general versions of relaxing QU-res, and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity.

This talk will focus on a conceptual discussion of the work's motivation, the framework and the main definitions.

Bottom menu

Kurt Gödel Research Center for Mathematical Logic. Währinger Straße 25, 1090 Wien, Austria. Phone +43-1-4277-50501. Last updated: 2010-12-16, 04:37.