<p>SOS can be considered as a proof system where lines are of the form $p(\vec{x}) \geq 0$ where $p(\vec{x})$ is a polynomial in variables $\vec{x}$.</p>

<p>The inference rules are: </p>

<ol>
<li>$\over x^2-x \geq 0$</li>
<li>$\over x-x^2 \geq 0$</li>
<li>$\over p(\vec{x})^2\geq 0$</li>
<li>$p(\vec{x}) \geq 0 \over p(\vec{x})x \geq 0$</li>
<li>$p(\vec{x}) \geq 0 \over p(\vec{x})(1-x) \geq 0$</li>
<li>$p_1(\vec{x}) \geq 0, \cdots, p_m(\vec{x}) \geq 0 \over \sum_{i=1}^m c_ip_i(\vec{x}) \geq 0$ where $c_1, \cdots, c_m \in \mathbb{R}^+$</li>
</ol>

<p>The main difference from previous systems is that we have a rule for $p(\vec{x})^2\geq 0$.</p>

<p>There are nice connections with semidefinite programming and approximation algorithms. </p>

<p>For more check out <a href="http://www.lsi.upc.edu/~atserias/">Albert Atserias</a>'s recent talk at BIRS workshop <a href="http://www.birs.ca/events/2014/5-day-workshops/14w5101">Theoretical Foundations of Applied SAT Solving</a>:</p>

<ul>
<li><a href="http://www.lsi.upc.edu/~atserias/">Albert Atserias</a>, <a href="http://videos.birs.ca/2014/14w5101/201401211115-Atserias.mp4">Mini-Tutorial on Semi-Algebraic Proof Systems</a> (<a href="http://www.birs.ca/workshops/2014/14w5101/files/AtseriasBanff.pdf">slides</a>), 2014</li>
</ul>

CC BY-SA 3.0
2014-02-17T11:12:56.807Z
Is this formulation the same as Emil's? Yours is "dynamic", and hence allows for DAG-like proofs, where Emil's is "static", and hence seems to correspond to a tree-like version of yours. So, apparently they are different with respect to complexity (e.g., degree, size in terms of number of monomials, and number of lines). Is this true?
Iddo Tzameret
CC BY-SA 3.0
2014-02-17T12:22:51.283Z
@Iddo, I think you are right. A complexity measure may not be the same. Albert explains in his talk very briefly the correspondence for the main interesting complexity measure if I remember correctly, but if one is interested in other measures then there is a need to be more careful in formulation.
Kaveh
CC BY-SA 3.0
2015-03-27T16:02:42.927Z
@Kaveh I put up two related questions if you can kindly help, (1) http://cstheory.stackexchange.com/questions/30930/some-questions-about-the-paper-hypercontractivity-sum-of-squares-proofs-and-t?rq=1  (2) http://cstheory.stackexchange.com/questions/30932/what-is-a-level-r-pseudo-expectation-functional
user6818
CC BY-SA 3.0
2014-01-27T17:15:52.380Z
2014-01-27T17:23:12.787Z
2014-01-27T17:23:12.787Z
Kaveh
<p>The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by <a href="http://dx.doi.org/10.1016/S0168-0072%2801%2900055-0">Grigoriev and Vorobjov</a>, is a “static” proof system for showing that a set of polynomial equations and inequations
$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$
where $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$, has no common solution in $\mathbb R^n$: a refutation of $S$ is given by polynomials $g_i$ and $e_{I,j}$ such that
$$\tag{$*$}-1=\sum_{i=1}^kg_if_i+\sum_{I\subseteq\{1,\dots,m\}}\sum_je_{I,j}^2\prod_{i\in I}h_i.$$
(One could work with any real-closed field in place of $\mathbb R$.) Stengle’s Positivstellensatz guarantees that $S$ has a refutation if and only if it has no solution. The main complexity measure here is the <em>degree</em> of the refutation, which is the maximum of total degrees of the polynomials that appear under the sum signs in $(*)$, that is, $g_if_i$ and $e_{I,j}^2\prod_{i\in I}h_i$.</p>

<p>As usual with algebraic proof systems, one can also consider it as a refutation system for unsatisfiable Boolean formulas $\phi$ by including in $S$ the axioms $x_i^2-x_i$ for each variable $x_i$, and a translation of $\phi$ by polynomial inequalities.</p>

<p>More on the history and development of SOS systems can be found in <a href="http://arxiv.org/abs/1211.1958">http://arxiv.org/abs/1211.1958</a> .</p>

CC BY-SA 3.0
2015-10-20T01:20:54.240Z
Laserre has a recent book on the optimization aspects. "An Introduction to Polynomial and Semi-Algebraic Optimization" published by Cambridge University Press.
Chandra Chekuri
CC BY-SA 3.0
2013-12-10T20:54:51.443Z
2013-12-10T20:54:51.443Z
Emil Jeřábek
<p>Recently I have seen several articles on arxiv that refer to a proof system called sum-of-squares.</p>

<p>Can someone explain what is a sum-of-squares proof and why such proofs are important/interesting? </p>

<p>How are they related to other algebraic proof systems? Are they some kind of dual to Lassere?</p>

CC BY-SA 3.0
2012-11-20T17:50:14.360Z
There is some overview in http://arxiv.org/abs/1211.1958 . The basic SOS system is defined in passing on page 3 (look for Grigoriev and Vorobjov).
Emil Jeřábek
CC BY-SA 3.0
2012-11-21T05:35:43.220Z
@Emil, it seems that the paper contains the answers to the questions in the post (it explains the system, its history, and its relevance to recent works), why not post your comment as an answer?
Kaveh
CC BY-SA 3.0
2013-11-15T18:57:43.943Z
@EmilJeřábek I will accept your comment if you post an expanded version of it as an answer.
Anonymous
CC BY-SA 3.0
2013-12-10T20:56:42.933Z
OK, I’ve done that, though I’d have preferred if it were answered by someone who actually understands these systems.
Emil Jeřábek
<cc.complexity-theory><lo.logic><algebraic-complexity><proof-complexity><sum-of-squares>
Sum-of-squares proof system
Anonymous
# Sum-of-squares proof system

