Система доказательства суммы квадратов

23

Недавно я видел несколько статей об arxiv, которые ссылаются на систему доказательств под названием сумма квадратов.

Может кто-нибудь объяснить, что такое доказательство суммы квадратов и почему такие доказательства важны / интересны?

Как они связаны с другими алгебраическими системами доказательств? Они что-то вроде двойника Лассере?

анонимное
источник
11
Краткий обзор есть в arxiv.org/abs/1211.1958 . Базовая система SOS определяется на странице 3 (ищите Григорьева и Воробьева).
Эмиль Йержабек поддерживает Монику
3
@ Эмиль, кажется, что статья содержит ответы на вопросы в посте (объясняет систему, ее историю и ее актуальность для последних работ), почему бы не опубликовать свой комментарий в качестве ответа?
Каве
@ EmilJeřábek Я приму ваш комментарий, если вы отправите расширенную версию в качестве ответа.
Аноним
2
Хорошо, я сделал это, хотя я бы предпочел, чтобы на него ответил кто-то, кто действительно понимает эти системы.
Эмиль Йержабек поддерживает Монику

Ответы:

18

Базовая система доказательства суммы квадратов, введенная Григорьевым и Воробьёвым под названием «Позитивстелленсатц опровержения» , представляет собой «статическую» систему доказательства, показывающую, что система полиномиальных уравнений и неравенств где f 1 , , f k , h 1 , ,

S={f1=0,,fk=0,h10,,hm0},
, не имеет общего решения в R n : опровержение S задается полиномами g i и e I , j, такими что - 1 = k i = 1 g i f i + I { 1 , , m } j e 2 If1,,fk,h1,,hmR[x1,,xn]RnSgieI,j (ВместоRможно работать с любым действительно замкнутым полем.) Positivstellensatz Стенгла гарантирует, чтоSимеет опровержение тогда и только тогда, когда у него нет решения. Основной мерой сложности здесь являетсястепеньопровержения, которая является максимумом всех степеней полиномов, которые появляются под знаками суммы в(), то естьgifiиe2I,jiIчя.
()1=i=1kgifi+I{1,,m}jeI,j2iIhi.
RS()gifieI,j2iIhi

Как обычно с алгебраическими системами доказательств, можно также рассматривать ее как систему опровержений для неудовлетворительных булевых формул , включив в S аксиомы x 2 i - x i для каждой переменной x i и перевод ϕ с помощью полиномиальных неравенств.ϕSxi2xixiϕ

Более подробную информацию об истории и развитии систем SOS можно найти по адресу http://arxiv.org/abs/1211.1958 .

Эмиль Йержабек поддерживает Монику
источник
1
Есть ли стандартная книга?
1
Также есть ли здесь применение теории моделей?
2
У Laserre есть недавняя книга по аспектам оптимизации. «Введение в полиномиальную и полуалгебраическую оптимизацию», опубликованное издательством Cambridge University Press.
Чандра Чекури
11

p(x)0p(x)x

Правила вывода:

  1. x2x0
  2. xx20
  3. p(x)20
  4. p(x)0p(x)x0
  5. p(x)0p(x)(1x)0
  6. p1(x)0,,pm(x)0i=1mcipi(x)0c1,,cmR+

p(x)20

Есть хорошие связи с полуопределенными алгоритмами программирования и аппроксимации.

Для получения дополнительной информации посмотрите недавний доклад Альберта Ацериаса на семинаре BIRS. Теоретические основы прикладного SAT-решения :

Кава
источник
Эта формулировка такая же, как у Эмиля? Твое "динамическое", и, следовательно, допускает DAG-подобные доказательства, где Эмиль "статичен", и, следовательно, кажется, соответствует твоей древовидной версии. Таким образом, по-видимому, они различаются по сложности (например, степень, размер с точки зрения количества мономов и количества строк). Это правда?
Иддо Цамерет
@ Идо, я думаю, ты прав. Мера сложности может не совпадать. Альберт очень кратко объясняет в своем выступлении соответствие для основной интересной меры сложности, если я правильно помню, но если кто-то интересуется другими мерами, тогда нужно быть более осторожным в формулировке.
Kaveh
@Kaveh Я могу задать два связанных вопроса, если вы можете помочь, (1) cstheory.stackexchange.com/questions/30930/… (2) cstheory.stackexchange.com/questions/30932/…
user6818