Di Habré ada beberapa artikel tentang cara memecahkan teka-teki silang Jepang, di mana penulis menemukan berbagai cara untuk menyelesaikan teka-teki silang semacam itu. Dalam komentar pada artikel
Memecahkan teka-teki silang warna Jepang dengan kecepatan cahaya, saya menyarankan bahwa karena menyelesaikan teka-teki silang Jepang adalah masalah NP-lengkap, mereka harus diselesaikan menggunakan alat yang sesuai, yaitu SAT solver. Karena ide saya disambut dengan skeptisisme, saya memutuskan untuk mencoba mengimplementasikannya dan membandingkan hasilnya dengan pendekatan lain. Apa yang datang dari ini dapat ditemukan di bawah luka.
Seperti yang Anda tahu, teka-teki silang atau nomogram Jepang adalah teka-teki logis di mana Anda harus mengembalikan gambar dalam persegi panjang menggunakan angka yang terletak di sebelah kiri di header baris dan di atas di header kolom. Angka-angka ini sesuai dengan urutan dan panjang blok sel yang berturut-turut diisi pada baris atau kolom yang sesuai, dan saat memasang blok, harus ada setidaknya satu sel kosong di antara mereka. Di sini saya hanya mempertimbangkan teka-teki silang dua warna, di mana setiap sel dapat dicat atau tidak. Bahkan, untuk mengatasi masalah ini, perlu untuk menemukan posisi setiap blok. Perlu dicatat bahwa tugas dapat memiliki satu atau beberapa solusi, dan juga tidak ada solusi sama sekali. Pemecah juga harus melaporkan ini.
Sangat mudah untuk memahami bahwa masalah dalam kasus umum adalah lengkap dan penulis berbagai aplikasi mencoba untuk menemukan algoritma solusi tercepat dengan
menulis sepeda mereka sendiri dari berbagai trik, daripada menggunakan metode yang dikembangkan dengan baik yang digunakan dalam masalah kepuasan Boolean. Namun, pernyataan ini membutuhkan bukti, jadi saya memutuskan untuk merumuskan kembali masalah pemecahan teka-teki silang Jepang dalam bentuk yang secara normal konjungtif dan menggunakan salah satu pemecah SAT yang terkenal untuk menyelesaikannya, untuk mengonfirmasi atau membantahnya.
Untuk mewakili masalah ini dalam bentuk konjungtif normal, kami memperkenalkan satu variabel Boolean untuk setiap sel di lapangan dan satu variabel untuk setiap posisi yang mungkin dari setiap blok dalam baris dan kolom. Untuk sel bidang Boolean, variabel akan berarti apakah sel yang diberikan berwarna atau tidak, dan untuk posisi blok Boolean, variabel akan berarti apakah blok ini hadir pada posisi ini atau tidak. Kami menulis hubungan yang diperlukan antara variabel (klausa):
1. Setiap blok yang dinyatakan dalam satu baris atau kolom harus muncul setidaknya dalam satu posisi. Ini sesuai dengan klausa formulir (X1 V X2 V ... XN), di mana X1, X2 ... XN adalah semua posisi yang mungkin dari blok ini dalam baris atau kolom.
2. Setiap blok di baris atau kolom harus muncul tidak lebih dari sekali. Ini sesuai dengan banyak klausa bentuk (bukan Xi) V (bukan Xj), di mana Xi, Xj (i! = J) adalah semua posisi yang mungkin dari blok ini dalam satu baris atau kolom.
3. Urutan blok yang benar. Karena perlunya mempertahankan urutan susunan balok yang benar, serta menghilangkan persimpangannya, maka perlu ditambahkan klausa bentuk (bukan Xi) V (bukan Xj), di mana Xi, Xj adalah variabel yang sesuai dengan posisi blok yang berbeda yang memiliki susunan atau persimpangan yang salah.
4. Sel bernoda harus terkandung dalam setidaknya satu blok yang posisinya termasuk sel ini. Ini sesuai dengan klausa bentuk ((bukan Xk) V X1 V X2 ... XN), di mana Xk adalah variabel yang sesuai dengan sel, dan X1, X2 ... XN adalah variabel yang sesuai dengan posisi blok yang berisi sel ini.
5. Setiap sel kosong tidak boleh terkandung dalam posisi yang memungkinkan dari satu blok. Ini sesuai dengan banyak klausa dari bentuk Xi V (bukan Xj), di mana Xi adalah variabel yang sesuai dengan sel, dan Xj adalah variabel yang sesuai dengan satu posisi dari setiap blok yang mengandung sel ini.
Dengan demikian, masalah dirumuskan dalam bentuk bentuk konjungtif normal dan dapat diselesaikan dengan menggunakan SAT solver. Selain itu, jika tidak ada solusi, pemecah SAT akan menentukan bahwa tidak ada solusi.
Sekarang saatnya untuk mengkonfirmasi atau membantah asumsi saya bahwa pemecah SAT akan mengatasi penyelesaian teka-teki silang Jepang lebih cepat daripada algoritma lainnya. Untuk memverifikasi ini, saya mengambil contoh dari situs web
Survey of Paint-by-Number Puzzle Solvers . Di situs ini terdapat tabel yang membandingkan kecepatan berbagai aplikasi untuk menyelesaikan teka-teki silang Jepang dan sekumpulan contoh yang bagus - dari yang paling ringan, yang diselesaikan oleh semua orang, hingga yang rumit, yang hanya diselesaikan oleh satu aplikasi. Hasil ini diperoleh pada komputer dengan prosesor 2.6GHz AMD AMD Phenom II X4 810 quad-core 64-bit Memory: 8 Gb. Saya menggunakan komputer Intel® Core (TM) i7-2600K CPU @ 3.40GHz Memory 16 Gb.
Akibatnya, saya mendapat hasil berikut:
======== sample-nin/webpbn-00001.nin ======== Start read data. 16 lines were read Solver started. vars = 150 Clauses = 562 SATISFIABLE apsnono finished. real 0m0,610s user 0m0,004s sys 0m0,002s ========= sample-nin/webpbn-00006.nin ======== Start read data. 41 lines were read Solver started. vars = 1168 Clauses = 10215 SATISFIABLE apsnono finished. real 0m0,053s user 0m0,028s sys 0m0,000s ========= sample-nin/webpbn-00016.nin ======== Start read data. 69 lines were read Solver started. vars = 7484 Clauses = 191564 SATISFIABLE apsnono finished. real 0m0,368s user 0m0,186s sys 0m0,008s ========= sample-nin/webpbn-00021.nin ======== Start read data. 40 lines were read Solver started. vars = 1240 Clauses = 11481 SATISFIABLE apsnono finished. real 0m0,095s user 0m0,034s sys 0m0,000s ========= sample-nin/webpbn-00023.nin ======== Start read data. 22 lines were read Solver started. vars = 311 Clauses = 1498 SATISFIABLE apsnono finished. real 0m0,147s user 0m0,006s sys 0m0,000s ========= sample-nin/webpbn-00027.nin ======== Start read data. 51 lines were read Solver started. vars = 2958 Clauses = 38258 SATISFIABLE apsnono finished. real 0m0,089s user 0m0,050s sys 0m0,010s ========= sample-nin/webpbn-00065.nin ======== Start read data. 75 lines were read Solver started. vars = 7452 Clauses = 134010 SATISFIABLE apsnono finished. real 0m0,272s user 0m0,166s sys 0m0,009s ========= sample-nin/webpbn-00436.nin ======== Start read data. 76 lines were read Solver started. vars = 6900 Clauses = 134480 SATISFIABLE apsnono finished. real 0m0,917s user 0m0,830s sys 0m0,005s ========= sample-nin/webpbn-00529.nin ======== Start read data. 91 lines were read Solver started. vars = 10487 Clauses = 226237 SATISFIABLE apsnono finished. real 0m0,286s user 0m0,169s sys 0m0,005s ========= sample-nin/webpbn-00803.nin ======== Start read data. 96 lines were read Solver started. vars = 9838 Clauses = 278533 SATISFIABLE apsnono finished. real 0m0,827s user 0m0,697s sys 0m0,008s ========= sample-nin/webpbn-01611.nin ======== Start read data. 116 lines were read Solver started. vars = 25004 Clauses = 921246 SATISFIABLE apsnono finished. real 0m3,467s user 0m3,301s sys 0m0,084s ========= sample-nin/webpbn-01694.nin ======== Start read data. 96 lines were read Solver started. vars = 13264 Clauses = 391427 SATISFIABLE apsnono finished. real 0m0,964s user 0m0,822s sys 0m0,016s ========= sample-nin/webpbn-02040.nin ======== Start read data. 116 lines were read Solver started. vars = 26445 Clauses = 1182535 SATISFIABLE apsnono finished. real 0m7,512s user 0m7,354s sys 0m0,122s ========= sample-nin/webpbn-02413.nin ======== Start read data. 41 lines were read Solver started. vars = 1682 Clauses = 15032 SATISFIABLE apsnono finished. real 0m0,258s user 0m0,053s sys 0m0,001s ========= sample-nin/webpbn-02556.nin ======== Start read data. 111 lines were read Solver started. vars = 11041 Clauses = 340630 SATISFIABLE apsnono finished. real 0m0,330s user 0m0,136s sys 0m0,009s ========= sample-nin/webpbn-02712.nin ======== Start read data. 95 lines were read Solver started. vars = 13212 Clauses = 364416 SATISFIABLE apsnono finished. real 0m6,503s user 0m6,365s sys 0m0,032s ========= sample-nin/webpbn-03541.nin ======== Start read data. 111 lines were read Solver started. vars = 19249 Clauses = 676595 SATISFIABLE apsnono finished. real 0m5,008s user 0m4,785s sys 0m0,100s ========= sample-nin/webpbn-04645.nin ======== Start read data. 121 lines were read Solver started. vars = 19159 Clauses = 793580 SATISFIABLE apsnono finished. real 0m4,739s user 0m4,477s sys 0m0,107s ========= sample-nin/webpbn-06574.nin ======== Start read data. 51 lines were read Solver started. vars = 2932 Clauses = 33191 SATISFIABLE apsnono finished. real 0m0,231s user 0m0,176s sys 0m0,000s ========= sample-nin/webpbn-06739.nin ======== Start read data. 81 lines were read Solver started. vars = 10900 Clauses = 256833 SATISFIABLE apsnono finished. real 0m0,782s user 0m0,730s sys 0m0,008s ========= sample-nin/webpbn-07604.nin ======== Start read data. 111 lines were read Solver started. vars = 18296 Clauses = 478535 SATISFIABLE apsnono finished. real 0m1,524s user 0m1,324s sys 0m0,026s ========= sample-nin/webpbn-08098.nin ======== Start read data. 39 lines were read Solver started. vars = 1255 Clauses = 10950 SATISFIABLE apsnono finished. real 0m0,216s user 0m0,133s sys 0m0,000s ========= sample-nin/webpbn-09892.nin ======== Start read data. 91 lines were read Solver started. vars = 13887 Clauses = 419787 SATISFIABLE apsnono finished. real 0m12,048s user 0m11,858s sys 0m0,088s ========= sample-nin/webpbn-10088.nin ======== Start read data. 116 lines were read Solver started. vars = 23483 Clauses = 1020515 SATISFIABLE apsnono finished. real 0m17,472s user 0m16,795s sys 0m0,321s ========= sample-nin/webpbn-10810.nin ======== Start read data. 121 lines were read Solver started. vars = 25726 Clauses = 895436 SATISFIABLE apsnono finished. real 0m0,898s user 0m0,562s sys 0m0,026s ========= sample-nin/webpbn-12548.nin ======== Start read data. 88 lines were read Solver started. vars = 13685 Clauses = 486012 SATISFIABLE apsnono finished. real 3m1,682s user 2m58,537s sys 0m1,507s ========= sample-nin/webpbn-18297.nin ======== Start read data. 79 lines were read Solver started. vars = 9708 Clauses = 272394 SATISFIABLE apsnono finished. real 0m16,643s user 0m16,326s sys 0m0,210s ========= sample-nin/webpbn-22336.nin ======== Start read data. 159 lines were read Solver started. vars = 67137 Clauses = 5420886 SATISFIABLE apsnono finished. real 1m46,555s user 1m43,336s sys 0m3,075s
Kesimpulan apa yang bisa ditarik dari ini?
- Pemecah SAT memecahkan semua contoh yang dipecahkan oleh aplikasi lain, bahkan webpbn-22336, yang diselesaikan dengan hanya satu aplikasi.
- Pemecah SAT dengan mudah memecahkan banyak contoh yang tidak dapat diselesaikan oleh sebagian besar aplikasi.
- Dalam kebanyakan kasus, waktu solusi lebih baik untuk pemecah SAT daripada untuk aplikasi lain.
- Saya menggunakan pemecah SAT single-threaded, jika Anda menggunakan pemecah SAT multi-threaded, hasilnya akan lebih baik.
- Saat menggunakan solver SAT, tidak perlu menemukan algoritma Anda sendiri, yang sudah, dengan probabilitas tinggi, diciptakan seseorang.
Sebagai kesimpulan, kita dapat menambahkan bahwa pemecah SAT dapat menerima lebih dari satu solusi, jika ada. Untuk melakukan ini, tambahkan satu klausa bentuk ((bukan X1) V (bukan X2) V ... (bukan XN)), di mana X1, X2 ... XN adalah variabel yang sesuai dengan sel yang diisi dalam solusi sebelumnya.