TR17-042 Authors: Pavel Hrubes, Pavel Pudlak

Publication: 6th March 2017 12:08

Downloads: 552

Keywords:

We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept that we call "unsatisfiability certificate". This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we prove exponential lower bounds for random $k$-CNFs, where $k$ the logarithm of the number of variables, and for the Weak Bit Pigeon Hole Principle. Furthermore, we prove a monotone variant of a hypothesis of Feige. We give a superpolynomial lower bound on monotone real circuits that approximately decide the satisfiability of $k$-CNFs, where $k=\omega(1)$. For $k\approx\log n$, the lower bound is exponential.