Abstract
We relate different approaches for proving the unsatisfiability of a system of real polynomial equations over Boolean variables. On the one hand, there are the static proof systems SheraliAdams and
sumofsquares (a.k.a. Lasserre), which are based on linear and
semidefinite programming relaxations. On the other hand, we
consider polynomial calculus, which is a dynamic algebraic proof
system that models GrÃ¶bner basis computations.
Our first result is that sumofsquares simulates polynomial
calculus: any polynomial calculus refutation of degree d can be
transformed into a sumofsquares refutation of degree 2d and only
polynomial increase in size.
In contrast, our second result shows that this is not the case for SheraliAdams: there are systems of polynomial equations that have polynomial calculus refutations of degree 3 and polynomial size, but require SheraliAdams refutations of large degree and exponential size.
A corollary of our first result is that the proof systems
Positivstellensatz and Positivstellensatz Calculus, which have been separated over nonBoolean polynomials, simulate
each other in the presence of Boolean axioms.
BibTeX  Entry
@InProceedings{berkholz:LIPIcs:2018:8527,
author = {Christoph Berkholz},
title = {{The Relation between Polynomial Calculus, SheraliAdams, and SumofSquares Proofs}},
booktitle = {35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
pages = {11:111:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770620},
ISSN = {18688969},
year = {2018},
volume = {96},
editor = {Rolf Niedermeier and Brigitte Vall{\'e}e},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/8527},
URN = {urn:nbn:de:0030drops85279},
doi = {10.4230/LIPIcs.STACS.2018.11},
annote = {Keywords: Proof Complexity, Polynomial Calculus, SumofSquares, SheraliAdams}
}
Keywords: 

Proof Complexity, Polynomial Calculus, SumofSquares, SheraliAdams 
Collection: 

35th Symposium on Theoretical Aspects of Computer Science (STACS 2018) 
Issue Date: 

2018 
Date of publication: 

27.02.2018 