Sistema de prueba de suma de cuadrados

Recientemente he visto varios artículos sobre arxiv que se refieren a un sistema de prueba llamado suma de cuadrados.

¿Alguien puede explicar qué es una prueba de suma de cuadrados y por qué esas pruebas son importantes / interesantes?

¿Cómo se relacionan con otros sistemas de prueba algebraica? ¿Son algún tipo de dual a Lassere?

cc.complexity-theory lo.logic algebraic-complexity proof-complexity sum-of-squares Anónimo
fuente

Hay una descripción general en arxiv.org/abs/1211.1958 . El sistema básico SOS se define de paso en la página 3 (busque Grigoriev y Vorobjov).

Emil Jeřábek apoya a Monica el

@Emil, parece que el documento contiene las respuestas a las preguntas en la publicación (explica el sistema, su historia y su relevancia para trabajos recientes), ¿por qué no publicar su comentario como respuesta?

Kaveh

@ EmilJeřábek Aceptaré tu comentario si publicas una versión ampliada de él como respuesta.

Anónimo el

Bien, lo he hecho, aunque hubiera preferido que fuera respondido por alguien que realmente entiende estos sistemas.

Emil Jeřábek apoya a Monica el

Respuestas:

El sistema de prueba de suma de cuadrados básico, introducido bajo el nombre de refutaciones Positivstellensatz por Grigoriev y Vorobjov , es un sistema de prueba "estático" para mostrar que un conjunto de ecuaciones y desigualdades polinómicas donde

S = {f_{1} = 0, \dots, f_{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\},$

, no tiene solución común en

: una refutación de

viene dado por polinomios

de tal manera que

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}$

(Se podría trabajar con cualquier campo realmente cerrado en lugar de

) Positivstellensatz de Stengle garantiza que

tiene una refutación si y solo si no tiene solución. La principal medida de complejidad aquí es elgradode refutación, que es el máximo de grados totales de los polinomios que aparecen bajo los signos de suma en

, es decir,

\begin{matrix} (*) & - 1 = \sum_{i = 1}^{k} g_{i} f_{i} + \sum_{I \subseteq {1, \dots, m}} \sum_{j} e_{I, j}^{2} \prod_{i \in I} h_{i} . \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$

$\phi$ $S$ $x_i^2-x_i$ $x_i$ $\phi$

Puede encontrar más información sobre la historia y el desarrollo de los sistemas SOS en http://arxiv.org/abs/1211.1958 .

Emil Jeřábek apoya a Monica
fuente

¿Hay un libro estándar?

¿También hay algún uso de la teoría de modelos aquí?

Laserre tiene un libro reciente sobre los aspectos de optimización. "Una introducción a la optimización polinómica y semi-algebraica" publicada por Cambridge University Press.

Chandra Chekuri

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

Las reglas de inferencia son:

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

Hay buenas conexiones con la programación semidefinida y los algoritmos de aproximación.

Para obtener más información, consulte la reciente charla de Albert Atserias en el taller BIRS Fundamentos teóricos de la resolución aplicada del SAT :

Albert Atserias , Mini-Tutorial sobre sistemas de prueba semi-algebraicos ( diapositivas ), 2014

Kaveh
fuente

¿Es esta formulación la misma que la de Emil? La suya es "dinámica" y, por lo tanto, permite pruebas similares a DAG, donde Emil es "estática" y, por lo tanto, parece corresponder a una versión suya similar a un árbol. Entonces, aparentemente son diferentes con respecto a la complejidad (por ejemplo, grado, tamaño en términos de número de monomios y número de líneas). ¿Es esto cierto?

Iddo Tzameret

@ Iddo, creo que tienes razón. Una medida de complejidad puede no ser la misma. Albert explica muy brevemente en su discurso la correspondencia para la principal medida de complejidad interesante si no recuerdo mal, pero si uno está interesado en otras medidas, entonces es necesario ser más cuidadoso en la formulación.

Kaveh

@Kaveh Puse dos preguntas relacionadas si puede ayudarme amablemente, (1) cstheory.stackexchange.com/questions/30930/… (2) cstheory.stackexchange.com/questions/30932/…

user6818