## New Directions in Proof Complexity

**Monday 10th April 2006 to Thursday 13th April 2006**

08:30 to 10:00 | Registration | ||

10:00 to 11:00 |
P Pudlak ([Academy of Sciences, Prague])$On \forall\Sigma_1^b$ sentences provable in bounded arithmetic We shall give a characterization of \forall\Sigma_1^b sentences provable in theories S_2^i. We shall consider also certain unrestricted versions of the principles that characterize these sentences and prove that they require iterated exponential time. This gives partial evidence that the hierarchy of \forall\Sigma_1^b sentences provable in S_2^i is strictly increasing. |
INI 1 | , |

11:00 to 11:30 | Coffee | ||

11:30 to 12:00 |
P Nguyen ([Toronto])The complexity of proving the discrete Jordan Curve theorem and related principles The Jordan Curve Theorem states that a simple, closed curve divides the plane into exactly two connected components. We consider the ``discrete'' version of this theorem (JCT) where the curve lies in an nxn grid. The Theorem can be formalized as either true statements in Bounded Arithmetic or families of propositional tautologies. Here we show that the formalizations in Bounded Arithmetic are provable in some weak theories (i.e., V^0 and V^0(2)); this implies that the families of tautologies have short proofs in the corresponding propositional proof systems. First, we formalize the theorem when the simple curve is given as a sequence of edges on the grid. We show that in this case the theorem can be proved in the theory V^0. Next, we consider the case where the input is a set of edges which generally form multiple simple closed curves. The interesting conclusion here is that the set of edges divides the plane into at least two connected components. We show that this is indeed provable in the theory V^0(2). The related principles include the STCONN on grid graph considered by Buss [Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies] and the nonplanarity of K3,3. STCONN is reducible to JCT, and thus it is provable in V^0(2). This improves Buss's result (that STCONN has polysize proof in TC^0-Frege). |
INI 1 | , |

12:00 to 12:30 |
A Beckmann ([Wales])Uniform proof complexity One main aim in Propositional Proof Complexity is to prove strong lower bounds for a general propositional proof system. Inspired by this program, we will introduce uniform reducts of propositional proof systems. Uniform reducts are sets of first order formulas of arithmetic which are defined using translations from first order formulas to propositional formulas. We will describe basic properties of uniform reducts, discuss their relationship to Cook's Programme, and explain some more advanced features of them. Recently, Steve Cook made an obervation relating the study of uniform reducts to the existence of optimal proof systems - if time permits we will touch on this as well. |
INI 1 | , |

12:30 to 13:30 | Lunch at Wolfson Court | ||

14:00 to 15:00 |
N Thapen ([Academy of Sciences, Prague])$T^1_2, T^2_2$ and search problems We give some new, natural principles characterizing the \Sigma^b_1 consequences of these theories, based on a reflection principle for resolution. |
INI 1 | |

15:00 to 15:30 | Tea | ||

15:30 to 16:00 |
E Jerabek ([Toronto])Approximate counting in bounded arithmetic We use the dual weak pigeonhole principle to develop approximate counting in bounded arithmetic. As an application, we show how to formalize classes of randomized algorithms, such as BPP. |
INI 1 | , |

16:00 to 16:30 |
C Pollett (San José State University)When can $S^1_2$ prove the weak pigeonhole principle? It is well known result of Krajicek and Pudlak that if $S^1_2$ could prove the injective weak pigeonhole principle for every polynomial time function then RSA would not be secure. In this talk, we will consider function algebras based on a common characterization of the polynomial time functions where we slightly modify the initial functions and further restrict the amount of allowable recursion. We will then argue that $S^1_2$ can prove the surjective weak pigeonhole principle for functions in this algebra. |
INI 1 | , |

17:00 to 18:00 | Wine and Beer Reception | ||

18:45 to 19:30 | Dinner at Wolfson Court (Residents only) |

09:30 to 10:30 |
S Cook ([Toronto])Capturing complexity classes by their reasoning power For each of many standard complexity classes within NP we associate a canonical set of universal and existential theorems which are those which can be proved using concepts in the class. In some cases we can also associate canonical proof systems in the quantified propositional calculus. |
INI 1 | , |

