Система доказательства суммы квадратов

Недавно я видел несколько статей об arxiv, которые ссылаются на систему доказательств под названием сумма квадратов.

Может кто-нибудь объяснить, что такое доказательство суммы квадратов и почему такие доказательства важны / интересны?

Как они связаны с другими алгебраическими системами доказательств? Они что-то вроде двойника Лассере?

Базовая система доказательства суммы квадратов, введенная Григорьевым и Воробьёвым под названием «Позитивстелленсатц опровержения» , представляет собой «статическую» систему доказательства, показывающую, что система полиномиальных уравнений и неравенств где f 1 , … , f k , h 1 , …

$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ , не имеет общего решения в R n : опровержение S задается полиномами g i и e I , j, такими что - 1 = k ∑ i = 1 g i f i + ∑ I ⊆ { 1 , … , m } ∑ j e 2 $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$$\mathbb R^n$$S$$g_i$$e_{I,j}$ (ВместоRможно работать с любым действительно замкнутым полем.) Positivstellensatz Стенгла гарантирует, чтоSимеет опровержение тогда и только тогда, когда у него нет решения. Основной мерой сложности здесь являетсястепеньопровержения, которая является максимумом всех степеней полиномов, которые появляются под знаками суммы в(∗), то естьgifiиe2I,j∏i∈Iчя. $$\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.$$ $\mathbb R$$S$$(*)$$g_if_i$$e_{I,j}^2\prod_{i\in I}h_i$

Как обычно с алгебраическими системами доказательств, можно также рассматривать ее как систему опровержений для неудовлетворительных булевых формул , включив в S аксиомы x 2 i - x i для каждой переменной x i и перевод ϕ с помощью полиномиальных неравенств.$\phi$$S$$x_i^2-x_i$$x_i$$\phi$

Более подробную информацию об истории и развитии систем SOS можно найти по адресу http://arxiv.org/abs/1211.1958 .

$p(\vec{x}) \geq 0$$p(\vec{x})$$\vec{x}$

Правила вывода:

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$$c_1, \cdots, c_m \in \mathbb{R}^+$

$p(\vec{x})^2\geq 0$

Есть хорошие связи с полуопределенными алгоритмами программирования и аппроксимации.

Для получения дополнительной информации посмотрите недавний доклад Альберта Ацериаса на семинаре BIRS. Теоретические основы прикладного SAT-решения :

• Альберт Ацериас , мини-учебник по полуалгебраическим системам доказательства ( слайды ), 2014