Mencari Sumber Sastra untuk Mengikuti ide

12

Saya cukup yakin bahwa saya bukan yang pertama untuk menghibur gagasan bahwa saya akan hadir. Namun, akan sangat membantu jika saya dapat menemukan literatur yang terkait dengan ide tersebut.

Idenya adalah untuk membangun Mesin Turing M dengan properti bahwa jika P = NP maka M akan menyelesaikan 3-SAT dalam waktu polinomial. (Pilihan 3-SAT sewenang-wenang. Bisa jadi masalah apa pun di NP).

Untuk lebih jelasnya, ini bukan klaim bahwa P = NP. Bahkan, saya percaya sebaliknya. Saya hanya menyatakan bahwa jika P = NP, maka M akan memberikan solusi waktu polinomial. Jika Anda mencari solusi yang efisien, saya harus memperingatkan bahwa ini jauh dari efisien.

M dibangun sebagai berikut: pertama, asumsikan penyandian kanonik untuk semua Mesin Turing, dan terapkan penomoran pada mesin ini. Jadi, ada Mesin Turing nomor 1, angka 2, dll. Gagasan Mesin Turing Universal yang dapat membaca format untuk mesin yang disediakan dan kemudian mensimulasikan bahwa mesin itu berjalan pada input terpisah sudah cukup terkenal. M akan menggunakan Mesin Turing Universal untuk membuat dan mensimulasikan setiap Mesin Turing secara bergantian.

Ini pertama kali mensimulasikan menjalankan Turing Machine 1 untuk satu langkah.
Ini kemudian melihat output dari Mesin Turing 1.
Ini mensimulasikan menjalankan Mesin Turing 1 untuk dua langkah dan melihat output, kemudian mulai mensimulasikan Mesin Turing 2 untuk 2 langkah. Ini berlanjut dan loop dengan cara ini, pada gilirannya menjalankan Turing Machine 1 untuk langkah k kemudian 2 untuk langkah k ... lalu akhirnya mesin k untuk langkah k.

Setelah setiap simulasi dijalankan, ia memeriksa output dari menjalankan. Jika output adalah penugasan variabel yang memenuhi contoh masalah 3-SAT, M berhenti dalam keadaan terima. Jika di sisi lain, output adalah string bukti dalam beberapa bahasa bukti yang dapat diverifikasi dengan hasil terbukti bahwa instance masalah tidak memuaskan, M berhenti dalam keadaan tolak. (Untuk bahasa bukti, kita bisa misalnya, menggunakan Aksioma Peano dengan logika Orde Kedua dan aksioma logika gaya Hilbert dasar. Saya meninggalkannya sebagai latihan bagi pembaca untuk mengetahui bahwa jika P = NP, valid bahasa bukti ada dan polinomial-waktu dapat diverifikasi).

Saya akan mengklaim di sini bahwa M akan menyelesaikan 3-SAT dalam waktu polinomial jika dan hanya jika P = NP. Akhirnya, algoritma akan menemukan beberapa Mesin Turing ajaib dengan angka K, yang kebetulan menjadi pemecah yang efisien untuk masalah 3-SAT, dan mampu memberikan bukti hasil untuk keberhasilan atau kegagalan. K akhirnya akan disimulasikan menjalankan langkah poli (strlen (input)) untuk beberapa polinomial. Polinomial untuk M kira-kira adalah kuadrat dari polinomial untuk k dalam faktor terbesar, tetapi dengan beberapa konstanta mengerikan dalam polinomial.

Untuk mengulangi pertanyaan saya di sini: Saya ingin tahu apakah ada sumber literatur yang menggunakan ide ini. Saya agak kurang tertarik membahas ide itu sendiri.

Provinsi Bill
sumber

Jawaban:

16

Tampaknya ide ini dikaitkan dengan Levin (Ini disebut pencarian optimal). Saya percaya fakta ini sudah diketahui. Algoritma serupa dijelaskan dalam wikipedia misalnya, meskipun menggunakan masalah jumlah bagian. Dalam artikel ini dari scholarpedia Anda dapat menemukan beberapa referensi tentang subjek, termasuk pointer ke algoritma asli dan beberapa algoritma pencarian optimal lainnya.

φP=NPφ

Komentar 2: Seperti yang Jaroslaw Blasiok tunjukkan dalam jawaban lain, algoritma ini tidak memutuskan Sat hanya mengasumsikan P = NP.

Mateus de Oliveira Oliveira
sumber
Saya baru saja menemukan referensi Wikipedia, dan memang, itu menyebutkan Levin, tetapi tanpa kutipan. Mungkin ini hanya menjadi cerita rakyat tetapi tidak pernah digunakan dalam literatur yang diterbitkan. Bagaimanapun, ini sangat membantu. Terima kasih.
Bill Province
Selamat datang. Saya menemukan beranda dengan beberapa referensi tentang masalah ini. Saya mengedit jawaban untuk memasukkannya.
Mateus de Oliveira Oliveira,
6

Gagasan menjalankan semua mesin Turing secara diagonal sebelumnya telah digunakan oleh Leonid Levin dalam apa yang sekarang dikenal sebagai Levins Universal Search. Sayangnya, dan bertentangan dengan kesalahpahaman yang sangat umum, untuk apa yang saya tahu variasi pada pencarian universal Levins TIDAK mampu memberikan penyelesaian algoritma SAT yang eksplisit (masalah keputusan) dalam waktu polinomial, diberikan semata-mata asumsi bahwa P = NP - dan algoritma Anda tidak melakukannya .

Peringatan tentang alasan yang diajukan terletak (seperti sangat sering) dalam "latihan mudah diserahkan kepada pembaca" - Saya tidak dapat membuktikan latihan sendiri dan saya tidak percaya bahwa pernyataannya benar, yaitu:

