ご存知のように、日本語のクロスワードまたはノモグラムは、行ヘッダーの左側と列ヘッダーの上の数字を使用して長方形の画像を復元する必要がある論理パズルです。 これらの番号は、対応する行または列の連続して埋められたセルのブロックの順序と長さに対応し、ブロックをインストールするとき、それらの間に少なくとも1つの空のセルが必要です。 ここでは、各セルを塗りつぶすか塗りつぶさないかの2色のクロスワードのみを検討します。 実際、この問題を解決するには、各ブロックの位置を見つける必要があります。 タスクには1つまたは複数のソリューションがあり、ソリューションもまったくないことに注意してください。 ソルバーはこれも報告する必要があります。
一般的な場合の問題は網羅的であり、多くのアプリケーションの作成者は、ブール充足可能性問題で使用されるよく開発された方法を使用する代わりに、さまざまなトリックの
この問題を連言的に正規の形式で表現するために、フィールドの各セルに1つのブール変数を、行と列の各ブロックの可能な位置ごとに1つの変数を導入します。 ブールフィールドのセルの場合、変数は特定のセルが色付きかどうかを意味し、ブールブロックの位置の場合、変数はこのブロックがこの位置に存在するかどうかを意味します。 変数（節）間に必要な関係を書きます：
1.行または列で宣言された各ブロックは、少なくとも1つの位置に表示される必要があります。 これは、（X1 V X2 V ... XN）という形式の節に対応します。ここで、X1、X2 ... XNはすべて、このブロックの行または列の可能な位置です。
2.行または列の各ブロックは、1回しか表示されません。 これは、フォーム（Xiではない）V（Xjではない）の多くの句に対応します。ここで、Xi、Xj（i！= J）は、行または列のこのブロックのすべての可能な位置です。
3.ブロックの正しい順序。 ブロックの正しい配列順序を維持し、それらの交差を排除する必要があるため、（Xiではなく）V（Xjではない）という形式の節を追加する必要があります。
4.染色された細胞は、位置にこの細胞が含まれる少なくとも1つのブロック内に含まれている必要があります。 これは、（（Xkではない）V X1 V X2 ... XN）という形式の節に対応します。ここで、Xkはセルに対応する変数であり、X1、X2 ... XNはこのセルを含むブロックの位置に対応する変数です。
5.各空のセルは、単一ブロックの可能な位置に含まれてはなりません。 これは、Xi V（Xjではない）の形式の多くの節に対応します。Xiはセルに対応する変数であり、Xjはこのセルを含むブロックの1つの位置に対応する変数です。
したがって、問題は連接正規形の形式で定式化され、SATソルバーを使用して解決できます。 さらに、解決策がない場合、SATソルバーは解決策がないと判断します。
さて、SATソルバーが他のアルゴリズムよりも速く日本のクロスワードを解決するという私の仮定を確認または反論する番です。 これをテストするために、Paint by by Number Puzzle Solversの Webサイトから例を取り上げました。 このサイトには、日本語のクロスワードを解決するためのさまざまなアプリケーションの速度と、すべての人が解決できる最も軽いものから、1つのアプリケーションのみが解決する複雑なものまでの優れた例の比較表があります。 これらの結果は、2.6 GHz CPU AMD Phenom II X4 810クアッドコア64ビットプロセッサを搭載したコンピューターで取得されました。メモリ：8 Gb。 Intel®Core（TM）コンピューターi7-2600K CPU @ 3.40GHz Memory 16 Gbを使用しました。
その結果、次の結果が得られました。
======== 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
これからどのような結論を導き出すことができますか？
- SATソルバーは、他のアプリケーションで解決されるすべての例を解決しました。webpbn-22336も、1つのアプリケーションだけで解決されます。
- SATソルバーは、ほとんどのアプリケーションでは解決できない多くの例を簡単に解決します。
- ほとんどの場合、SATソルバーのソリューション時間は、他のアプリケーションよりも優れています。
- マルチスレッドSATソルバーを使用している場合、結果はさらに良くなります。
- SATソルバーを使用する場合、独自のアルゴリズムを発明する必要はありません。アルゴリズムは、すでに高い確率で発明されています。
結論として、SATソルバーは、もしあれば複数のソリューションを受け取ることができると付け加えることができます。 これを行うには、（（X1ではない）V（X2ではない）V ...（XNではない））という形式の句を1つ追加します。ここで、X1、X2 ... XNは前のソリューションの塗りつぶされたセルに対応する変数です。