System sprawdzania sumy kwadratów

Ostatnio widziałem kilka artykułów na temat arxiv, które odnoszą się do systemu sprawdzania zwanego sumą kwadratów.

Czy ktoś może wyjaśnić, co to jest dowód sumy kwadratów i dlaczego takie dowody są ważne / interesujące?

Jak są one powiązane z innymi algebraicznymi systemami dowodowymi? Czy są czymś podwójnym w stosunku do Lassere?

Podstawowy system sprawdzania sum kwadratów, wprowadzony przez Grigoriewa i Worobjowa pod pozorami Positivstellensatz , jest „statycznym” systemem dowodzenia pokazującym, że zbiór równań i równań wielomianowych gdzie f 1 , … , f k , h 1 , …

$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ , ma wspólny rozwiązanie R n : a odrzucenia S oblicza się według wielomianów g ı i wiadomości e I , J, w taki sposób, - 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}$ (Można pracować z dowolnym prawdziwym zamkniętym polem zamiastR.) Positivstellensatz Stengle'a gwarantuje, żeSma obalenie tylko wtedy, gdy nie ma rozwiązania. Głównym kryterium złożoność jest tustopieńz odrzucenia, który jest maksymalnym wszystkich stopni wielomianów, które znajdują się pod postacią sumy z(*), tzngIfIie2I,JΠi∈Ihja. $$\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$

Jak zwykle w przypadku algebraicznych systemów dowodowych, można go również uznać za system odrzucania niezadowalających wzorów boolowskich poprzez włączenie do S aksjomatów x 2 i - x i dla każdej zmiennej x i oraz tłumaczenie ϕ przez nierówności wielomianowe.$\phi$$S$$x_i^2-x_i$$x_i$$\phi$

Więcej na temat historii i rozwoju systemów SOS można znaleźć na stronie http://arxiv.org/abs/1211.1958 .

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

Reguły wnioskowania są następujące:

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$

Są ładne połączenia z półfinałowym programowaniem i algorytmami aproksymacyjnymi.

Więcej informacji można znaleźć w ostatnim wystąpieniu Alberta Atseriasa podczas warsztatów BIRS Teoretyczne podstawy zastosowania rozwiązania SAT :

• Albert Atserias , Mini-samouczek na temat półalgebraicznych systemów dowodowych ( slajdy ), 2014