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?

— Anonimowy
źródło

Przegląd znajduje się w arxiv.org/abs/1211.1958 . Podstawowy system SOS został zdefiniowany na stronie 3 (poszukaj Grigoriewa i Worobjowa).

— Emil Jeřábek wspiera Monikę

@Emil, wydaje się, że artykuł zawiera odpowiedzi na pytania zawarte w poście (wyjaśnia system, jego historię i znaczenie dla ostatnich prac), dlaczego nie opublikować komentarza jako odpowiedzi?

— Kaveh

@ EmilJeřábek Przyjmuję twój komentarz, jeśli opublikujesz jego rozszerzoną wersję jako odpowiedź.

— Anonimowy

OK, zrobiłem to, chociaż wolałbym, gdyby odpowiedziała na nie ktoś, kto faktycznie rozumie te systemy.

— Emil Jeřábek popiera Monikę

Odpowiedzi:

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

S. = {{fa}_{1} = 0, \dots, {fa}_{k} = 0, h_{1} \geq 0, \dots, h_{m} \geq 0},

$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$

, ma wspólny rozwiązanie

: a odrzucenia

oblicza się według wielomianów

w taki sposób,

f_{1}, \dots, f_{k}, h_{1}, \dots, h_{m} \in R [x_{1}, \dots, x_{n}]

$f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$

R^{n}

$\mathbb R^n$

S

$S$

g_{i}

$g_i$

e_{I, j}

$e_{I,j}$

(Można pracować z dowolnym prawdziwym zamkniętym polem zamiast

) Positivstellensatz Stengle'a gwarantuje, że

ma 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

, tzn

\begin{matrix} (*) & - 1 = \sum_{ja = 1}^{k} {sol}_{ja} {fa}_{ja} + \sum_{ja \subseteq {1, \dots, m}} \sum_{jot} {mi}_{ja, jot}^{2)} \prod_{ja \in ja} h_{ja} . \end{matrix}

$\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.$

R

$\mathbb R$

S

$S$

(*)

$(*)$

g_{i} f_{i}

$g_if_i$

e_{I, j}^{2} \prod_{i \in I} h_{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 aksjomatów dla każdej zmiennej 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 .

— Emil Jeřábek wspiera Monikę
źródło

Czy istnieje standardowa książka?

Czy jest tu także jakieś zastosowanie teorii modeli?

Laserre ma ostatnią książkę na temat aspektów optymalizacji. „Wprowadzenie do optymalizacji wielomianowej i półalgebraicznej” opublikowane przez Cambridge University Press.

— Chandra Chekuri

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

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

$\over x^2-x \geq 0$
$\over x-x^2 \geq 0$
$\over p(\vec{x})^2\geq 0$
$p(\vec{x}) \geq 0 \over p(\vec{x})x \geq 0$
$p(\vec{x}) \geq 0 \over p(\vec{x})(1-x) \geq 0$
$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

— Kaveh
źródło

Czy ten preparat jest taki sam jak Emila? Twoja jest „dynamiczna”, a zatem pozwala na dowody podobne do DAG, gdzie Emila jest „statyczne”, a zatem wydaje się, że odpowiada twojej wersji drzewiastej. Najwyraźniej różnią się one pod względem złożoności (np. Stopień, rozmiar pod względem liczby monomialów i liczby linii). Czy to prawda?

— Iddo Tzameret

@Iddo, myślę, że masz rację. Miara złożoności może nie być taka sama. Albert w swoim wystąpieniu wyjaśnia bardzo krótko korespondencję dla głównej interesującej miary złożoności, jeśli dobrze pamiętam, ale jeśli ktoś interesuje się innymi miarami, to trzeba być bardziej ostrożnym w formułowaniu.

— Kaveh

@Kaveh Zadałem dwa powiązane pytania, jeśli możesz uprzejmie pomóc, (1) cstheory.stackexchange.com/questions/30930/… (2) cstheory.stackexchange.com/questions/30932/…

— user6818