Sistema de prova de soma de quadrados

Recentemente, vi vários artigos sobre o arxiv que se referem a um sistema de prova chamado soma de quadrados.

Alguém pode explicar o que é uma prova de soma de quadrados e por que essas provas são importantes / interessantes?

Como eles estão relacionados a outros sistemas de provas algébricas? Eles são algum tipo de dualidade com Lassere?

O sistema básico de prova de soma de quadrados, introduzido sob o nome de refutações de Positivstellensatz por Grigoriev e Vorobjov , é um sistema de prova "estático" para mostrar que um conjunto de equações e inequações polinomiais onde f 1 , … , f k , h 1 , …

$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ , não tem solução comum em R n : uma refutação de S é dada por polinômios$f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$$\mathbb R^n$$S$ e e I , j tal que - 1 = k ∑ i = 1 g i f i + ∑ I ⊆ { 1 , … , m } ∑ j e 2 $g_i$$e_{I,j}$ (Pode-se trabalhar com qualquer campo fechado real no lugar deR.) A Positivstellensatz de Stengle garante queStenha uma refutação se e somente se não tiver solução. A principal medida de complexidade aqui é ograude refutação, que é o máximo do total de graus dos polinômios que aparecem sob os sinais de soma( $$\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$ , ou seja, g i f i e e 2 I , j Π i ∈ I h i .$(*)$$g_if_i$$e_{I,j}^2\prod_{i\in I}h_i$

Como de costume em sistemas de prova algébrica, também se pode considerar um sistema de refutação de fórmulas booleanas insatisfatórias incluindo em S os axiomas x 2 i - x i para cada variável x i e uma tradução de ϕ por desigualdades polinomiais.$\phi$$S$$x_i^2-x_i$$x_i$$\phi$

Mais informações sobre a história e o desenvolvimento dos sistemas SOS podem ser encontradas em http://arxiv.org/abs/1211.1958 .

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

As regras de inferência são:

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$

Existem boas conexões com programação semidefinida e algoritmos de aproximação.

Para saber mais, confira a recente palestra de Albert Atserias no workshop BIRS: Fundamentos Teóricos da Resolução Aplicada de SAT :

• Albert Atserias , Mini-Tutorial em Sistemas de Prova Semi-Algébrica ( slides ), 2014