eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-25
69:1
69:25
10.4230/LIPIcs.ITCS.2022.69
article
On Semi-Algebraic Proofs and Algorithms
Fleming, Noah
1
2
Göös, Mika
3
Grosser, Stefan
4
Robere, Robert
4
University of California, San Diego, CA, USA
Memorial University, St. John’s, Canada
EPFL, Lausanne, Switzerland
McGill University, Montreal, Canada
We give a new characterization of the Sherali-Adams proof system, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula C if and only if there is an ε > 0 and a degree-d conical junta J such that viol_C(x) - ε = J, where viol_C(x) counts the number of falsified clauses of C on an input x. Using this result we show that the linear separation complexity, a complexity measure recently studied by Hrubeš (and independently by de Oliveira Oliveira and Pudlák under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs.
We then investigate separation results for viol_C(x) - ε. In particular, we give a family of unsatisfiable CNF formulas C which have polynomial-size and small-width resolution proofs, but for which any representation of viol_C(x) - 1 by a conical junta requires degree Ω(n); this resolves an open question of Filmus, Mahajan, Sood, and Vinyals. Since Sherali-Adams can simulate resolution, this separates the non-negative degree of viol_C(x) - 1 and viol_C(x) - ε for arbitrarily small ε > 0. Finally, by applying lifting theorems, we translate this lower bound into new separation results between extension complexity and monotone circuit complexity.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol215-itcs2022/LIPIcs.ITCS.2022.69/LIPIcs.ITCS.2022.69.pdf
Proof Complexity
Extended Formulations
Circuit Complexity
Sherali-Adams