Open problems/work in progress seminar
hosted by Studentsky logicky seminar in Fall 2011

Usual time and place: Thursday 10.40 - 12.10, Dept. of Algebra, Karlin

Program in anti-chronological order:

  • 14.December at 12.2o (note different day/time)
    We shall have a double seminar this time:

    1) Petra Kurinova
    A polynomial algorithm for the binary Post Correspondence Problem

    The Post Correspondence Problem is undecidable in general but it is in the computational complexity class P in the binary case. I shall talk about a p-time algorithm for the problem.

    2) Alena Peterova
    Lower bounds for resolution using Razborov's approximation method

    One method for proving lower bounds on the length of resolution and cutting plane proofs is to reduce them to monotone circuits (Krajicek; Pudlak). Then, the Razborov's approximation method is used to prove exponential lower bound on the size of monotone circuits. Our goal is to apply the approximation method on the resolution proofs directly.


  • 8.December at 10.4o
    Jan Pich
    Provability of circuit lower bounds in Bounded Arithmetics

    Interesting circuit lower bounds like SAT$\notin$ P/poly could be unprovable in strong fragments of Bounded Arithmetic. This possibility is reflected in Razborov's conjecture about NW-generators. We will discuss it and show that NW-generators are hard for a tree-like version of Frege working with formulas built on a fraction of variables of the statement that is supposed to be proven.
    Another way how to obtain the unprovability result for strong theories (under a hardness assumption) is to prove that proofs of circuit lower bounds in these systems are NP-natural. It can be shown that in all sufficiently strong proof systems admitting a feasible disjunction property circuit lower bounds are already NP-natural. We will present the argument in the context of intuitionistic Bounded Arithmetics.

    The intuitionistic part is joint work with Kaveh Ghasemloo.


  • 1.December at 10.4o
    Yuval Filmus
    Interpolating Cutting Plane(s) using games

    Cutting Plane(s) is a refutation proof system coming in two flavors, syntactic and semantic. Interpolation theorems have been proved for the semantic version with small coefficients (Krajicek; Pitassi et al.) and for the (unrestricted) syntactic version (Pudlak). The former theorems construct monotone boolean circuits, the latter monotone real circuits. For both types of circuits there are strong lower bounds, which in turn imply strong lower bounds on the size of CP refutations of the clique/coclique dichotomy.
    We rephrase the constructions of Krajicek and Pitassi et al. in terms of a two-player game which translates to a monotone boolean circuit. A random version of the game translates to a monotone real circuit.
    We had hoped that the more advanced version of the game would enable us to prove an interpolation theorem for unrestricted semantic CP. However, at this stage it stands as an open problem.

    Joint work with Toni Pitassi.


  • 24.November at 10.40
    Alexander V. Smal
    Optimal algorithms, acceptors and proof systems

    The existence of optimal objects, such as algorithms, acceptors or proof systems, is a major open question in complexity theory. There is a bunch of results that relate existence of one optimal object to another. This talk will give a short survey on results about such an optimal objects and related open problems.


  • 18.November (Friday) at 13.3o-45
    (note atypical day and hour!)
    Anupam Das
    The Relative Complexity of Deep Inference Proof Systems

    Deep inference proof systems, broadly construed, are an extension of regular inference systems by allowing inference rules to operate arbitrarily deep inside a formula, rather than on just the main connective. Clearly this can allow for a speedup in size of proofs, but there are many questions open regarding the significance of this speedup, especially for its cut-free tree-like systems. In this talk I will talk through recent results connecting the complexity of deep inference proofs to more traditional systems. In particular I will pose (and briefly discuss) the problem of finding a lower bound for cut-free tree-like deep inference, which remains open.


  • 10.November: no seminar


  • 3.November
    There will be two seminars:

    1) Kaveh Ghasemloo (morning)
    Subsystems of TV^0 and sub-exponential size bounded depth Frege proofs

    We study subsystems of $TV^0$ where string induction axiom is restricted to sublinear size strings and show how first-order proofs of bounded formulas in these theories translate to subexponential size bounded-depth Frege proofs. We also show that string induction for size $n^{1/d}$ strings contains $VNC^1$ by formalizing the well-known fact that $NC^1$ circuits have sub-exponential size bounded-depth circuits. As a corollary we obtain an alternative proof of [FPS'11] that subexponential size bounded-depth Frege simulates Frege.

    This is joint work with Phuong Nguyen and Steve Cook.

    [FPS'11]: Yuval Filmus, Toniann Pitassi, Rahul Santhanam, "Exponential lower bounds for AC^0-Frege imply polynomial Frege lower bounds", ICALP 2011.

    2) Sebastian Muller (afternoon, 13.3o)
    Short Proofs by short Cuts

    We study polylogarithmic cuts of models of the bounded arithmetic V^0. We will see that any polylog cut N of a $V^0$ model M is a model of $VNC^1$. This is due to the fact that N-strings can be represented as numbers in M and we can thus use a stronger form of induction to prove a $VNC^1$-complete problem. As a corollary we obtain a modeltheoretic proof of a uniform version of the result from [FPS11] that bounded-depth Frege subexponentially simulates Frege.


  • 27.October
    Dai Le
    Formalizing the Goldreich-Levin theorem

    The Goldreich-Levin theorem is one of the most fundamental theorems of cryptography. The theorem shows how to construct a hardcore predicate from any one-way function. I will discuss our progress on how to extend Emil Jerabek's approximate counting framework to formalize this theorem within the theory VPV + the surjective weak pigeonhole principle for polytime functions.

    The work is joint with Wesley George and Stephen Cook.


  • 20.October
    Luke Friedman
    continues from 13.October


  • 13.October
    Luke Friedman
    Kolmogorov Complexity, Circuits, and the Strength of Logical Theories of Arithmetic

    Can complexity classes be characterized in terms of efficient reducibility to the (undecidable) set of Kolmogorov-random strings? Although this might seem improbable, a series of papers has recently provided evidence that this may be the case. In particular, it is known that there is a class of problems C defined in terms of polynomial-time truth-table reducibility to R_K (the set of Kolmogorov-random strings) that lies between BPP and PSPACE. In this talk, we investigate improving this upper bound from PSPACE to (PSPACE intersect P/poly)
    More precisely, we present a collection of true statements in the language of arithmetic, (each provable in ZF) and show that if these statements can be proved in certain extensions of Peano arithmetic, then BPP \subseteq C \subseteq (PSPACE intersect \Ppoly)
    We conjecture that C is equal to P, and discuss the possibility this might be an avenue for trying to prove the equality of BPP and P.

    Joint with Eric Allender, George Davie, Sam Hopkins, and Iddo Tzameret


  • 6.October
    Jan Krajicek
    On possibilities to extend feasible interpolation to stronger proof systems

    The feasible interpolation idea, known facts, chain feasible interpolation, feasible disjunction property, and various problems.