Nonogram et SAT Solver

Auteur

Joël Foutelet

Cet article montre une méthode de résolution logique des nonograms avec l'utilisation d'un SAT Solver

- Titre : Nonogram et SAT Solver

- Auteur : Joël Foutelet

- Parution : 3 mars 2015

- Licence : Les sources présentées sur cette page sont libres de droits et vous pouvez les utiliser à votre convenance. Par contre, la page de présentation constitue une œuvre intellectuelle protégée par les droits d'auteur. Copyright ® 2015 Joël Foutelet. Aucune reproduction, même partielle, ne peut être faite de ce site et de l'ensemble de son contenu : textes, documents, images, etc. sans l'autorisation expresse de l'auteur. Sinon vous encourez selon la loi jusqu'à trois ans de prison et jusqu'à 300 000 € de dommages et intérêts.

Sommaire

- Les nonograms

- A. Qu'est-ce qu'un nonogram

- B. Résolution d'un nonogram

- C. Les SAT Solvers

- D. Principe de la résolution des nonograms avec un SAT Solver

- E. Mise en oeuvre de la résolution avec SAT Solver

- E-1. Codage en Python des lignes pour le solveur

- E-2. Les contraintes sur les intervalles de cases blanches

- F. Complément : appel à un solveur externe.

- G. Quelques nonograms.

Les nonograms

A - Qu'est-ce qu'un nonogram

Un nonogram est un casse-tête logique consistant à remplir une grille avec des cases noires ou blanches. Des nombres sont listés sur les cotés de la grille indiquant le nombres de cases noires consécutives dans la rangée correspondante. Plus de détails sur les nonograms peuvent être trouvés ici.

Exemple de nonogram à résoudre :                  Nonogram résolu :

B - Résolution d'un nonogram

Des exemples de programmes de résolution de nonograms peuvent être trouvés ici

C - Les SAT Solvers

Un SAT solver est un logiciel permettant de décider si une formule logique est satisfiable, c'est-à-dire si on peut affecter des valeurs Vrai/Faux aux variables logiques en jeu de manière à ce que la formule soit vraie.

Exemples de formules logiques

- Si a est une variable logique, la formule a /\ ~a (a et non a) est fausse quelle que soit la valeur logique de a, la formule n'est pas "satisfiable".

- Si a et b sont des variables logiques la formule (a /\ b) \/ (a /\ ~b) est satisfiable, c'est à dire que par exemple pour a Vrai et B Faux , la formule est vraie.

Les formules logiques doivent être mises sous la forme CNF (Conjonctive Normal Form). Une Forme Normale Conjonctive est un ensemble de disjonctions (suites de OU), chaque disjonction étant connectée à la suivante par un ET.

Exemples de conjonctions

- A /\ B

- A \/ B

- A

- (A \/ B) /\ C

- (A \/ ~B \/ ~C) /\ (~D \/ E \/ F)

Contre exemples de conjonctions

- ~(A /\ B) car la négation s'applique à toute la parenthèse

- A /\ (B \/ (C /\ D)) car un "et" est imbriqué dans un "ou"

La mise en forme des formules pour la résolution par SAT Solver utilise la plus part du temps la codification DIMACS.

Format DIMACS

- Toute ligne débutant par "c" est un commentaire.

- La première ligne peut être p cnf nnn nnn, ce texte décrivant les paramètres, cnf indiquant que la formule est mise en forme conjonctive normale (chaque ligne est une suite de ou, les lignes représentent des et), le premier nombre est le nombre de variables logiques en jeu, le second est le nombre de lignes du fichier.

- Les autres lignes sont des suites de nombres positifs ou négatifs terminées par 0.

Le problème suivant (a /\ b /\ ~c) \/ (a /\ ~b) sera codé

p cnf 3 2
1 2 -3 0
1 -2 0

Le fichier fournit par le SAT Solver est composé généralement de deux lignes, la première est SAT ou UNSAT dont la signification est simple à comprendre. Si la deuxième ligne est présente, elle contient la liste des variables, une valeur positive signifie Vrai, négative signifie Faux. Le problème ci-dessus fournit à cryptominisat donne le fichier suivant

SAT
1 2 -3 0

Cela signifie que le problème possède (au moins) une solution, qui est a = Vrai, B = Vrai et C = faux.
On peut chercher une solution avec une valeur de variable donnée, par exemple en forçant la valeur de a à Faux :

p cnf 3 3
1 2 -3 0
1 -2 0
-1 0

on obtient

SAT
-1 -2 -3 0

Existe-t-il une solution avec a Faux et b Vrai ?

p cnf 3 4
1 2 -3 0
1 -2 0
-1 0
2 0

Résultat :

UNSAT

Pas de solution !

D - Principe de la résolution des nonograms avec un SAT Solver

