View: session overviewtalk overviewside by side with other conferences

09:15 | Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets SPEAKER: James Aisenberg ABSTRACT. We extend results of Bonet, Buss and Pitassi on Bondy's Theorem and of Nozaki, Arai and Arai on Boolobas's Theorem by proving that Frankl's Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parameter t, we prove that Frankl's Theorem has polynomial size, constant depth proofs from instances of the pigeonhole principle. |

09:45 | n^O(log log n) size monotone proofs of the weak pigeonhole principle SPEAKER: Anupam Das ABSTRACT. We present n |

10:45 | Weak Pigeonhole Principles, Circuits for Approximate Counting, and Bounded-Depth Proofs SPEAKER: Albert Atserias ABSTRACT. I will start this talk by giving an overview of the status of the weak pigeonhole principle (WPHP) in proof complexity and the connection between this problem and some fundamental questions on the computational complexity of approximate counting. Then I will discuss some recent progress on the main remaining question about WPHP, namely whether the known quasipolynomial-size depth-2 proof is optimal in terms of size. We show that a relativized version of the WPHP that also has quasipolynomial-size depth-2 proofs does indeed require quasipolynomial size to prove in depth-2. To our knowledge, this gives the first example of a natural principle with matching but superpolynomial upper and lower bounds in a natural proof system. |

12:00 | Total Space in Resolution SPEAKER: Ilario Bonacina ABSTRACT. We show Ω(n |

12:30 | From Small Space to Small Width in Resolution SPEAKER: Mladen Miksa ABSTRACT. In 2003, Atserias and Dalmau established that the space complexity of formulas in resolution is an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies on tools from finite model theory. We give an alternative proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds. |

14:30 | Are matrix identities hard instances for strong proof systems? SPEAKER: Iddo Tzameret ABSTRACT. I will first talk about the Based on the above, I will argue that matrix identities may be good hard candidates for strong proof systems, and I will discuss an initial study of this approach under different settings and assumptions. Under certain conditions, this approach can potentially lead up to Based on a joint work with Fu Li. |

15:30 | Lower bounds for splittings by linear combinations SPEAKER: Dmitry Itsykson ABSTRACT. A typical DPLL algorithm for the Boolean satisfiability problem splits the input problem into two by assigning the two possible values to a variable; then it simplifies the two resulting formulas. In the talk we consider an extension of the DPLL paradigm. Our algorithms can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that explicitly encode linear systems modulo two, which were used for proving exponential lower bounds for conventional DPLL algorithms. |

16:30 | Narrow Proofs May Be Maximally Long SPEAKER: Massimo Lauria ABSTRACT. We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n |

17:00 | Parity games and propositional proofs SPEAKER: Neil Thapen ABSTRACT. Parity games are a class of two player games played by moving a token around a finite graph. They have important applications in automata theory, logic and verification. The main computational problem for such games is to decide which player has a winning strategy. This problem is reducible to a search problem in the intersection of the classes PLS and PPAD, but is not known to be in P, despite intensive research work. A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if resolution is weakly automatizable, then the decision problem for parity games is in P. We also give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to the related classes of mean payoff games and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form. |