Logic seminar

On Semi-Algebraic Proofs and Algorithms

We discuss a new characterization of the Sherali-Adams proof system, a standard propositional proof system considered in both proof complexity and combinatorial optimization, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula F if and only if there is an ε > 0 and a degree-d conical junta J such that viol(x) − ε = J, where viol(x) counts the number of falsified clauses of F on an input x. This result implies that the linear separation complexity, a complexity measure recently studied by Hrubes (and independently by de Oliveira Oliveira and Pudlak under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs, sharpening a feasible interpolation result of Hakoniemi. On the lower-bound side, we prove a separation between the conical junta degree of viol(x) - 1 and Resolution width; since Sherali-Adams can simulate Resolution this also separates the conical junta degree of viol(x) - 1 and viol(x) - ε for arbitrarily small ε > 0. Finally, by applying known lifting theorems, we can translate this separation into separations between extension complexity and monotone circuit complexity.

This talk is based on joint work with Noah Fleming, Mika Goos, and Stefan Grosser.