Apakah ada algoritma waktu linear non-deterministik untuk CNF-SAT?

Masalah keputusan CNF-SAT dapat digambarkan sebagai berikut:

Input: Rumus boolean $\phi$ dalam bentuk normal konjungtif.

Pertanyaan: Apakah ada tugas variabel yang memenuhi ? $\phi$

Saya sedang mempertimbangkan beberapa pendekatan berbeda untuk memecahkan CNF-SAT dengan mesin Turing dua-tape non-deterministik .

Saya percaya bahwa ada NTM yang memecahkan CNF-SAT dalam langkah . $n \cdot \texttt{poly}(\log(n))$

Pertanyaan: Apakah ada NTM yang memecahkan CNF-SAT dalam langkah ? $O(n)$

Setiap referensi yang relevan dihargai bahkan jika mereka hanya menyediakan pendekatan waktu non-deterministik dekat waktu linear.

time-complexity sat turing-machines np nondeterminism Michael Wehar
sumber

Santhanam pada tahun 2001 menulis: "SAT NTIME ( polylog ), hasil yang mengikuti dari fakta bahwa SAT dapat diterima dalam waktu polylog pada NRAM dan bahwa ada simulasi NRAM yang efisien oleh NTM, karena Gurevich dan Shelah. " Jadi sepertinya tidak mungkin bagi saya bahwa SAT NTIME ( ) diketahui. (Rujukannya adalah untuk LNCS 363 dari 1989.)

\in

$\in$

n

$n$

(n)

$(n)$

n

$n$

(n)

$(n)$

\in

$\in$

n

$n$

András Salamon

@ Boson, asumsikan bahwa Anda tidak hanya diberikan tugas yang memuaskan tetapi juga perhitungan lengkap dari rumus. Bagaimana Anda memeriksa apakah itu perhitungan yang valid dalam waktu linier? Tidak jelas bahkan Anda dapat melakukannya untuk 3CNF-SAT karena Anda harus melompat-lompat untuk mencari tugas ke variabel.

Kaveh

@ Boson Tidak jelas apakah Anda dapat memverifikasi bahwa tugas memenuhi rumus dalam waktu linier dengan TM dua-tape. Anda mungkin harus memindahkan kepala kaset bolak-balik berkali-kali. Jika Anda memiliki pendekatan yang efisien untuk verifikasi ini, beri tahu saya. :)

Michael Wehar

Hanya sebuah catatan: jika variabel diwakili dalam unary (SAT masih NPC), maka ada dua kaset NTM yang mengakui formula memuaskan unary

dalam

langkah

φ

$\varphi$

2 | φ |

$2|\varphi|$

Marzio De Biasi

@MichaelWehar jika Anda menggunakan jenis penghitungan, Anda dapat mengurutkan n kunci dalam rentang [0, k] dalam waktu O (n + k) dalam model akses acak yang masuk akal (mis. Mesin Turing akses acak, di mana Anda dapat mengambil O (log n) waktu untuk menuliskan indeks, kemudian dapat melompat ke indeks rekaman itu dalam 1 langkah). Jika Anda menyandikan setiap literal sebagai string (log n + 1) bit, maka jumlah klausa dan variabel paling banyak adalah O (n / log n), dalam hal ini O (log n) - operasi waktu pada semua literal baik-baik saja. Memperluas dua pita TM tidak mudah, setidaknya dengan jenis penghitungan.

Ryan Williams

Jawaban:

Ini hanya komentar panjang. Beberapa kali yang lalu saya bertanya (sendiri :-) seberapa cepat NTM multitape yang menerima bahasa NP-complete (cukup dikodekan). Saya datang dengan ide ini:

3-SAT tetap NP-lengkap bahkan jika variabel diwakili dalam unary. Secara khusus kita dapat mengkonversi klausul - kira - dari 3-SAT rumus sewenang-wenang pada variabel dan klausa dalam urutan karakter lebih alfabet di mana setiap kejadian variabel diwakili dalam unary: $(x_i \lor \neg x_j \lor x_k)$ $\varphi$ $n$ $m$ $\Sigma = \{ +, -, 1 \}$

$+ 1^{i} 0,- 1^{j} ,+ 1^{k}$

Misalnya, dapat dikonversi menjadi: $(x_2 \lor -x3 \lor +4)$

+110-1110+11110

Jadi kita dapat mengonversi rumus 3-SAT dalam string ekuivalen menyatukan klausa-klausa. Bahasa adalah NP-complete. $\varphi_i$ $U(\varphi_i)$ $L_U = \{ U(\varphi_i) \mid \varphi_i \in 3-SAT \}$

2-tape NTM dapat memutuskan apakah string dalam waktu lewat sini. $x \in L_U$ $2|x|$

kepala pertama memindai input dari kiri ke kanan dan dengan logika internal, ia melacak ketika masuk atau keluar klausa atau mencapai akhir rumus. Setiap kali ia menemukan atau , head kedua mulai bergerak ke kanan dengan itu pada yang mewakili . Pada akhir , jika head kedua pada maka ia menebak nilai kebenaran atau (itu membuat tugas) dan menulisnya di kaset kedua; jika ia menemukan atau maka variabel tersebut telah diberi nilai; $+$ $-$ $1^i$ $x_i$ $1^i$ $0$ $+$ $-$ $+$ $-$
dalam kedua kasus, menggunakan logika internal, NTM cocok dengan nilai kebenaran di bawah kepala kedua (penugasan) dengan terakhir terlihat atau ; jika mereka cocok maka klausa terpenuhi; $+$ $-$
kemudian kepala kedua dapat kembali ke sel paling kanan;
dengan logika internal NTM dapat melacak jika semua klausa terpenuhi sementara kepala pertama bergerak ke akhir input.

