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.

ABSTRACT. We present n^{O(log log n)}-size proofs in the (tree-like) monotone sequent calculus of the pigeonhole principle with (1 + ε)n pigeons and n holes, for ε = 1/polylog n. This improves on the bound of n^{O(log n)} inherited from proofs of the usual pigeonhole principle, with n + 1 pigeons and n holes, by Atserias et al., and supports the more general conjecture that the monotone sequent calculus polynomially simulates Hilbert-Frege systems.

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.

ABSTRACT. We show Ω(n²) lower bounds on the total space used in resolution refutations of random k-CNFs over n variables, and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the long-standing open problem of whether there are families of k-CNF formulas of size O(n) requiring total space Ω(n²) in resolution, and gives the first truly quadratic lower bounds on total space. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.

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.

ABSTRACT. I will first talk about the complexity of generating identities of matrix rings. And demonstrate an unconditional lower bound on the minimal number of generators needed to generate a matrix identity, where the generators are substitution instances of elements from any given finite basis of the matrix identities.

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 exponential-size lower bounds on arithmetic proofs, which are proofs of polynomial identities operating with arithmetic circuits and whose axioms are the polynomial-ring axioms (these proofs serve as an algebraic analogue of the Extended Frege propositional proof system). I will also discuss shortly the applicability of our approach to strong propositional proof systems.

Based on a joint work with Fu Li.

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.

We prove exponential lower bounds on the running time of DPLL with splitting by linear combinations on 2-fold Tseitin formulas and on formulas that encode the pigeonhole principle.

Raz and Tzameret introduced a system R(lin) that operates with disjunctions of linear equalities with integer coefficients. We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over GF(2); we call this system Res-Lin. Res-Lin can be p-simulated in R(lin) but currently we do not know any superpolynomial lower bounds in R(lin). Tree-like proofs in Res-Lin are equivalent to the behavior of our algorithms on unsatisfiable instances. We prove that Res-Lin is implication complete and also prove that Res-Lin is polynomially equivalent to its semantic version.

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^Ω(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however - the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.

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.