Apakah SAT-widthed decidable dalam logspace?

Elberfeld, Jakoby, dan Tantau 2010 ( ECCC TR10-062 ) membuktikan versi teorema Bodlaender yang hemat ruang. Mereka menunjukkan bahwa untuk grafik dengan treewidth paling banyak , dekomposisi pohon dengan lebar dapat ditemukan menggunakan ruang logaritmik. Faktor konstan dalam batas ruang tergantung pada . (Teorema Bodlaender menunjukkan batas waktu linier, dengan ketergantungan eksponensial pada dalam faktor konstan.)k k $k$$k$$k$$k$

SAT menjadi mudah ketika himpunan klausa memiliki lebar rendah. Secara khusus, Fischer, Makowsky, dan Ravve 2008 menunjukkan bahwa pemenuhan formula CNF dengan grafik insiden yang dibatasi oleh dapat diputuskan dengan operasi aritmatika maksimal ketika dekomposisi pohon diberikan. Dengan teorema Bodlaender, menghitung dekomposisi pohon dari grafik kejadian untuk tetap dapat dilakukan dalam waktu linier, dan oleh karena itu SAT dapat diputuskan untuk rumus treewidth terikat dalam waktu yang merupakan polinomial derajat rendah dalam jumlah variabel .2 O ( k ) n k $k$$2^{O(k)} n$$k$$n$

Orang kemudian dapat berharap bahwa SAT harus benar-benar dapat ditentukan menggunakan ruang logaritmik, untuk rumus dengan treewidth terikat dari grafik kejadian. Tidak jelas cara memodifikasi Fischer et al. pendekatan untuk memutuskan SAT menjadi sesuatu yang hemat ruang. Algoritma ini bekerja dengan menghitung ekspresi untuk sejumlah solusi, melalui inklusi-eksklusi, dan secara rekursif mengevaluasi jumlah solusi dari formula yang lebih kecil. Meskipun treewidth dibatasi tidak membantu, subformula tampaknya terlalu besar untuk dihitung dalam ruang logaritmik.

Ini membuat saya bertanya:

Apakah SAT untuk rumus treewidth terikat diketahui di atau ?N $\mathsf{L}$$\mathsf{NL}$

Memang, dengan menggunakan hasil di Elberfeld-Jakoby-Tantau-2010 orang dapat menunjukkan bahwa SAT dapat diputuskan dalam logspace pada formula yang grafik kejadiannya telah membatasi treewidth. Berikut ini adalah sketsa tentang bagaimana langkah-langkah utama pembuktian klaim ini berjalan.

1. Pengertian dekomposisi pohon dan treewidth dapat digeneralisasi ke struktur relasional yang sewenang-wenang. Lihat misalnya bagian 2 dan 3 makalah ini oleh Dalmau, Kolaitis dan Vardi.
2. Teorema Courcelle menyatakan bahwa logika MSO dapat diputuskan dalam waktu linier pada struktur relasional treewidth konstan.
3. Teorema Bodlaender menyiratkan bahwa jika suatu struktur relasional memiliki , maka dekomposisi pohon dari struktur tersebut dapat ditemukan dalam waktu . Dengan kata lain, dekomposisi semacam itu dapat ditemukan dalam waktu linier pada grafik treewidth konstan.f ( t ) ⋅ $t$$f(t)\cdot n$
4. Satu dapat menentukan struktur relasional cocok yang dapat digunakan untuk mengkodekan formula bersama-sama dengan grafik kejadian yang . Treewidth of paling banyak merupakan konstanta plus treewidth dari .F I τ $\tau$$F$$I$$\tau$$I$
5. Himpunan struktur relasional yang menyandikan rumus yang memuaskan + grafik kejadiannya dapat ditentukan MSO.$\tau$
6. Oleh karena itu, oleh teorema Bodlander + Courcelle, orang dapat memutuskan apakah formula treewidth konstan dapat dipenuhi dalam waktu linier.
7. Elberfeld-Jakoby-Tantau-2010 menunjukkan bahwa "waktu linier" dapat digantikan oleh "ruang logaritmik" pada teorema Bodlaender dan Courcelle.
8. Oleh karena itu, untuk setiap rumus MSO , dan setiap struktur relasional , seseorang dapat menentukan dalam ruang logaritmik apakah puas .$\varphi$τ $\tau$$\tau$$\varphi$
9. Secara khusus, SAT dapat ditentukan dalam logspace pada grafik treewidth konstan.