Edward Hirsch, Arist Kojevnikov

We prove that the Cutting Plane proof system based on

Gomory-Chvatal cuts polynomially simulates the

lift-and-project system with integer coefficients

written in unary. The restriction on coefficients can be

omitted when using Krajicek's cut-free Gentzen-style extension

of both systems. We also prove that Tseitin tautologies

have short proofs in ...
more >>>

Edward Hirsch, Sergey I. Nikolenko

Goerdt (1991) considered a weakened version of the Cutting Plane proof system with a restriction on the degree of falsity of intermediate inequalities. (The degree of falsity of an inequality written in the form $\sum a_ix_i+\sum b_i(1-x_i)\ge c,\ a_i,b_i\ge0$ is its constant term $c$.) He proved a superpolynomial lower bound ... more >>>

Dmitry Sokolov

In 1990 Karchmer and Widgerson considered the following communication problem $Bit$: Alice and Bob know a function $f: \{0, 1\}^n \to \{0, 1\}$, Alice receives a point $x \in f^{-1}(1)$, Bob receives $y \in f^{-1}(0)$, and their goal is to find a position $i$ such that $x_i \neq y_i$. Karchmer ... more >>>

Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, Avi Wigderson

The Stabbing Planes proof system was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas -- certain unsatisfiable systems of linear equations mod 2 -- which are canonical ... more >>>

Noah Fleming, Toniann Pitassi, Robert Robere

We further the study of supercritical tradeoffs in proof and circuit complexity, which is a type of tradeoff between complexity parameters where restricting one complexity parameter forces another to exceed its worst-case upper bound. In particular, we prove a new family of supercritical tradeoffs between depth and size for Resolution, ... more >>>