Este proyecto consiste en resolver el rompecabezas de Binairo (ver aquí un juego online), también llamado Takuzu, y que se describe a continuación. Tenemos una cuadrícula de nxn celdas que pueden contener un círculo blanco o un círculo negro. La configuración inicial proporciona algunos valores de celda y el resto se debe rellenar con círculos según las siguientes reglas:
Cada fila y cada columna debe contener la misma cantidad de círculos de cada color, es decir, n/2 instancias de cada caso.
No puede haber más de 2 círculos consecutivos del mismo color en cualquier dirección (vertical u horizontal).
No puede haber dos filas o dos columnas con la misma configuración.
A continuación se puede ver un ejemplo de configuración inicial y la solución correspondiente.
Codificará el escenario como un problema SAT y como un programa ASP.
Esto toma un archivo ASCII con la cuadrícula inicial donde cada celda contiene un carácter: '0' (un círculo blanco), '1' (un círculo negro) o '.' (una celda vacía para llenar). La primera línea contiene un número par n>=2 que especifica el número de filas y columnas (tenemos una cuadrícula cuadrada). Por ejemplo, el ejemplo de la imagen de arriba se representaría como:
6
......
.11.0.
01....
....00
.1....
0..1..
Este programa generará un archivo DIMACS y realizará una llamada externa a cloche cuando use SAT o clingo cuando use ASP para obtener una solución. También decodificará la salida e imprimirá la solución completa de la siguiente manera:
100110
011001
010011
101100
110010
001101
Por defecto, usa ASP y la carpeta de ejemplos contiene un conjunto de puntos de referencia de diferentes tamaños (6, 8, 10, 14, 20), donde domX.txt es el archivo de entrada y solX.txt su solución correspondiente.
./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