next day
all days

View: session overviewtalk overviewside by side with other conferences

10:15-10:45Coffee Break
10:45-12:00 Session 16A: PC Opening and Invited Talk (Pavel Pudlak)
Location: FH, Seminarraum 101B
On Some Conjectures in Proof Complexity
SPEAKER: Pavel Pudlák

ABSTRACT. Our aim is to study conjectures that are somehow connected with consistency and/or incompleteness of first order theories. We want to fully understand (1) how far we can go by considering stronger and stronger conjectures and (2) whether the system of conjectures splits into incomparable ones or there there are always stronger unifying conjectures. Currently the conjectures that we have can be classified into two levels - uniform and nonunifom, and two directions - universal and existential. We still hope to be able to find a stronger unifying conjecture.

12:00-13:00 Session 17B: Contributed Talks: SAT and QBF
Location: FH, Seminarraum 101B
Size-Space Bounds and Trade-offs for CDCL Proofs
SPEAKER: Marc Vinyals

ABSTRACT. A long line of research has shown that conflict-driven clause learning viewed as a proof system can polynomially simulate resolution. We give a more explicit description of this CDCL proof system, which allows us to define proof size and space in a natural way and also capture aspects such as clause learning schemes and restart policies. This in turn makes it possible to study which upper and lower bounds on size, space and size-space trade-offs in general resolution carry over to proofs actually realizable by CDCL solvers.

Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction
SPEAKER: Hubie Chen

ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.

13:00-14:30Lunch Break
14:30-15:30 Session 18A: Invited Talk (Jakob Nordström)
Location: FH, Seminarraum 101B
A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity

ABSTRACT. This presentation is intended as a survey of results on proof space and time-space trade-offs in proof complexity. We will try to provide some proof sketches to give a flavour of the proof methods used, but also explain the limitations of current techniques and state some tantalising problems that remain open.

15:30-16:00 Session 19: Contributed Talk: Polynomial Calculus
Location: FH, Seminarraum 101B
Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
SPEAKER: Marc Vinyals

ABSTRACT. Recently, an active line of research has been into the space complexity of proofs. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PC space. This yields formulas that exhibiting a degree-space separation similar to what is known for resolution. Using related ideas, we show that Tseitin formulas over random 4-regular graphs almost surely require space at least Ω(√n).

Our proofs use techniques from [Bonacina-Galesi '13]. Our final contribution, however, is to show that these techniques cannot yield non-constant space lower bounds for the functional pigeonhole principle, which is conjectured to be hard for PC space.

16:00-16:30Coffee Break
16:30-18:00 Session 20A: Contributed Talks: Bounded Arithmetic
Location: FH, Seminarraum 101B
Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time

ABSTRACT. In bounded arithmetic, a host of theories have been developed which correspond to complexity classes within the polynomial
hierarchy and below polynomial-time. Recent research has tried to characterize the provably total NP search problems
in such theories, where a total NP search problem is provably total in a theory T if it can be formalized in the language of T, and T can prove that, for each instance, there exists a solution to the search problem. For example, Buss and Krajcek showed that the class of provably total NP search problems in a certain bounded arithmetic theory (denoted T12 or  TV1) is characterized by PLS. Further characterizations for theories above T12 were later discovered. To the best of our knowledge, no such characterizations are known for the theories below T12 until this work.

Given a class S of provably total NP search problems for some theory, the general aim of our research project is to identify some specific provably total NP search problem class (usually defined via some specific combinatorial principle) which is complete within S under AC0-many-one reduction; completeness should be proven using AC0-reasoning only, i.e. formalizable in V0. For example, it was shown by Cook and Nguyen that PLS, where the neighborhood function and the initial point are given by AC0-functions, is complete in the above sense for the class of provably total NP search problems in T12.

For the theory related to polynomial-time, we identify the search problem class Inflationary Iteration (IITER) which serves our above described aim. A function F (defined on finite strings) is inflationary if X is a subset of F(X) (under the natural identification of strings with finite sets). An IITER principle is defined as a special case of the iteration principle, in which the iterated function has to be AC0-computable and inflationary.

Cook and Nguyen have a generic way of defining a bounded arithmetic theory VC for complexity classes C below polynomial-time. For such theory VC, we define a search problem class KPT[C] which serves our above described aim. These problems are based on a version of Herbrand's theorem proven by Krajicek, Pudlak and Takeuti.

Parameter-free induction in bounded arithmetic

ABSTRACT. In the area of strong fragments of Peano Arithmetic, it proved fruitful to study not just the usual induction fragments IΣi, but also fragments axiomatized by parameter-free induction schemata, and theories axiomatized using the closely related induction inference rules.

In contrast, induction rules and parameter-free schemata have been largely ignored in bounded arithmetic literature. Apart from IEi- briefly discussed by Kaye (1990), the corresponding fragments of Buss's S2 were only studied by Bloch (1992) and Cordon-Franco et al. (2009). Many basic questions about these fragments were disregarded, in particular, neither paper even mentions Πbi-induction rules and parameter-free schemata, despite that they could be expected to behave rather differently from Σbi-rules by analogy with the case of strong fragments.

In this talk, we will try to systematically investigate parameter-free and inference rule versions of the theories Ti2 and Si2. We will particularly focus on the following questions:

  • Reductions between the various rules and schemata.
  • Conservativity results between the fragments, and the formula complexity of axioms.
  • The number of instances (nesting) of R needed to generate the closure T+R, and finite axiomatizability of fragments.
  • Reformulation of axioms and rules in terms of reflection principles for propositional proof systems.
  • Conditional or relativized separations between the fragments.
Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic

ABSTRACT. The aim of this presentation is to show that a lot of complexity theory can be formalized in low fragments of arithmetic like Cook's theory PV1. We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV1 (no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the (n,d,λ)-graphs needed to derive the PCP theorem in PV1.