Lösen Sie japanische Kreuzworträtsel mit SAT Solver

Auf Habré gab es mehrere Artikel zum Lösen japanischer Kreuzworträtsel, in denen die Autoren verschiedene Möglichkeiten zur Lösung solcher Kreuzworträtsel entwickelten. Im Kommentar zum Artikel Lösen japanischer Farbkreuzworträtsel mit Lichtgeschwindigkeit schlug ich vor, dass das Lösen japanischer Kreuzworträtsel ein NP-vollständiges Problem darstellt und daher mit dem entsprechenden Tool, dem SAT-Löser, gelöst werden muss. Da meine Idee auf Skepsis stieß, beschloss ich, sie umzusetzen und die Ergebnisse mit anderen Ansätzen zu vergleichen. Was dabei herauskam, ist unter dem Schnitt zu finden.

Wie Sie wissen, ist ein japanisches Kreuzworträtsel oder Nomogramm ein logisches Rätsel, bei dem Sie das Bild in einem Rechteck wiederherstellen müssen, indem Sie die Zahlen links in den Zeilenüberschriften und oben in den Spaltenüberschriften verwenden. Diese Nummern entsprechen der Reihenfolge und Länge der Blöcke aufeinanderfolgend gefüllter Zellen in der entsprechenden Zeile oder Spalte. Bei der Installation von Blöcken muss mindestens eine leere Zelle zwischen ihnen sein. Hier betrachte ich nur zweifarbige Kreuzworträtsel, bei denen jede Zelle entweder übermalt werden kann oder nicht. Um dieses Problem zu lösen, ist es tatsächlich notwendig, die Position jedes Blocks zu finden. Es ist zu beachten, dass eine Aufgabe eine oder mehrere Lösungen sowie überhaupt keine Lösungen haben kann. Der Solver muss dies ebenfalls melden.

Es ist leicht zu verstehen, dass das Problem im Allgemeinen erschöpfend ist und die Autoren zahlreicher Anwendungen versuchen, den schnellsten Lösungsalgorithmus zu finden, indem sie ihre eigenen Fahrräder mit verschiedenen Tricks schreiben , anstatt die gut entwickelten Methoden zu verwenden, die im Booleschen Erfüllbarkeitsproblem verwendet werden. Diese Aussage erfordert jedoch Beweise, daher habe ich beschlossen, das Problem der Lösung des japanischen Kreuzworträtsels in einer konjunktiv normalen Form neu zu formulieren und es mit einem der bekannten SAT-Löser zu lösen, zu bestätigen oder zu widerlegen.

Um dieses Problem in konjunktiv normaler Form darzustellen, führen wir eine Boolesche Variable für jede Zelle im Feld und eine Variable für jede mögliche Position jedes Blocks in Zeilen und Spalten ein. Für eine Zelle eines Booleschen Feldes bedeutet eine Variable, ob eine bestimmte Zelle farbig ist oder nicht, und für eine Position eines Booleschen Blocks bedeutet eine Variable, ob dieser Block an dieser Position vorhanden ist oder nicht. Wir schreiben die notwendigen Beziehungen zwischen den Variablen (Klauseln):

1. Jeder in einer Zeile oder Spalte deklarierte Block muss mindestens an einer Position erscheinen. Dies entspricht einer Klausel der Form (X1 V X2 V ... XN), wobei X1, X2 ... XN alle möglichen Positionen dieses Blocks in einer Zeile oder Spalte sind.

2. Jeder Block in einer Zeile oder Spalte sollte nur einmal vorkommen. Dies entspricht vielen Klauseln der Form (nicht Xi) V (nicht Xj), wobei Xi, Xj (i! = J) alle möglichen Positionen dieses Blocks in einer Zeile oder Spalte sind.

3. Die richtige Reihenfolge der Blöcke. Da es notwendig ist, die korrekte Reihenfolge der Anordnung von Blöcken beizubehalten und deren Schnittpunkt zu beseitigen, müssen Klauseln der Form (nicht Xi) V (nicht Xj) hinzugefügt werden, wobei Xi, Xj Variablen sind, die den Positionen verschiedener Blöcke entsprechen, die die falsche Reihenfolge haben oder sich schneiden.

4. Eine gefärbte Zelle muss in mindestens einem Block enthalten sein, dessen Position diese Zelle enthält. Dies entspricht einer Klausel der Form ((nicht Xk) V X1 V X2 ... XN), wobei Xk die der Zelle entsprechende Variable ist und X1, X2 ... XN die Variablen sind, die den Positionen der Blöcke entsprechen, die diese Zelle enthalten.

5. Jede leere Zelle sollte nicht an einer möglichen Position eines einzelnen Blocks enthalten sein. Dies entspricht vielen Klauseln der Form Xi V (nicht Xj), wobei Xi die der Zelle entsprechende Variable ist und Xj die Variable ist, die einer Position eines Blocks entspricht, der diese Zelle enthält.

Somit wird das Problem in Form einer konjunktiv normalen Form formuliert und kann unter Verwendung des SAT-Lösers gelöst werden. Wenn es keine Lösung gibt, stellt der SAT-Löser außerdem fest, dass es keine Lösung gibt.

Jetzt ist es an der Zeit, meine Annahme zu bestätigen oder zu widerlegen, dass der SAT-Löser die Lösung japanischer Kreuzworträtsel schneller als andere Algorithmen bewältigen kann. Um dies zu überprüfen, habe ich Beispiele von der Website der Umfrage zu Puzzle-Lösern nach Anzahl genommen . Auf dieser Website finden Sie eine Tabelle, in der die Geschwindigkeit verschiedener Anwendungen zum Lösen japanischer Kreuzworträtsel und eine Reihe guter Beispiele verglichen werden - von den leichtesten, die von jedem gelöst werden können, bis zu komplexen, die nur eine Anwendung löst. Diese Ergebnisse wurden auf einem Computer mit einer 2,6-GHz-CPU AMD Phenom II X4 810 Quad-Core-64-Bit-Prozessor erhalten. Speicher: 8 GB. Ich habe einen Intel® Core (TM) Computer i7-2600K CPU mit 3,40 GHz Speicher 16 GB verwendet.

Als Ergebnis habe ich folgende Ergebnisse erhalten:

======== 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 

Welche Schlussfolgerungen können daraus gezogen werden?

1. Der SAT-Löser hat alle Beispiele gelöst, die von anderen Anwendungen gelöst werden, sogar webpbn-22336, das nur von einer Anwendung gelöst wird.
2. Der SAT-Löser löst leicht viele Beispiele, die von den meisten Anwendungen nicht gelöst werden können.
3. In den meisten Fällen ist die Lösungszeit für den SAT-Solver besser als für andere Anwendungen.
4. Ich habe einen Single-Threaded-SAT-Solver verwendet. Wenn Sie einen Multi-Threaded-SAT-Solver verwenden, sind die Ergebnisse sogar noch besser.
5. Bei Verwendung des SAT-Lösers müssen keine eigenen Algorithmen erfunden werden, die bereits mit hoher Wahrscheinlichkeit von jemandem erfunden wurden.

Abschließend können wir hinzufügen, dass der SAT-Solver gegebenenfalls mehr als eine Lösung erhalten kann. Fügen Sie dazu eine Klausel der Form ((nicht X1) V (nicht X2) V ... (nicht XN)) hinzu, wobei X1, X2 ... XN die Variablen sind, die den gefüllten Zellen in der vorherigen Lösung entsprechen.