Chaque case du nonogram est associée à une variable logique. Cette variable devra être positive si la case est noire, négative si elle est blanche.
Prenons l'exemple de la deuxième ligne du nonogram présenté plus haut. On voit qu'il y a deux séquences de deux cases noires pour une longueur totale de huit cases.
Il y a N possibilités de séquences de cases blanches entre les séquences de cases noires. On utilisera l2,N variables logiques pour décrire les différentes configurations de la deuxième ligne. Supposons que l2,i décrive la configuration suivante 2b, 2n, 1b, 2n, 1b. On appelle c2,i les cases de la deuxième ligne du nonogram.
On aura une liste d'implications :
l2,i Vrai => c2,0 Faux
l2,i Vrai => c2,1 Faux
l2,i Vrai => c2,2 Vrai
l2,i Vrai => c2,3 Vrai
l2,i Vrai => c2,3 Faux
....
....

Rappelons que l'implication a => b se traduit en CNF en ~a \/ b.
On obtient les formules suivantes :
l2,i Faux \/ c2,0 Faux
l2,i Faux \/ c2,1 Faux
l2,i Faux \/ c2,2 Vrai
l2,i Faux \/ c2,3 Vrai
l2,i Faux \/ c2,3 Faux
....
....

Elles se traduiront en DIMACS en :
-l2,i -c2,0 0
-l2,i -c2,1 0
-l2,i c2,2 0
-l2,i c2,3 0
-l2,i -c2,3 0
....
....

Concernant maintenant les différentes Li,j :
Au moins une doit être vraie, ceci peut se traduire par exemple par :
li,0 Faux => li,1 Vrai ou li,2 Vrai ou ...

Soit en langage DIMACS
li,0 li,1 li,2 .... 0

E - Mise en oeuvre de la résolution avec SAT Solver

Le langage utilisé ici est le Python (version 3.4.2 sous Windows 7 64 bits).
Pourquoi ce choix ? Python possède un interface vers le SAT Solver PICOSAT grâce à la bibliothèque Python EDA écrite par Chris Drake.
J'utiliserai aussi une bibliothèque de programmation par contraintes écrite par Gustavo Niemeyer.
Il y a sans doute beaucoup à redire à mon code, je ne connais Python que depuis très peu de temps, ce qui m'intéresse ici, c'est l'utilisation du solveur !
Je ne vais donc détailler que les points relatifs au codage de l'information pour celui-ci.

E-1 - Codage en Python des lignes pour le solveur

On s'intéresse ici au codage relatif aux lignes et aux colonnes. Il est identique dans les deux cas, seule différence les numéros de lignes et de colonnes sont inversés !
Je ne détaillerai donc que le codage des lignes.

Codage d'une ligne du nonogram

def calcul_des_lignes(LINES, NCOLUMNS, variables):
# Il est nécessaire de connaître le numéro de ligne
for l in range(len(LINES)) :
Noires = LINES[l]

# Nombres de séquences de cases noires de cette ligne
nb = len(Noires)

% total de cases noires sur la ligne
val = reduce(lambda x, y: x+y, Noires,0)

# obtention de toutes les possibilités de séquences de cases blanches
# ici on utilise la bibliothèque de contraintes
Lst = get_intervals(nb, NCOLUMNS - val)

# on mémorise la liste des variables logiques décrivant les configurations des case noires
conditions = []
for serie in Lst :
# numéro de colonne
c = 0

# création de la variable logique associées à la configuration
# de la ligne traitée dans la boucle qui suit
cond = variables.__next__()

# au moins une configuration doit exister
conditions.append(cond)

# on traite toutes les séquences de la configuration
Len = len(serie)
for s in range(Len) :
v = serie[s]
# la sequences de cases blanches (variables négatives)
for i in range(v) :
# cond Vrai => case blanche
# cond Faux ou case blanche
# en DIMACS -cond -valeur associée à la case
clauses.append([-cond, -x(l,c)])
c = c+1
# il y a une séquence de noires de moins que de blanches !
if s < Len - 1 :
# la sequences de cases noires (variables positives)
for i in range(Noires[s]) :
# cond Vrai => case noire
# cond Faux ou case noire
# en DIMACS -cond valeur associée à la case
clauses.append([-cond, x(l,c)])
c = c+1
# on ajoute la liste des conditions sur les variables logiques à la liste des clauses
clauses.append(conditions)

E-2 - Les contraintes sur les intervalles de cases blanches

On s'intéresse maintenant à l'obtention de toutes les possibilités de séquences de cases blanches dans une rangée.
On utilise une bibliothèque de contraintes pour les obtenir toutes.

Toutes les séquences de cases blanches

# calcul du nombre de possibilités de cases blanches sur une rangée
# c'est ici qu'une bibliothèque de contraintes est utile !
# les arguments passés sont le nombre d'intervalles à calculer et
# le maximum possible pour chaque intervalle
def get_intervals(Nb, Max) :
# Les variables en jeu sont nommées
# on est donc ici limité à un maximum de 25 séquences de cases noires sur une ligne !
all_keys = "abcdefghijklmnopqrstuvwxyz"

