Ingin tahu tentang bukti kelengkapan NP yang dibantu komputer

Dalam makalah "KOMPLEKSITAS MASALAH KEPUASAN" oleh Thomas J. Schaefer, penulis telah menyebutkan bahwa

This raises the intriguing possibility of computer-assisted NP-completeness proofs. Once the researcher has established the basic framework for simulating conjunctions of clauses, the relational complexity could be explored with the help of a computer. The computer would be instructed to randomly generate various input configurations and test whether the defined relation was non-affine, non-bijunctive, etc.

Tentu saja, ini adalah batasan:

The fruitfulness of such an approach remains to be proved: the enumeration of the elements of a relation on lO or 15 variables is Surely not a light computational task.

Saya ingin tahu itu

1. Apakah ada penelitian lanjutan dalam mengembangkan gagasan "bukti kelengkapan NP berbantuan komputer" ini? Apa yang paling mutakhir (mungkin khusus untuk atau )? Karena Schaefer telah mengusulkan gagasan bukti Kelengkapan NP "berbantuan komputer" (setidaknya untuk pengurangan dari ), apakah ini berarti ada beberapa prinsip / struktur umum yang mendasari pengurangan ini (untuk yang dari atau )? Jika demikian, apakah mereka? $\textsf{3SAT}$SAT 3SAT$\textsf{3-Partition}$
   $\textsf{SAT}$$\textsf{3SAT}$$\text{3-Partition}$
2. Adakah yang punya pengalaman dalam membuktikan kelengkapan NP dengan asisten komputer? Atau adakah yang bisa membuat contoh buatan?

Sedangkan untuk pertanyaan 2, setidaknya ada dua contoh bukti yang melibatkan asisten komputer.$NP$

Erickson dan Ruskey memberikan bukti berbantuan komputer bahwa Domino Tatami Covering adalah NP-complete. Mereka memberikan pengurangan waktu polinomial dari planar 3-SAT ke penutup domino tatami. SAT-solver (Minisat) digunakan untuk mengotomatiskan penemuan gadget dalam pengurangan. Tidak ada bukti lainnya yang diketahui.$NP$

Ruepp dan Holzer membuktikan bahwa puzzle pensil Kakuro adalah -complete. Beberapa bagian dari bukti dihasilkan secara otomatis menggunakan SAT-solver (sekali lagi Minisat).N $NP$$NP$

Dalam tulisan ini, saya menunjukkan bahwa jika untuk beberapa ada grafik dengan derajat maksimum dan kekuatan tepi kromatik benar-benar lebih besar dari , maka -lengkap untuk memutuskan apakah kekuatan tepi kromatik paling banyak adalah . Grafik tersebut dikenal untuk dan saya melakukan pencarian komputer untuk menemukan grafik teks yang cocok untuk .k k Θ p 2 k k > 3 12 k = $k\geq 3$$k$$k$$\Theta_2^p$$k$$k>3$$12$$k=3$

Kompleksitas kekuatan kromatik dan kekuatan tepi kromatik. Kompleksitas Komputasi, 14 (4): 308-340, 2006

Dari komentar di atas:

Saya menggunakan perpustakaan Choco Java untuk pemrograman Constraint untuk memeriksa perilaku yang benar dari gadget yang digunakan untuk membuktikan NP-kelengkapan dari teka-teki berikut: Binary Puzzle, Tents, Rolling cube puzzle tanpa sel bebas, Net. Saya belum punya waktu untuk menerbitkannya, tetapi draft makalah tersedia di blog saya.

$0$$1$$n \times n$

(A) gerbang logika (AND + OR) dan tautan, jika kita ingin menggunakan PLANAR SAT sebagai sumber masalah NPC; atau

(B) simpul derajat 3 di mana tepatnya 1 pintu masuk dan 1 pintu keluar dapat diaktifkan secara bersamaan, jika kita ingin menggunakan HAMILTONIAN CYCLE pada grafik kotak sebagai sumber masalah NPC (perhatikan bahwa dalam kasus ini, harus ada yang lain kondisi yang memaksa "jalur terhubung").

Dalam kedua kasus kami menggunakan konfigurasi awal yang memperbaiki batas gadget (untuk melarang interaksi yang tidak diinginkan) dan kami mengizinkan interaksi antara dua gadget yang berdekatan hanya melalui elemen pusat (atau grup elemen). Konfigurasi elemen pusat tersebut harus mewakili nilai logika dalam kasus (A) atau traversal dalam kasus (B).

Misalnya untuk memodelkan sebuah DAN:

***C***   *=fixed elements (initial config. of the puzzle)
*xxxxx*   x=internal logic (some elements can be fixed,
AxxxxxB     other must be completed/traversed)
*xxxxx*   A,B,C=elements shared with adjacent gadgets
*******

Pada titik ini untuk memeriksa gadget menggunakan pemecah SAT (lebih baik menggunakan CPL) cukup untuk menerapkan aturan teka-teki, kemudian memeriksa kepuasan ketika A, B, C mengambil semua kombinasi nilai yang mungkin; dan melihat apakah mereka konsisten dengan perilaku yang diinginkan. Misalnya dalam kasus AND, dalam semua konfigurasi gadget yang valid (memuaskan) di mana C benar (C menunjukkan nilai logika true), baik A dan B harus benar.

Jika gadget sangat rumit (misalnya dalam teka-teki Rolling cube) saya pikir itu adalah satu-satunya cara untuk memastikan bahwa mereka bekerja dengan benar (dan bahwa bukti NPC benar).

Saya melakukan hal ini - bukti kelengkapan NP berbantuan komputer - dalam tesis sarjana saya!

