Binairo Puzzle
1.0.0
Dieses Projekt besteht in der Lösung des Binairo-Rätsels (siehe hier ein Online-Spiel), auch Takuzu genannt, und wie folgt beschrieben. Wir haben ein Gitter aus nxn Zellen, das einen weißen oder einen schwarzen Kreis enthalten kann. Die anfängliche Konfiguration stellt einige Zellwerte bereit und der Rest muss gemäß den folgenden Regeln mit Kreisen gefüllt werden:
Jede Zeile und jede Spalte muss die gleiche Anzahl an Kreisen jeder Farbe enthalten, d. h. n/2 Instanzen jedes Falls.
Es dürfen in keiner Richtung (vertikal oder horizontal) mehr als zwei aufeinanderfolgende Kreise derselben Farbe vorhanden sein.
Es dürfen keine zwei Zeilen oder zwei Spalten mit derselben Konfiguration vorhanden sein.
Ein Beispiel für die Erstkonfiguration und die entsprechende Lösung finden Sie unten.
Es wird das Szenario sowohl als SAT-Problem als auch als ASP-Programm kodieren.
Dazu wird eine ASCII-Datei mit dem Anfangsraster benötigt, in der jede Zelle ein Zeichen enthält: „0“ (ein weißer Kreis), „1“ (ein schwarzer Kreis) oder „.“ (eine leere Zelle, die gefüllt werden muss). Die erste Zeile enthält eine gerade Zahl n>=2, die die Anzahl der Zeilen und Spalten angibt (wir haben ein quadratisches Gitter). Das Beispiel im Bild oben würde beispielsweise wie folgt dargestellt werden:
6
......
.11.0.
01....
....00
.1....
0..1..
Dieses Programm generiert eine DIMACS-Datei und führt einen externen Aufruf an Klammer aus, wenn es SAT verwendet, oder Clingo, wenn es ASP verwendet, um eine Lösung zu erhalten. Außerdem wird die Ausgabe zurück dekodiert und die vollständige Lösung wie folgt gedruckt:
100110
011001
010011
101100
110010
001101
Standardmäßig wird ASP verwendet und der Beispielordner enthält eine Reihe von Benchmarks unterschiedlicher Größe (6, 8, 10, 14, 20), wobei domX.txt die Eingabedatei und solX.txt die entsprechende Lösung ist.
./binairo.py [-h] [-a] [-c input] input
-h show this help message and exit
-a use ASP to solve
-c compare the result with this file
-input route of the binairo puzzle instance
