Sistem bukti jumlah kotak

Baru-baru ini saya telah melihat beberapa artikel tentang arxiv yang merujuk pada sistem bukti yang disebut sum-of-square.

Dapatkah seseorang menjelaskan apa yang merupakan bukti jumlah kotak dan mengapa bukti semacam itu penting / menarik?

Bagaimana mereka terkait dengan sistem bukti aljabar lainnya? Apakah mereka semacam dualitas bagi Lassere?

Sistem bukti penjumlahan dasar, yang diperkenalkan dengan nama sanggahan Positivstellensatz oleh Grigoriev dan Vorobjov , adalah sistem bukti "statis" untuk menunjukkan bahwa seperangkat persamaan dan persamaan polinomial mana , tidak memiliki solusi umum dalam : sanggahan diberikan oleh polinomial dan sedemikian sehingga (Seseorang dapat bekerja dengan bidang yang benar-benar tertutup di tempatf 1 , ... , f k , h 1 , ... , h m ∈ R [ x 1 , ... , x n ] R n S g i e

$$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$$\mathbb R^n$$S$$g_i$- 1 = k ∑ i = 1 g i f i + ∑ I ⊆ { 1 , … , m } ∑ j e 2 I , j ∏ i ∈ I h i . $e_{I,j}$ $$\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$.) Positivstellensatz Stengle menjamin bahwa $S$ memiliki penolakan jika dan hanya jika ia tidak memiliki solusi. Ukuran kompleksitas utama di sini adalah tingkat sanggahan, yang merupakan maksimum dari total derajat polinomial yang muncul di bawah tanda penjumlahan dalam $(*)$ , yaitu, $g_if_i$ dan $e_{I,j}^2\prod_{i\in I}h_i$ .

Seperti biasa dengan sistem bukti aljabar, kita juga dapat menganggapnya sebagai sistem sanggahan untuk formula Boolean \ phi yang tidak memuaskan $\phi$dengan memasukkan dalam $S$ aksioma $x_i^2-x_i$ untuk setiap variabel $x_i$ , dan terjemahan $\phi$ oleh ketidaksetaraan polinomial.

Lebih lanjut tentang sejarah dan pengembangan sistem SOS dapat ditemukan di http://arxiv.org/abs/1211.1958 .

SOS dapat dianggap sebagai sistem bukti di mana garis-garis dalam bentuk mana adalah polinomial dalam variabel .$p(\vec{x}) \geq 0$$p(\vec{x})$$\vec{x}$

Aturan inferensi adalah:

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$ mana$c_1, \cdots, c_m \in \mathbb{R}^+$

Perbedaan utama dari sistem sebelumnya adalah bahwa kita memiliki aturan untuk .$p(\vec{x})^2\geq 0$

Ada koneksi bagus dengan pemrograman semidefinite dan algoritma aproksimasi.

Untuk informasi lebih lanjut, lihat pembicaraan Albert Atserias baru-baru ini di lokakarya BIRS. Theoretical Foundation of SAT Applied SAT Solving :

• Albert Atserias , Tutorial Mini tentang Sistem Bukti Semi-Aljabar ( slide ), 2014