Ce projet consiste à résoudre le puzzle Binairo (voir ici un jeu en ligne), également appelé Takuzu, et décrit comme suit. Nous avons une grille de nxn cellules pouvant contenir un cercle blanc ou un cercle noir. La configuration initiale fournit certaines valeurs de cellules et le reste doit être rempli de cercles selon les règles suivantes :
Chaque ligne et chaque colonne doivent contenir le même nombre de cercles de chaque couleur, soit n/2 instances de chaque cas.
Il ne peut y avoir plus de 2 cercles consécutifs de la même couleur dans n'importe quelle direction (verticale ou horizontale).
Il ne peut pas y avoir deux lignes ou deux colonnes avec la même configuration.
Un exemple de configuration initiale et la solution correspondante sont visibles ci-dessous.
Il encodera le scénario à la fois comme problème SAT et comme programme ASP.
Cela prend un fichier ASCII avec la grille initiale où chaque cellule contient un caractère : '0' (un cercle blanc), '1' (un cercle noir) ou '.' (une cellule vide à remplir). La première ligne contient un nombre pair n>=2 précisant le nombre de lignes et de colonnes (nous avons une grille carrée). Par exemple, l'exemple de l'image ci-dessus serait représenté comme :
6
......
.11.0.
01....
....00
.1....
0..1..
Ce programme générera un fichier DIMACS et effectuera un appel externe à fermoir lorsqu'il utilise SAT ou à clingo lorsqu'il utilise ASP pour obtenir une solution. Il décodera également la sortie et imprimera la solution complète comme suit :
100110
011001
010011
101100
110010
001101
Par défaut, il utilise ASP et le dossier d'exemples contient un ensemble de benchmarks de différentes tailles (6, 8, 10, 14, 20), où domX.txt est le fichier d'entrée et solX.txt sa solution correspondante.
./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