Dengan asumsi P = NP, ada ukuran polinomial ZFC membuktikan ketidakpuasan dari formula Boolean yang diberikan.

Selain itu: Saya tidak bisa melihat bagaimana membuktikan keberadaan ZFC pendek polinomi terbukti tidak memuaskan di bawah asumsi (lebih kuat) bahwa "P = NP dapat dibuktikan dalam ZFC". Menjadi mudah namun dengan asumsi yang lebih kuat, yaitu:

(*) Ada mesin M yang berjalan dalam waktu polinomial yang terbukti memecahkan SAT.

Dan ini, saya percaya, asumsi yang benar di mana algoritma Anda memecahkan SAT dalam waktu polinomial. Di atas oleh "terbukti memecahkan SAT" Maksud saya: ada mesin M, dan bukti ZFC bahwa M memecahkan SAT.

Perhatikan bahwa asumsi ini masih sedikit lebih lemah daripada yang berikut: (**) Ada mesin M, yang terbukti berjalan dalam waktu polinomial dan terbukti memecahkan SAT.

Di bawah (**) orang dapat memiliki konstruksi eksplisit mencapai tujuan yang sama yang bahkan lebih sederhana: menghitung semua ZFC membuktikan sampai Anda menemukan mesin yang benar M (menghabiskan waktu konstan), dan kemudian jalankan M pada contoh yang diberikan.

Memang benar, bahwa dengan asumsi P = NP terdapat beberapa sistem bukti yang dapat diverifikasi secara polinomi dengan bukti pendek untuk ketidakpuasan formula yang diberikan. Sayangnya kami tidak mengetahui sistem pembuktian maupun verifikasi secara langsung, dan ini tidak membantu dalam pengaturan ini.

f1(x)

Perhatikan bahwa skema ini berlaku, misalnya, untuk masalah FAKTOR; di sini f hanya perkalian (didefinisikan hanya untuk faktor-faktor selain \ pm 1) dan B adalah pemeriksaan utama. Maka pencarian universal Levins akan menjadi (hingga faktor konstan) algoritma yang optimal untuk FAKTOR. Mengingat bahwa algoritma optimal lebih lambat daripada algoritma yang dikenal untuk pemeriksaan primarity - dalam kasus lain pemeriksaan primarity menjadi dominan.

NPcoNP

Jarosław Błasiok
sumber
1
Jika P = NP maka co-NP = co-P = P = NP. Jadi UNSATISFIABILITY ada di NP, jadi ada saksi seukuran polinomial - Anda tidak perlu menggunakan mesin Turing. Tidak bisakah Anda mengubah saksi itu menjadi bukti ZFC bahwa formula itu tidak memuaskan? Saya tidak mengerti mekanisme bukti ZFC tetapi intuisi yang saya terima dari berbagai tempat adalah bahwa, kecuali jika Anda berurusan dengan "hal-hal aneh", ZFC sesuai dengan semua hal yang Anda pikir dapat Anda buktikan, sebelum Anda mendengar tentang teori himpunan. Objek yang terbatas seperti formula Boolean dan saksi polinomial tentang ketidakpuasannya sepertinya tidak aneh.
David Richerby
Ya, jika P = NP, maka UNSAT adalah dalam NP, dan ia memiliki ukuran saksi polinomial. Yaitu: saksi ukuran nol, semua pekerjaan dilakukan oleh pemverifikasi, bukan? Saya hanya punya satu ide dalam pikiran bagaimana mengubah saksi ukuran nol ini menjadi ZFC membuktikan ketidakpuasan: memberikan bukti ZFC bahwa mesin saya benar-benar memecahkan UNSAT, dan kemudian menunjukkan rangkaian mesin ini pada formula - yang akan menjadi bukti yang valid, dan ini sesuai dengan fakta bahwa algoritma yang diusulkan oleh OP bekerja di bawah (*). Tetapi bagaimana jika ada beberapa mesin rumit yang kebetulan memecahkan SAT, tetapi fakta ini tidak dapat dibuktikan? Bukan berarti saya percaya itu yang terjadi
Jarosław Błasiok
1
Kesalahpahaman yang saya maksudkan adalah: "jika P = NP, maka Levins Universal Search memberikan algoritma waktu polinomial menyelesaikan masalah NP-complete" atau seperti yang kadang-kadang dinyatakan: "Tidak mungkin untuk hanya memiliki bukti nonkonstruktif P = NP, karena dari algoritma Levins ". Keduanya salah - formulasi Wikipedia menyajikan metode yang berhenti dalam polytime pada contoh-YES dari SUMU SUET, tetapi tidak berhenti sama sekali pada contoh-contoh TIDAK - itu bukan algoritma yang menentukan jumlah subset dalam polytime. Formulasi OP lebih baik untuk tujuan tersebut, tetapi membutuhkan asumsi yang lebih kuat daripada P = NP untuk memutuskan SAT dalam polytime.
Jarosław Błasiok
1
NPcoNP
1
Sekarang cara untuk mengatasi hal ini, karena Anda tidak tahu verifikasi secara eksplisit untuk masalah unSAT, akan mencoba untuk menemukan bukti singkat dalam beberapa logika formal yang sudah kita ketahui dan dapat memverifikasi (biarlah aksioma ZFC, atau Peano - kami adalah lebih mungkin untuk menemukan bukti singkat di yang sebelumnya), bahwa contoh ini tidak memuaskan. Tetapi jika seseorang ingin membuktikan bahwa ada bukti singkat dalam logika formal ini, seseorang perlu asumsi yang lebih kuat daripada P = NP.
Jarosław Błasiok