Contoh:

Tape 1 (formula)    Tape 2 (variable assignments)
+110-1110+11110...  0000000000000...
^                   ^
+110-1110+11110...  0000000000000...
 ^                  ^
+110-1110+11110...  0000000000000...
  ^                  ^
+110-1110+11110...  0+00000000000... first guess set x2=T; matches +
  ^                  ^               so remember that current clause is satisfied
+110-1110+11110...  0+00000000000... 
  ^                  ^
...
+110-1110+11110...  0+00000000000... 
    ^               ^
...
+110-1110+11110...  0++0000000000... second guess set x3=T
       ^              ^              don't reject because current
                                     clause is satisfied (and in every
                                     case another literal must be parsed)

Waktu dapat dikurangi menjadi jika kita menambahkan beberapa simbol berlebihan ke representasi klausa: $|x|$

$+ 1^{i} 0^i,- 1^{j} 0^j ,+ 1^{k} 0^k \; ... \; \text{+++}$

( menandai akhir formula) $\text{+++}$

Dengan cara ini kepala kedua dapat kembali ke sel paling kiri sementara yang pertama memindai bagian . Menggunakan sebagai pembatas klausa dan sebagai penanda untuk akhir rumus kita bisa menggunakan representasi yang sama untuk rumus CNF dengan jumlah literal per klausa yang sewenang-wenang. $0^i$ $\text{++}$ $\text{+++}$

Marzio De Biasi
sumber

Representasi unary tidak ambigu, sehingga orang dapat menggunakan 0/1 untuk +/-, memberikan 011011110111110 untuk contoh pertama Anda. 00 kemudian berfungsi sebagai penanda akhir klausa, karena 000 tidak dapat terjadi (jika 00 terjadi, maka itu adalah penanda akhir variabel dan tanda berikutnya, jadi simbol berikutnya harus 1). Worktape tunggal berisi tugas

bit yang ditebak ke variabel

. Ketika variabel dibaca, head worktape bergerak maju dan kemudian dipindahkan kembali ke awal ketika angka 0 terlihat, jadi paling banyak

langkah untuk setiap bit input.

v

$v$

v

$v$

2

$2$

András Salamon

Dengan kata lain, bahkan NDTM dengan pita input satu arah dan satu worktape menggunakan paling banyak

langkah untuk Unary SAT yang dikodekan dengan alfabet Boolean.

2 n

$2n$

András Salamon

Untuk membuat segala sesuatunya lebih rapi, seseorang selanjutnya dapat meminta bahwa input pertama berisi awalan dengan jumlah variabel

ditentukan dalam unary. Ini memungkinkan tebakan dibuat saat membaca awalan. Ini kemudian semacam pengkodean "unary SATLIB", dengan ukuran paling banyak kuadrat dalam contoh SAT standar, selama setiap variabel muncul setidaknya satu kali dalam rumus dan variabel diberi nomor 0 hingga

. Ini tampaknya persyaratan yang masuk akal.

v

$v$

v - 1

$v-1$

András Salamon

@ AndrásSalamon: bagus! Memperbaiki pengkodean dan model (pita satu arah baca + pita kerja 2 arah) kita dapatkan runtime terburuk

pada input ukuran

, di mana

dapat dibuat secara sewenang-wenang besar dengan menyematkan beberapa penyimpanan tetap dalam logika internal TM . Mungkin menarik untuk menyelidiki apakah sesuatu dapat dibuktikan dengan menggunakan satu arah input-tape dan argumen crossing-section.

2 n - c

$2n - c$

n

$n$

c

$c$

Marzio De Biasi

Ya, sejauh yang saya tahu produk ruang-waktu untuk Unary SAT adalah sesuatu seperti

dengan argumen standar. Representasi variabel unary menghindari kesenjangan antara batas bawah

paling dikenaldan batas atas

batas atas untuk CNF-SAT (meskipun algoritme yang lebih baik dalam hal itu mungkin juga dapat mengurangi kesenjangan).

Θ (n \sqrt{n})

$\Theta(n\sqrt{n})$

Ω (n^{2} / (\log n)^{1 + ε})

$\Omega(n^2/(\log n)^{1+\varepsilon})$

O (n^{3} / (\log n)^{ε^{'}})

$O(n^3/(\log n)^{\varepsilon'})$

András Salamon

Bukan apa yang Anda cari, tetapi untuk NTM 1-tape, jawabannya tampaknya negatif: SAT tidak dapat dipecahkan oleh NTM 1-tape dalam waktu linear non-deterministik.

Menurut makalah ini (Teorema 4.1), kelas bahasa reguler adalah kelas bahasa yang dikenali oleh 1-tape NTM dalam waktu . Jadi, jika ada 1-tape NTM penyelesaian SAT dalam waktu , maka SAT (lebih tepatnya, himpunan rumus yang memuaskan di CNF) akan menjadi bahasa biasa, maka dapat dipecahkan dalam ruang konstan deterministik. $REG$ $o(n \log(n))$ $o(n \log(n))$

Boson
sumber

Teorema itu hanya sekitar satu kepala mesin Turing.

$\:$ (Misalnya, mesin Turing dua-kepala dapat dengan mudah memutuskan bahasa palindrom dalam waktu linier dan ruang konstan.)

$\;\;\;\;$

Ini bagus! Terima kasih banyak. Tapi, saya paling tertarik dengan case dua-tape. :)

Michael Wehar

Seperti yang ditulis @Ricky. AFAIK masih konsisten dengan apa yang kita ketahui bahwa SAT berada dalam waktu linier deterministik. Untuk membuktikan sebaliknya, Anda akan memerlukan batas waktu lebih rendah untuk SAT dan kami tidak memilikinya (sepertinya tidak dekat dengan satu).

Kaveh