在哈布雷（Habré）上，有几篇有关解决日语填字游戏的文章，作者提出了各种解决此类填字游戏的方法。 在文章“
用光速解决日语填字游戏”的评论中
，我建议由于解决日语填字游戏是一个NP完全问题，因此必须使用相应的工具SAT解算器来解决。 由于我的想法遭到怀疑，因此我决定尝试将其实施，并将结果与其他方法进行比较。 可以从削减中找到这件事。
如您所知，日语填字游戏或列线图是一种逻辑难题，您需要使用行标题左侧和列标题上方的数字将图像恢复为矩形。 这些数字对应于相应行或列中连续填充的单元的块的顺序和长度，并且在安装块时，它们之间必须至少有一个空单元。 在这里，我只考虑两种颜色的填字游戏，其中每个单元格都可以绘制或不绘制。 实际上，为了解决这个问题，必须找到每个块的位置。 应该注意的是，一项任务可以有一个或多个解决方案，也没有解决方案。 求解器还必须报告此情况。
不难理解，一般情况下该问题是详尽无遗的，许多应用程序的作者试图通过
编写自己的各种技巧来寻找最快的求解算法，而不是使用布尔可满足性问题中使用的完善方法。 但是，此声明需要证明，因此，我决定重新组合以普通形式解决日语填字游戏的问题，并使用著名的SAT解算器之一对其进行解决，以确认或驳斥它。
为了以合态范式表示此问题，我们为字段中的每个单元格引入一个布尔变量，为行和列中每个块的每个可能位置引入一个变量。 对于布尔字段的单元格，变量将表示给定单元格是否着色，对于布尔块的位置，变量将表示此块是否存在于此位置。 我们在变量（子句）之间编写必要的关系：
1.在行或列中声明的每个块必须至少出现在一个位置。 这对应于（X1 V X2 V ... XN）形式的子句，其中X1，X2 ... XN是该块在行或列中的所有可能位置。
2.行或列中的每个块不应出现多次。 这对应于格式（不是Xi）V（不是Xj）的许多子句，其中Xi，Xj（i！= J）是该块在行或列中的所有可能位置。
3.正确的块顺序。 由于必须保持正确的块排列顺序并消除它们的交集，因此有必要添加形式（不是Xi）V（不是Xj）的子句，其中Xi，Xj是对应于具有错误顺序或相交的不同块位置的变量。
4.染色的细胞必须包含在其位置包括该细胞的至少一个区域内。 这对应于形式为（（非Xk）V X1 V X2 ... XN）的子句，其中Xk是与该单元格相对应的变量，而X1，X2 ... XN是与包含该单元格的块位置相对应的变量。
5.每个空单元格都不应包含在单个块的任何可能位置。 这对应于许多形式为Xi V（不是Xj）的子句，其中Xi是对应于该单元的变量，而Xj是对应于包含该单元的任何块的一个位置的变量。
因此，该问题以合取范式的形式提出，可以使用SAT解算器解决。 此外，如果没有解决方案，则SAT求解器将确定没有解决方案。
现在是时候来确认或驳斥我的假设，即SAT解算器将比其他算法更快地处理日语填字游戏。 为了验证这一点，我从“
按数字绘制拼图难题调查”网站上获取了示例。 在此站点上，有一张表格，比较了各种应用程序解决日语填字游戏的速度，并提供了一系列好的示例-从每个人都可以解决的最轻巧的问题到只有一个应用程序可以解决的复杂问题的示例。 这些结果是在装有2.6GHz AMD Phenom II X4 810四核64位处理器，内存为8 Gb的计算机上获得的。 我使用了Intel®Core（TM）计算机i7-2600K CPU @ 3.40GHz内存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也仅由一个应用程序解决。
- SAT求解器可以轻松解决大多数应用无法解决的许多示例。
- 在大多数情况下，SAT求解器的求解时间比其他应用程序要好。
- 我使用了单线程SAT求解器，如果使用多线程SAT求解器，结果会更好。
- 使用SAT求解器时，无需发明自己的算法，而很有可能已经有人发明了自己的算法。
总之，我们可以补充说，SAT解算器可以接收多个解决方案（如果有）。 为此，添加一个形式为（（not X1）V（not X2）V ...（not XN））的子句，其中X1，X2 ... XN是对应于先前解决方案中已填充单元格的变量。