View: session overviewtalk overviewside by side with other conferences
10:45 | Opening SPEAKER: Olaf Beyersdorff |
11:00 | 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 | 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. |
12:30 | 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. |
14:30 | A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity SPEAKER: Jakob Nordström 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 | 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:30 | Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time SPEAKER: Jean-Jose Razafindrakoto ABSTRACT. In bounded arithmetic, a host of theories have been developed which correspond to complexity classes within the polynomial 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. |
17:00 | Parameter-free induction in bounded arithmetic SPEAKER: Emil Jeřábek 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:
|
17:30 | Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic SPEAKER: Ján Pich 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. |