10:30 to 11:00 |
M Vardi ([Rice])Constraint propagation as a proof system Refutation proofs can be viewed as a special case of constraint propagation, which is a fundamental technique in solving constraint-satisfaction problems. The generalization lifts, in a uniform way, the concept of refutation from Boolean satisfiability problems to general constraint-satisfaction problems. On the one hand, this enables us to study and characterize basic concepts, such as refutation width, using tools from finite-model theory. On the other hand, this enables us to introduce new proof systems, based on representation classes, that have not been considered up to this point. We consider ordered binary decision diagrams (OBDDs) as a case study of a representation class for refutations, and compare their strength to well-known proof systems, such as resolution, the Gaussian calculus, cutting planes, and Frege systems of bounded alternation-depth. In particular, we show that refutations by ODBBs polynomially simulate resolution and can be exponentially stronger. Joint work with Albert Atserias and Phokion Kolaitis. |
INI 1 | , |

11:00 to 11:30 | Coffee | ||

11:30 to 12:00 |
M Soltys ([McMaster])The proof complexity of matrix algebra There are fast parallel algorithms for computing the characteristic polynomial of a matrix: notably Berkowitz's and Csanky's algorithms. While these algorithms run in NC2, all the known proofs of correctness require polynomial time concepts. Are there quasi-polynomial Frege (i.e., NC2-Frege) proofs of correctness of these algorithms? Or is it the case the universal matrix identities separate Frege and Extended Frege? This talk will address these questions and present recent progress in this area. |
INI 1 | |

12:00 to 12:30 |
S Perron ([Toronto])A minimal quantified proof system for polytime reasoning |
INI 1 | |

12:30 to 13:30 | Lunch at Wolfson Court | ||

14:00 to 15:00 |
R Impagliazzo ([California, San Diego])Which SAT instances are the hardest? |
INI 1 | |

15:00 to 15:30 | Tea | ||

15:30 to 16:00 |
S Riis ([London])Sporadic propositional proofs The following feature is shared by certain weak propositional proof systems: If $\psi_n$ is a uniformly generated sequence of propositional formula, and the sequence $\psi_n$ has polynomial size proofs, then the sequence $\psi_n$ in fact has polynomial size proofs that are generated in an uniform manner . For stronger propositional proof systems (like the Frege Proof Systems) this feature might fail and sporadic proofs (that are not instances of a sequence of uniform proofs) might exist. In the talk I will argue that understanding and limiting the behaviour of these sporadic proofs could be crucial for any serious progress in Propositional Proof Complexity. |
INI 1 | , |

16:00 to 16:30 |
N Galesi ([Rome])Resolution by pebbling games We present an approach to study the complexity of refutations in Resolution by means of certain pebbling games. We will define certain classes of such games that allow to obtain a new frame for: (1) proving size lower bounds in Resolution; (2) devising new algorithms to find Resolution refutations; (3) characterizing the hardness of provability in Resolution as an "almost" satisfiability. We'll discuss about how to extend a similar approach to stronger systems than Resolution. |
INI 1 | |

18:45 to 19:30 | Dinner at Wolfson Court (Residents only) |

09:30 to 10:30 |
T Pitassi ([Toronto])Using lower bounds in proof complexity |
INI 1 | , |

10:30 to 11:00 |
J Nordstrom ([Royal Institute of Technology, Stockholm])Narrow proofs may be spacious: separating space and width in resolution The width of a resolution proof is the maximal number of literals in any clause of the proof. The space of a proof is the maximal number of memory cells used if the proof is only allowed to resolve on clauses kept in memory. Both of these measures have previously been studied and related to the refutation size of unsatisfiable CNF formulas. Also, the resolution refutation space of a formula has been proven to be at least as large as the refutation width, but it has remained unknown whether space can be separated from width or the two measures coincide asymptotically. We prove that there is a family of k-CNF formulas for which the refutation width in resolution is constant but the refutation space is non-constant, thus solving an open problem mentioned in several previous papers. |
INI 1 | , |

11:00 to 11:30 | Coffee | ||

