Sum-of-squares proof system

Question

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?

Answer 1

The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by Grigoriev and Vorobjov, 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 .

Answer 2

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's recent talk at BIRS workshop Theoretical Foundations of Applied SAT Solving:

• Albert Atserias, Mini-Tutorial on Semi-Algebraic Proof Systems (slides), 2014