Setelah saya menemukan permainan pentomino di mana perlu untuk menempatkan angka 13 ke dalam persegi 8 dengan 8. Setelah periode waktu tertentu ketika saya mencoba gagal untuk menyelesaikan masalah ini, saya memutuskan bahwa perlu untuk menulis sebuah program yang akan melakukan ini untuk saya. Untuk melakukan ini, perlu memilih algoritma solusi. Hal pertama yang terlintas dalam pikiran adalah algoritma cabang dan perbatasan yang biasa, ketika angka-angka ditumpuk satu sama lain berdekatan satu sama lain (algoritma dengan link menari tidak cocok di sini, karena angka-angka berbeda). Berbagai heuristik biasanya digunakan untuk mempercepat algoritme ini, misalnya bercabang dengan jumlah opsi paling sedikit. Anda dapat menemukan dan menerapkan heuristik lain dalam algoritma ini, tetapi di sini saya berpikir bahwa banyak trik berbeda untuk mempercepat solusi dari masalah tersebut telah diterapkan pada SAT solver. Oleh karena itu, perlu untuk menerjemahkan tugas ke dalam bahasa matematika yang sesuai dan menggunakan semacam solver SAT. Tentang bagaimana ini diterapkan dan apa hasil yang dihasilkan dapat dibaca di bawah potongan.
Pada awalnya saya ingin mengingatkan Anda apa permainan pentamino. Ini adalah bidang 8x8 persegi, yang harus diberi ubin dengan 13 angka - 12 coretan, yang terdiri dari 5 kotak dan satu angka 2x2:
Di sini perlu dikatakan apa masalah kepuasan Boolean atau masalah SAT. Secara umum, ini dapat dirumuskan sebagai temuan nilai-nilai variabel Boolean di mana ekspresi yang diberikan menjadi benar. Secara umum, ini adalah tugas lengkap NP, tetapi ada banyak trik yang membantu untuk menyelesaikannya secara efektif. Untuk melakukan ini, banyak aplikasi khusus yang disebut pemecah SAT telah dikembangkan. Saya akan menggunakan pemecah SAT bernama minisat. Untuk mengatasi masalah ini, perlu menulis ulang ekspresi input dalam bentuk normal konjungtif, yaitu, dalam bentuk produk dari jumlah variabel yang logis. Setiap braket dalam bentuk konjungtif normal di sini disebut klausa, yang merupakan "atau" logis beberapa literal, yaitu, variabel Boolean atau penolakannya. Sebagai contoh:
(x1 V bukan x3) (x2 V x4) (x2 V x3 V tidak X4)
Saya perlu menerjemahkan tugas pemasangan ke tugas SAT. Ambil beberapa figur pentamino dan letakkan di lapangan bermain dengan semua cara yang mungkin, termasuk shift, belokan dan refleksi. Untuk setiap posisi dari figur tersebut, kita mengaitkan variabel Boolean dan kita akan mengasumsikan bahwa jika dalam solusi akhir kita angka ini hadir dalam posisi khusus ini, maka variabel tersebut akan benar, dan jika tidak, maka false. Kami melakukan ini untuk semua angka.
Sekarang mari kita buat formula yang menggambarkan masalah kita, yaitu, kita akan benar-benar memberlakukan batasan pada variabel kita. Hal pertama yang harus dilakukan adalah memastikan bahwa semua sel di lapangan bermain kita akan ditutupi dengan setidaknya satu angka. Untuk melakukan ini, untuk setiap sel dari 64, kami menemukan semua angka dan posisi dari angka-angka ini yang menutupi sel ini dan menyusun klausa dari variabel yang ditugaskan ke posisi ini dari angka-angka. Hal kedua yang harus dilakukan adalah menghilangkan persimpangan bentuk. Ini dapat dilakukan dalam siklus ganda, cukup memilah semua posisi yang mungkin dari semua angka dan menentukan apakah pasangan memiliki sel yang sama. Jika ada, maka mereka berpotongan dan Anda perlu menambahkan klausa formulir (bukan x_i V bukan x_j), di mana x_i adalah variabel yang ditetapkan ke posisi pertama, dan x_j adalah posisi kedua. Klausa ini benar ketika x_i dan x_j tidak sama dengan satu pada saat yang sama, yaitu mengecualikan persimpangan. Dan akhirnya, hal ketiga yang perlu dipertimbangkan adalah bahwa setiap figur hanya dapat hadir di lapangan bermain satu kali. Untuk melakukan ini, kita juga melalui semua posisi masing-masing gambar dalam siklus ganda dan untuk setiap pasangan posisi dari angka yang sama kita membuat klausa yang mirip dengan yang sebelumnya dan terdiri dari dua negatif. Yaitu, ketika dua angka identik muncul (tetapi dalam posisi yang berbeda), salah satu klausa ini akan memberikan salah dan, karenanya, akan mengecualikan solusi semacam itu.
Itu semua teori, dan sekarang mari kita beralih ke praktik. Setiap gambar memiliki angka dari 1 hingga d untuk membedakannya dari yang lain dan mudah dicetak. Kemudian buat matriks dari lapangan bermain dan encode sel yang sesuai dari lapangan bermain sebagai ditempati / tidak ditempati oleh gambar:
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. 1 1 . . . . .
1 1 . . . . . .
. 1 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
2 . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
3 . . . . . . .
3 . . . . . . .
3 . . . . . . .
3 3 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
4 . . . . . . .
4 . . . . . . .
4 4 . . . . . .
. 4 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
5 5 . . . . . .
5 5 . . . . . .
5 . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
6 6 6 . . . . .
. 6 . . . . . .
. 6 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
7 . 7 . . . . .
7 7 7 . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
8 . . . . . . .
8 . . . . . . .
8 8 8 . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . 9 . . . . .
. 9 9 . . . . .
9 9 . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. a . . . . . .
aaa . . . . .
. a . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
b . . . . . . .
bb . . . . . .
b . . . . . . .
b . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. cc . . . . .
. c . . . . . .
cc . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
. . . . . . . .
dd . . . . . .
dd . . . . . .
Sekarang, untuk masing-masing bagian, perlu untuk menemukan semua posisi yang mungkin di lapangan bermain melalui pergeseran, belokan dan refleksi. Mari kita mulai dengan belokan dan refleksi. Secara total, ada 8 kemungkinan transformasi belokan dan refleksi, termasuk satu transformasi sepele yang membuat gambarnya utuh. Untuk transformasi ini, saya membuat 8 matriks yang sesuai, seperti yang ditunjukkan di bawah ini. Setelah rotasi atau refleksi, angka tersebut dapat melampaui bidang bermain, sehingga perlu mengembalikannya ke bidang bermain. Juga harus diperhitungkan bahwa beberapa tokoh dapat berubah menjadi diri mereka sendiri setelah transformasi, dan kasus-kasus seperti itu harus dikecualikan. Saya menambahkan opsi unik ke kelas Orientation. Hasilnya adalah kode berikut:
int dimension_ = 2; const unsigned int MATRIX_SIZE = dimension_ * dimension_; int * matrix = new int[ MATRIX_SIZE ]; for( unsigned int i = 0; i < MATRIX_SIZE; i++ ) { matrix[ i ] = 0; } for( unsigned int i = 0; i < dimension_; i++ ) { int * matrix1 = new int[ MATRIX_SIZE ]; std::copy( matrix, matrix + MATRIX_SIZE, matrix1 ); matrix1[ i ] = 1; for( unsigned int j = dimension_; j < 2 * dimension_; j++ ) { if( !matrix1[ j - dimension_ ] ) { int * matrix2 = new int[ MATRIX_SIZE ]; std::copy( matrix1, matrix1 + MATRIX_SIZE, matrix2 ); matrix2[ j ] = 1; unsigned int NUMBER = 1 << dimension_; for( unsigned int l = 0; l < NUMBER; l++ ) { int * matrix3 = new int[ MATRIX_SIZE ]; std::copy( matrix2, matrix2 + MATRIX_SIZE, matrix3 ); if( l & 1 ) { for( unsigned int l1 = 0; l1 < dimension_; l1++ ) { matrix3[ l1 ] = -matrix3[ l1 ]; } } if( l & 2 ) { for( unsigned int l1 = dimension_; l1 < 2 * dimension_; l1++ ) { matrix3[ l1 ] = -matrix3[ l1 ]; } } Orientation * orientation = new Orientation( figure ); for( std::vector<Point *>::const_iterator h = figure->points().begin(); h != figure->points().end(); ++h ) { const Point * p = *h; int x = 0; for( unsigned int i1 = 0; i1 < dimension_; i1++ ) { x = x + p->coord( i1 ) * matrix3[ i1 ]; } int y = 0; for( unsigned int i1 = 0; i1 < dimension_; i1++ ) { y = y + p->coord( i1 ) * matrix3[ dimension_ + i1 ]; } Point p1( x, y ); orientation->createPoint( p1.coord( 0 ), p1.coord( 1 ) ); } orientation->moveToOrigin(); if( isUnique( orientations, orientation ) ) { orientations.push_back( orientation ); } else { delete orientation; } delete [] matrix3; } delete [] matrix2; } } delete [] matrix1; }
Kode ini diterapkan untuk masing-masing gambar, dan kemudian, Orientasi unik yang diterima digeser sepanjang sumbu x dan y menciptakan semua posisi yang mungkin dari setiap gambar. Akibatnya, kami memiliki jumlah posisi berbeda berikut untuk masing-masing angka:
---------- Figure 1
Count = 288
---------- Figure 2
Count = 64
---------- Figure 3
Count = 280
---------- Figure 4
Count = 280
---------- Figure 5
Count = 336
---------- Figure 6
Count = 144
---------- Figure 7
Count = 168
---------- Figure 8
Count = 144
---------- Figure 9
Count = 144
---------- Figure a
Count = 36
---------- Figure b
Count = 280
---------- Figure c
Count = 144
---------- Figure d
Count = 49
Kemudian kami menetapkan variabel Boolean untuk setiap posisi yang memungkinkan dan membuat formula, seperti dijelaskan di atas. Setelah itu, kami memanggil minisat langsung dari aplikasi, yang mengembalikan solusi - satu set variabel kami dengan nilai yang diberikan benar atau salah. Mengetahui posisi mana variabel-variabel ini ditugaskan, kami mencetak solusinya:
bbbb 3 3 3 3
ddbc 8 8 8 3
dd 1 ccc 8 2
5 5 1 1 1 c 8 2
5 5 5 1 4 4 4 2
7 7 a 4 4 9 6 2
7 aaa 9 9 6 2
7 7 a 9 9 6 6 6
Apa selanjutnya
Tentu, untuk memikirkan ini tidak akan begitu menarik. Oleh karena itu, pertanyaan pertama yang muncul bagi saya adalah "berapa banyak solusi berbeda yang ada yang tidak berbeda dalam belokan sepele dan refleksi dari lapangan bermain?". Untuk melakukan ini, ada mode dalam pemecah SAT yang memungkinkan Anda untuk menambahkan klausa tanpa kehilangan informasi yang ada, yang secara signifikan mempercepat proses dibandingkan seolah-olah solusi dicari dari awal. Solusi berikut dapat ditemukan dengan menambahkan klausa yang berisi negasi dari semua variabel yang ada dalam solusi sebelumnya. Setelah menambahkan prosedur ini dan membandingkan solusi baru dengan yang sebelumnya, dengan mempertimbangkan belokan dan refleksi dari lapangan bermain, saya mendapat 1364 opsi berbeda.
Perpanjangan lain yang menarik yang saya terapkan adalah studi tentang berbagai bentuk lapangan dan tokoh lainnya. Dan akhirnya, studi bidang bermain tiga dimensi sangat menarik. Tapi ini topik untuk artikel lain.
Perbarui
Setelah menambahkan kondisi tambahan: untuk setiap angka dari satu klausa - harus ada setidaknya satu posisi angka ini di lapangan bermain, perhitungannya menjadi jauh lebih cepat. Selain itu, satu kesalahan telah diperbaiki, sebagai akibatnya jumlah semua opsi unik yang mungkin adalah 16146.