11:30 to 12:30 |
N Segerlind ([Washington])Connections between zero-one programming, communication complexity and proof complexity Some of the most powerful techniques for solving NP-complete problems are based on integer programming techniques such as the Lovasz-Schrijver lift-and-project method. When used for satisfiability algorithms, such techniques can be viewed as propositional proof systems that prove tautologies (by establishing that the negation of a formula is unsatisfiable), and the proof structure is a successive derivation of low-degree inequalities over the rationals until a contradiction is found. A major challenge on the frontier of propositional proof complexity is to understand the power of these propositional proof systems (which we call "threshold logics") . At present, it is conceivable that such systems could prove every tautology with derivation cubic in the size of the tautology (note: it is fairly easy to come up with examples that require large refutations by a particular algorithm based on these ILP techniques, however, the proof systems can be viewed as generalizations that nondeterministically make optimal choices at each step to minimize derivation size, so the difference is between proving lower bounds for a particular algorithm and proving lower bounds for all possible algorithms of a certain form). It is conjectured that there are tautologies which require exponential size to prove in these systems but there is yet no proof to confirm this. In this lecture, we survey recent progress in a program towards proving size lower bounds for these logics by proving lower bounds for the multiparty number-on-the-forehead communication complexity of the set-disjointness function. Our primary contributions are: establishing the reduction from proof size lower bounds to communication lower bounds, and new lower bounds (that fall slightly short of what is needed for a superpolynomial proof size lower bound) for the NOF communication complexity of the set disjointness function. Some of this material will appear in Computational Complexity 2005, some of it is submitted, and some of it is ongoing. Collaborators include Paul Beame, Toniann Pitassi, and Avi Wigderson. |
INI 1 | |

12:30 to 13:30 | Lunch at Wolfson Court | ||

19:30 to 18:00 | Conference Dinner at Christ's College (Dining Hall) |

09:30 to 10:30 |
I Tzameret ([Tel Aviv])The strength of multilinear proofs We discuss an algebraic proof system that manipulates multilinear arithmetic formulas. We show this proof system to be fairly strong even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, algebraic proofs manipulating depth 3 multilinear arithmetic formulas are strictly stronger than Resolution, Polynomial Calculus (and Polynomial Calculus with Resolution); and (over characteristic 0) admit polynomial-size proofs of the (functional) pigeonhole principle. Finally, we illustrate a connection between lower bounds on multilinear proofs and lower bounds on multilinear arithmetic circuits. |
INI 1 | , |

10:00 to 10:30 |
ML Bonet ([Barcelona])A complete resolution-like calculus for Maxsat Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound. Joint work with Jordi Levy and Felip Manya. |
INI 1 | |

11:00 to 11:30 | Coffee | ||

11:30 to 12:30 |
S Dantchev ([Durham])Parametrised proof complexity Motivated by the well known concept of Fixed-Parameter Tractability, we initiate research in an area that we call Parametrised Proof Complexity. We first give a Cook-Rekhow-style definition of a parametrised proof system, and then relate the (im)possibility of existence of a fixed-parameter tractable (FPT) proof system to the FPT vs W[2] question. We observe that the most popular method for designing fixed-parameter algorithms, Bounded Search Tree, corresponds to Tree-like Resolution in the context of parametrised proof systems, and give some upper and lower bounds for the latter. We finally discuss and prove some dichotomy results (also called complexity gap theorems) for weak relativised proof systems. This is a work in progress, joint with B. Martin and S. Szeider. |
INI 1 | , |

12:30 to 13:30 | Lunch at Wolson Court | ||

14:00 to 14:30 |
P Naumov (McDaniel College)Meta complexity of propositional proofs |
INI 1 | |

14:30 to 15:30 |
M Alekhnovich ([California, San Diego])On the power of Lovasz-Schrijver hierarchy Lov\'{a}sz and Schrijver described a generic method of tightening the LP and SDP relaxation for any $0$-$1$ optimization problem. These tightened relaxations were the basis of several celebrated approximation algorithms (such as for MAX-CUT, MAX-3SAT, and SPARSEST CUT). In this talk I will survey recent lower bounds for the number of rounds in this model for well-known problems such as MAX-SAT, Hypergraph Vertex Cover and Minimum Set Cover. Also I will elaborate why these lower bounds are encoding dependent, in particular the standard NP reductions do not seem to work in this model. This fact leads to the wide list of open problems, which appear important for proof complexity, computational complexity and algorithm design. |
INI 1 | |

15:30 to 16:00 | Tea | ||

18:45 to 19:30 | Dinner at Wolfson Court (Residents only) |