# On a besoin de listes de valeurs à associés à chaque variable
# Rappelons que les valeurs définies par le range s'arrètent à Max)
min = [i for i in range(Max+1)]
max = [i for i in range(1,Max+1)]
# création d'une instance de problème à résoudre
problem = Problem()

# Le premier intervalle peut être vide
# (les cases noires démarrent au bord de la grille)
problem.addVariable("a", min)

# Entre les cases noires, il faut au moins une case blanche
for i in range(1, Nb) :
problem.addVariable(all_keys[i], max)

# Le dernier intervalle peut être vide.
problem.addVariable(all_keys[Nb], min)

# La somme des cases noires doit être exactement Max.
problem.addConstraint(ExactSumConstraint(Max))

# on récupère les solutions
Res = problem.getSolutions()

# on met maintenant les solutions en forme pour les utiliser dans la suite du programme
# il existe sans doute une écriture plus idiomatique que celle que j'ai écrite
Resultat = []
for r in Res :
item = []
keys = list(r.keys())
for i in range(Nb+1) :
for u in keys :
if all_keys[i] == u :
item.append(r[u])
Resultat.append(item)

return Resultat

F - Complément : appel à un solveur externe.

L'appel au solveur se fait par sol = pycosat.solve(clauses).
Il peut arriver que la liste des clauses soit trop importante et que PICOSAT "explose". Je propose donc une solution alternative qui fait appel à un solveur externe. J'ai utilisé cryptominisat qui est assez rapide et compilable relativement facilement pour Windows. Il va sans dire que l'installation est beaucoup plus rapide sur Linux !
Voici les détails de l'appel, suivi de l'affichage du nonogram sur la console :

Appel à un solveur externe

# il faut écrire les clauses dans un fichier texte
with open("in-nono.txt", "w") as f:
#la ligne d'en tête décrivant le fichier
f.write('p cnf ' + str( numvariables ) +' '+ str( len(clauses))+'\n')
#chaque clause est écrite sur une ligne
# la liste des nombres séparés par un espace se termine par 0
for c in clauses:
f.write( " ".join(map(lambda x: str(x),c)))
f.write( " 0\n")

# appel au solveur
# on donne un fichier d'entrée et un fichier de sortie
# sinon la sortie est écrite sur le terminal
os.system('c:/windows/cryptominisat.exe in-nono.txt out-nono.txt')

# on lit le fichier de sortie
with open("out-nono.txt", "r") as f:
lines = list(f)
# s'il n'y a pas 2 lignes, c'est que le solveur n'a pas résolu le problème
if len(lines) != 2 :
print("Pas de solution")
else :
# la première ligne doit être "SAT"
assert lines[0] == "SAT\n"

# on récupère la liste des nombres
assignments = lines[1].split(" ")

# on ne gardera que les nombres positifs (vrais)
positives = []
for literal in assignments:
lit = int(literal)
if lit in reverse_xs and lit > 0:
(s,p) = reverse_xs[lit]
positives.append((s,p))

# affichage du nonogram
for l in range(len(LINES)) :
chars = list()
for c in range(len(COLUMNS)) :
# si on a un nombre positifs
# on affiche le "#"
if (l,c) in positives :
chars.append("#")
#sinon, c'est un "."
else :
chars.append(".")

# on affiche la ligne
print("".join(chars))

Le code source zyppé du programe Python est accessible ici.

G - Quelques nonograms.

Voici les différents nonograms définis dans le code.

>>>
une poule
Nombre de variables logiques : 202
Nombre de clauses logiques   : 1117

.###....
##.#....
.###..##
..##..##
..######
#.#####.
######..
....#...
...##...

Duree : 0.054 s

>>> main(1)
une figure
Nombre de variables logiques : 4515
Nombre de clauses logiques   : 82180

..........######....
........###.#..###..
...#..###...#....###
..###.##############
...#..#............#
..#.#.##..........##
#####..##........##.
#####...#........#..
#####..###.###.###..
########.###.###.###

Duree : 0.342 s

>>> main(2)
un animal
Nombre de variables logiques : 16943
Nombre de clauses logiques   : 386715

....................#####
..##..............###..##
.##..............#####..#
##.............########..
##....#####.###########..
#.#..##....#....######...
#..##.....#.......###....
##........#.............#
.##.....######.........##
..###############....####
.....##########..########
....##.#.####.###..######
........#################
........#################
.......##################
.......#...##############
.......#.#.##############
........#####...#########
.................########
..................#######

Duree : 1.350 s

>>> main(3)
lambda
Nombre de variables logiques : 512
Nombre de clauses logiques   : 4288

.##.......
#.##......
#..#......
...##.....
....#.....
...###....
...###....
..##.##...
..##..#...
.##...##.#
.##....###
##.....##.

Duree : 0.184 s