Sistema de prova de soma de quadrados

23

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?

Anônimo
fonte
11
Há uma visão geral em arxiv.org/abs/1211.1958 . O sistema SOS básico é definido na página 3 (procure Grigoriev e Vorobjov).
Emil Jeřábek apoia Monica
3
@Emil, parece que o artigo contém as respostas para as perguntas da publicação (explica o sistema, seu histórico e sua relevância para trabalhos recentes), por que não postar seu comentário como resposta?
Kaveh
@ EmilJeřábek Aceitarei seu comentário se você postar uma versão expandida dele como resposta.
Anónimo
2
OK, eu fiz isso, embora eu preferisse que fosse respondido por alguém que realmente entendesse esses sistemas.
Emil Jeřábek apoia Monica

Respostas:

18

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={f1=0 0,...,fk=0 0,h10 0,...,hm0 0},
, não tem solução comum em R n : uma refutação de S é dada por polinômiosf1,...,fk,h1,...,hmR[x1,...,xn]RnS e e I , j tal que - 1 = k i = 1 g i f i + I { 1 , , m } j e 2 IgEueEu,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(
()-1=Eu=1kgEufEu+Eu{1,...,m}jeEu,j2EuEuhEu.
RS , ou seja, g i f i e e 2 I , j Π i I h i .()gEufEueEu,j2EuEuhEu

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.ϕSxEu2-xEuxEuϕ

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

Emil Jeřábek apoia Monica
fonte
1
Existe um livro padrão?
1
Também existe algum uso da teoria dos modelos aqui?
2
Laserre tem um livro recente sobre os aspectos de otimização. "Uma introdução à otimização polinomial e semi-algébrica" ​​publicada pela Cambridge University Press.
Chandra Chekuri
11

p(x)0 0p(x)x

As regras de inferência são:

  1. x2-x0 0
  2. x-x20 0
  3. p(x)20 0
  4. p(x)0 0p(x)x0 0
  5. p(x)0 0p(x)(1-x)0 0
  6. p1(x)0 0,,pm(x)0 0Eu=1mcEupEu(x)0 0c1,,cmR+

p(x)20 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 :

Kaveh
fonte
Essa formulação é igual à de Emil? O seu é "dinâmico" e, portanto, permite provas do tipo DAG, onde o de Emil é "estático" e, portanto, parece corresponder a uma versão semelhante à sua. Portanto, aparentemente eles são diferentes em relação à complexidade (por exemplo, grau, tamanho em termos de número de monômios e número de linhas). Isso é verdade?
Iddo Tzameret 17/02/2014
@ Idd, acho que você está certo. Uma medida de complexidade pode não ser a mesma. Albert explica muito brevemente em sua palestra a correspondência para a principal e interessante medida de complexidade, se bem me lembro, mas se alguém estiver interessado em outras medidas, é necessário ter mais cuidado na formulação.
21414 Kaveh
@Kaveh Eu fiz duas perguntas relacionadas, se você puder ajudar, (1) cstheory.stackexchange.com/questions/30930/… (2) cstheory.stackexchange.com/questions/30932/…
user6818