Bagian yang buruk - ini dalam bahasa Rusia dan tidak diterjemahkan ke bahasa Inggris. http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf

Saya bekerja dengan gerbang logis dalam masalah 2D. Rencananya adalah:

• Secara manual desain seperti apa "kawat" dalam masalah Anda.
• Gunakan pencarian yang sangat cerdas dan dioptimalkan (sebenarnya pemrograman dinamis di atas set profil) untuk secara otomatis merancang semua gerbang logis yang diperlukan.
• KEUNTUNGAN!

Kode tersedia, dengan cara: https://code.google.com/p/metadynamic-programming/

Dengan cara ini, dengan kerja manual hanya untuk mendesain kawat dan mengkode aturan masalah 2D spesifik, saya dapat membuktikan NP-kelengkapan:

• Kapal penyapu ranjau
• Meliputi area dengan domino horisontal dan trimino vertikal
• $k$$k \ge 4$$k \in [4,6]$

si penanya telah mengindikasikan bahwa dia baik-baik saja dengan interpretasi yang lebih luas dari pernyataan Schaefer dalam sebuah jawaban. secara kebetulan telah mengumpulkan tautan untuk blog tentang topik terdekat & akan menulis beberapa di sini.

pernyataan asli (bagian 7 hal.225) jelas dalam maksudnya seperti yang diilustrasikan dengan contoh pengurangan NP lengkap dari 2 pencocokan sempurna yang dapat berwarna dari 7.1 menggunakan "dikotomi thm" 2.1.

$F(x)$

$F(x)$$x$

mengambil pov luas ide-ide umum ini dapat dilihat telah tumbuh & dieksplorasi di banyak bidang penelitian sejak 1978 ini renungan / "ide benih" yang mengarah ke seluruh cabang besar dan program penelitian, masih berlangsung, tidak ada yang ada di hampir segala bentuk pada saat penulisan makalah Schaefers. 1 ^st satu ide umum adalah analisis empiris dari NP sifat kelengkapan via misalnya generator / pemecah / analisis .

• area penelitian terbesar yang muncul di sini adalah ke dalam contoh-contoh SAT acak dan melihat kinerja SAT solver pada mereka yang mengarah pada penemuan titik transisi pada pertengahan 1990-an, yang kemudian terbukti memiliki koneksi mendalam ke fisika statistik dan aspek yang tampaknya ada di mana-mana / intrinsik / fundamental. / karakteristik semua masalah NP lengkap. ada sangat banyak makalah di daerah ini & sekarang beberapa buku. lihat mis. Informasi, fisika, dan Komputasi Mezard / Montanari

• Mengurai masalah kepuasan atau Menggunakan grafik untuk mendapatkan wawasan yang lebih baik tentang masalah kepuasan , Herwig 2006 (83pp). ini adalah pendekatan yang agak baru yang diterbitkan penelitian lain yang melihat struktur variabel-klausa instance SAT yang dihasilkan dan menganalisis struktur / metrik mereka untuk menemukan korelasi dengan kekerasan.

• seseorang dapat mengambil masalah konjektur-sulit dan menyandikannya sebagai instance SAT & kemudian memeriksa strukturnya atau menjalankan solver SAT pada mereka & mengamati perilaku dinamis dari solver SAT. itu tidak mudah untuk mengetahui kapan ini dilakukan pertama tetapi kasus awal adalah dengan anjak piutang, mungkin pada pertengahan 1990-an, dan contoh-contoh ini muncul dalam kontes pemecah DIMACS SAT. sayangnya ini belum tentu dianggap sebagai hasil penelitian yang dapat diterbitkan secara terpisah pada saat itu. ada kiasan dalam beberapa makalah SAT.

  lihat misalnya Memuaskan ini: Sebuah Mencoba di Memecahkan Perdana faktorisasi menggunakan satisfiability pemecah oleh Stefan Schoenmackers, Anna Cavender dan juga pertanyaan cs.se mengurangi masalah faktorisasi integer untuk masalah NP lengkap & (ada beberapa terkait / tersebar (T) CS stackexchange pertanyaan lain di ini).

2 ^nd lain yang modern umumnya ide / benih yang melekat dalam pernyataan tua Schaefers yang menyerang masalah hard algoritmik atau matematika secara umum dengan mengkonversi mereka untuk SAT contoh, dan menggunakan off-the-rak (tapi state-of-the-art) SAT pemecah (yaitu Pemecahan SAT dapat dianggap secara luas sebagai salah satu kasus paling awal dalam logika / matematika dari teorema otomatis komputer yang membuktikan di mana solusi rumus SAT seperti "teorema", meskipun diakui pov modern yang mungkin telah agak bergeser) dan ada beberapa yang terkenal baru-baru ini sukses di depan ini.

• yang masalah Erdos Kesenjangan yang berkaitan dengan batas-batas di jalan-jalan random sangat sulit dan kemajuan terbatas dengan pendekatan analitik, dan novel / belum pernah terjadi sebelumnya, pendekatan empiris dengan SAT baru-baru ini diambil untuk mencapai beberapa hasil kunci pada masalah terbuka terkait, dirayakan oleh banyak orang sebagai terobosan benar. serangan SAT terhadap dugaan ketidaksesuaian Erdos Konev, Lisitsa

• penelitian tentang jaringan penyortiran yang optimal telah berlangsung puluhan tahun dan ada masalah alam terbuka yang sulit pada ukuran minimal jaringan untuk mengurutkan sejumlah elemen. dalam beberapa tahun terakhir telah ada kemajuan besar baru-baru ini dalam mengonversikannya menjadi instance SAT & menjalankan solver standar. Batas Baru pada Jaringan Penyortiran Optimal Ehlers, Müller, juga mengutip karya terbaru lainnya.