Videos and presentation materials from other INI events are also available.
Event  When  Speaker  Title  Presentation Material 

LAAW04 
10th April 2006 10:00 to 11:00 
P Pudlak 
$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. 

LAAW04 
10th April 2006 11:30 to 12:00 
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 [Polynomialsize Frege and Resolution Proofs of stConnectivity 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^0Frege). 

LAAW04 
10th April 2006 12:00 to 12:30 
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. 

LAAW04 
10th April 2006 14:00 to 15:00 
$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. 

LAAW04 
10th April 2006 15:30 to 16:00 
E Jerabek 
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. 

LAAW04 
10th April 2006 16:00 to 16:30 
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. 

LAAW04 
11th April 2006 09:30 to 10:30 
S Cook 
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. 

LAAW04 
11th April 2006 10:30 to 11:00 
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 constraintsatisfaction problems. The generalization lifts, in a uniform way, the concept of refutation from Boolean satisfiability problems to general constraintsatisfaction problems. On the one hand, this enables us to study and characterize basic concepts, such as refutation width, using tools from finitemodel 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 wellknown proof systems, such as resolution, the Gaussian calculus, cutting planes, and Frege systems of bounded alternationdepth. In particular, we show that refutations by ODBBs polynomially simulate resolution and can be exponentially stronger. Joint work with Albert Atserias and Phokion Kolaitis. 

LAAW04 
11th April 2006 11:30 to 12:00 
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 quasipolynomial Frege (i.e., NC2Frege) 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. 

LAAW04 
11th April 2006 12:00 to 12:30 
A minimal quantified proof system for polytime reasoning  
LAAW04 
11th April 2006 14:00 to 15:00 
R Impagliazzo  Which SAT instances are the hardest?  
LAAW04 
11th April 2006 15:30 to 16:00 
S Riis 
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. 

LAAW04 
11th April 2006 16:00 to 16:30 
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. 

LAAW04 
12th April 2006 09:30 to 10:30 
T Pitassi  Using lower bounds in proof complexity  
LAAW04 
12th April 2006 10:30 to 11:00 
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 kCNF formulas for which the refutation width in resolution is constant but the refutation space is nonconstant, thus solving an open problem mentioned in several previous papers. 

LAAW04 
12th April 2006 11:30 to 12:30 
Connections between zeroone programming, communication complexity and proof complexity Some of the most powerful techniques for solving NPcomplete problems are based on integer programming techniques such as the LovaszSchrijver liftandproject 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 lowdegree 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 numberontheforehead communication complexity of the setdisjointness 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. 

LAAW04 
13th April 2006 09:30 to 10:30 
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 polynomialsize proofs of the (functional) pigeonhole principle. Finally, we illustrate a connection between lower bounds on multilinear proofs and lower bounds on multilinear arithmetic circuits. 

LAAW04 
13th April 2006 10:00 to 10:30 
A complete resolutionlike calculus for Maxsat MaxSAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolutionlike calculus for MaxSAT 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 MaxSAT and a time upper bound. Joint work with Jordi Levy and Felip Manya. 

LAAW04 
13th April 2006 11:30 to 12:30 
Parametrised proof complexity Motivated by the well known concept of FixedParameter Tractability, we initiate research in an area that we call Parametrised Proof Complexity. We first give a CookRekhowstyle definition of a parametrised proof system, and then relate the (im)possibility of existence of a fixedparameter tractable (FPT) proof system to the FPT vs W[2] question. We observe that the most popular method for designing fixedparameter algorithms, Bounded Search Tree, corresponds to Treelike 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. 

LAAW04 
13th April 2006 14:00 to 14:30 
P Naumov  Meta complexity of propositional proofs  
LAAW04 
13th April 2006 14:30 to 15:30 
On the power of LovaszSchrijver 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 MAXCUT, MAX3SAT, and SPARSEST CUT). In this talk I will survey recent lower bounds for the number of rounds in this model for wellknown problems such as MAXSAT, 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. 