(Asked by: username_0 on 2012-11-20)

Recently I have seen several articles on arxiv that refer to a proof system called sum-of-squares.

Can someone explain what is a sum-of-squares proof and why such proofs are important/interesting?

How are they related to other algebraic proof systems? Are they some kind of dual to Lassere?

**Tags:** cc.complexity-theory, lo.logic, algebraic-complexity, proof-complexity, sum-of-squares
> **Comments:**
> **username_1**: There is some overview in http://arxiv.org/abs/1211.1958 . The basic SOS system is defined in passing on page 3 (look for Grigoriev and Vorobjov).  
> **username_2**: @Emil, it seems that the paper contains the answers to the questions in the post (it explains the system, its history, and its relevance to recent works), why not post your comment as an answer?  
> **username_0**: @EmilJeřábek I will accept your comment if you post an expanded version of it as an answer.  
> **username_1**: OK, I’ve done that, though I’d have preferred if it were answered by someone who actually understands these systems.  

---

## 2 answers

### Answer by username_1 on 2013-12-10. Score: 19 | Accepted answer

The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by [Grigoriev and Vorobjov](http://dx.doi.org/10.1016/S0168-0072%2801%2900055-0), is a “static” proof system for showing that a set of polynomial equations and inequations
$$S=\{f\_1=0,\dots,f\_k=0,h\_1\ge0,\dots,h\_m\ge0\},$$
where $f\_1,\dots,f\_k,h\_1,\dots,h\_m\in\mathbb R[x\_1,\dots,x\_n]$, has no common solution in $\mathbb R^n$: a refutation of $S$ is given by polynomials $g\_i$ and $e\_{I,j}$ such that
$$\tag{$\*$}-1=\sum\_{i=1}^kg\_if\_i+\sum\_{I\subseteq\{1,\dots,m\}}\sum\_je\_{I,j}^2\prod\_{i\in I}h\_i.$$
(One could work with any real-closed field in place of $\mathbb R$.) Stengle’s Positivstellensatz guarantees that $S$ has a refutation if and only if it has no solution. The main complexity measure here is the *degree* of the refutation, which is the maximum of total degrees of the polynomials that appear under the sum signs in $(\*)$, that is, $g\_if\_i$ and $e\_{I,j}^2\prod\_{i\in I}h\_i$.

As usual with algebraic proof systems, one can also consider it as a refutation system for unsatisfiable Boolean formulas $\phi$ by including in $S$ the axioms $x\_i^2-x\_i$ for each variable $x\_i$, and a translation of $\phi$ by polynomial inequalities.

More on the history and development of SOS systems can be found in <http://arxiv.org/abs/1211.1958> .

> **Comments:**
> **username_5**: Laserre has a recent book on the optimization aspects. "An Introduction to Polynomial and Semi-Algebraic Optimization" published by Cambridge University Press.  

---

### Answer by username_2 on 2014-01-27. Score: 12

SOS can be considered as a proof system where lines are of the form $p(\vec{x}) \geq 0$ where $p(\vec{x})$ is a polynomial in variables $\vec{x}$.

The inference rules are:

1. $\over x^2-x \geq 0$
2. $\over x-x^2 \geq 0$
3. $\over p(\vec{x})^2\geq 0$
4. $p(\vec{x}) \geq 0 \over p(\vec{x})x \geq 0$
5. $p(\vec{x}) \geq 0 \over p(\vec{x})(1-x) \geq 0$
6. $p\_1(\vec{x}) \geq 0, \cdots, p\_m(\vec{x}) \geq 0 \over \sum\_{i=1}^m c\_ip\_i(\vec{x}) \geq 0$ where $c\_1, \cdots, c\_m \in \mathbb{R}^+$

The main difference from previous systems is that we have a rule for $p(\vec{x})^2\geq 0$.

There are nice connections with semidefinite programming and approximation algorithms.

For more check out [Albert Atserias](http://www.lsi.upc.edu/~atserias/)'s recent talk at BIRS workshop [Theoretical Foundations of Applied SAT Solving](http://www.birs.ca/events/2014/5-day-workshops/14w5101):

* [Albert Atserias](http://www.lsi.upc.edu/~atserias/), [Mini-Tutorial on Semi-Algebraic Proof Systems](http://videos.birs.ca/2014/14w5101/201401211115-Atserias.mp4) ([slides](http://www.birs.ca/workshops/2014/14w5101/files/AtseriasBanff.pdf)), 2014

> **Comments:**
> **username_3**: Is this formulation the same as Emil's? Yours is "dynamic", and hence allows for DAG-like proofs, where Emil's is "static", and hence seems to correspond to a tree-like version of yours. So, apparently they are different with respect to complexity (e.g., degree, size in terms of number of monomials, and number of lines). Is this true?  
> **username_2**: @Iddo, I think you are right. A complexity measure may not be the same. Albert explains in his talk very briefly the correspondence for the main interesting complexity measure if I remember correctly, but if one is interested in other measures then there is a need to be more careful in formulation.  
> **username_4**: @Kaveh I put up two related questions if you can kindly help, (1) http://cstheory.stackexchange.com/questions/30930/some-questions-about-the-paper-hypercontractivity-sum-of-squares-proofs-and-t?rq=1  (2) http://cstheory.stackexchange.com/questions/30932/what-is-a-level-r-pseudo-expectation-functional  

---

