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.
- 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 (OU) chaque disjonction étant connectée à la suivante par une conjonction. (ET).
- A /\ B
- A \/ B
- A
- (A \/ B) /\ C
- (A \/ ~B \/ ~C) /\ (~D \/ E \/ F)
- ~(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. Cette codification est très simple :
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 cnf, c'est à dire une suite de lignes "et", chaque ligne étant une suite de "ou", 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 EDABibliothèque PyEDA é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 solver !
import time
import itertools
import pycosat
from functools import *
from constraint import *
##############################################
# déclaration des variables globales
# déclaration de la liste des clauses
# qui seront passées au serveur
clauses = []
# dict pour la mémorisation des données
xs = dict()
reverse_xs = dict()
# fin de la déclaration des variables globales
##############################################
# une petite facilité d'écriture
def x(l,c):
return xs[(l,c)]
# calcul du nombre de possilités de cases blanches sur une rangée
# c'est ici qu'une bibliothèque de contraintes est utile !
def get_intervals(Nb, Max) :
all_keys = "abcdefghijklmnopqrstuvwxyz"
min = [i for i in range(Max+1)]
max = [i for i in range(1,Max+1)]
problem = Problem()
problem.addVariable("a", min)
for i in range(1, Nb) :
problem.addVariable(all_keys[i], max)
problem.addVariable(all_keys[Nb], min)
problem.addConstraint(ExactSumConstraint(Max))
Res = problem.getSolutions()
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
def affiche(sol, NLINES, NCOLUMNS):
positives = []
for literal in sol:
lit = int(literal)
if lit in reverse_xs and lit > 0:
(s,p) = reverse_xs[lit]
positives.append((s,p))
for l in range(NLINES) :
chars = list()
for c in range(NCOLUMNS) :
if (l,c) in positives :
chars.append("#")
else :
chars.append(".")
print("".join(chars))
print("\n")
def calcul_des_lignes(LINES, NCOLUMNS, variables):
for l in range(len(LINES)) :
Noires = LINES[l]
nb = len(Noires)
val = reduce(lambda x, y: x+y, Noires,0)
Lst = get_intervals(nb, NCOLUMNS - val)
conditions = []
for serie in Lst :
c = 0
cond = variables.__next__()
conditions.append(cond)
Len = len(serie)
for s in range(Len) :
v = serie[s]
for i in range(v) :
clauses.append([-cond, -x(l,c)])
c = c+1
if s < Len - 1 :
for i in range(Noires[s]) :
clauses.append([-cond, x(l,c)])
c = c+1
clauses.append(conditions)
def calcul_des_colonnes(COLUMNS, NLINES, variables) :
for c in range(len(COLUMNS)) :
Noires = COLUMNS[c]
nb = len(Noires)
val = reduce(lambda x, y: x+y, Noires,0)
Lst = get_intervals(nb, NLINES - val)
conditions = []
for serie in Lst :
l = 0
cond = variables.__next__()
conditions.append(cond)
Len = len(serie)
for s in range(Len) :
v = serie[s]
for i in range(v) :
clauses.append([-cond, -x(l,c)])
l = l+1
if s < Len - 1 :
for i in range(Noires[s]) :
clauses.append([-cond, x(l,c)])
l = l+1
clauses.append(conditions)
def charge(fig) :
if fig == 0 :
Mes = "une poule"
LIGNES = [[3], [2,1], [3,2], [2,2], [6], [1,5], [6], [1], [2]]
COLONNES = [[1,2], [3,1], [1,5], [7,1], [5], [3], [4], [3]]
elif fig == 1 :
Mes = "une figure"
LIGNES = [[6], [3, 1, 3], [1, 3, 1, 3], [3, 14], [1, 1, 1], [1, 1, 2, 2], [5, 2, 2], [5, 1, 1], [5, 3, 3, 3], [8, 3, 3, 3]]
COLONNES = [[4], [4], [1, 5], [3, 4], [1, 5], [1], [4, 1], [2, 2, 2], [3, 3], [1, 1, 2], [2, 1, 1], [1, 1, 2], [4, 1], [1, 1, 2], [1, 1, 1], [2, 1, 2], [1, 1, 1], [3, 4], [2, 2, 1], [4, 1]]
elif fig == 2 :
Mes = "un animal"
LIGNES= [[5], [2, 3, 2], [2, 5, 1], [2, 8], [2, 5, 11], [1, 1, 2, 1, 6], [1, 2, 1, 3], [2, 1, 1], [2, 6, 2], [15, 4], [10, 8], [2, 1, 4, 3, 6], [17], [17], [18], [1, 14], [1, 1, 14], [5, 9], [8], [7]]
COLONNES = [[5], [3, 2], [2, 1, 2], [1, 1, 1], [1, 1, 1], [1, 3], [2, 2], [1, 3, 3], [1, 3, 3, 1], [1, 7, 2], [1, 9, 1], [1, 10], [1, 10], [1, 3, 5], [1, 8], [2, 1, 6], [3, 1, 7], [4, 1, 7], [6, 1, 8], [6, 10], [7, 10], [1, 4, 11], [1, 2, 11], [2, 12], [3, 13]]
else :
Mes = "lambda"
LIGNES = [[2], [1,2], [1,1], [2], [1], [3], [3], [2,2], [2,1], [2,2,1], [2,3],[2,2]]
COLONNES = [[2,1], [1,3], [2,4], [3,4], [4], [3], [3], [3], [2], [2]]
print(Mes)
return [LIGNES, COLONNES]
def solve(LINES, COLUMNS):
t1 = time.clock()
global clauses
clauses = []
global xs
xs = dict()
global reverse_xs
reverse_xs = dict()
# Chaque case repérée par ligne colonne
lc_pairs = [(l,c) for l in range(len(LINES)) for c in range(len(COLUMNS))]
# compteur de numérotation des varaibles
variables = itertools.count(1,1)
for l,c in lc_pairs :
xs[(l,c)] = variables.__next__()
reverse_xs[xs[(l,c)]] = (l,c)
calcul_des_lignes(LINES, len(COLUMNS), variables)
calcul_des_colonnes(COLUMNS, len(LINES), variables)
print("Nombre de variables logiques :", variables.__next__())
print("Nombre de clauses logiques :", len(clauses))
print('\n')
# on fait appel à PICOSAT
# voir à la fin du code une solution alternative avec un solveur externe à Python
sol = pycosat.solve(clauses)
if sol == "UNSAT" :
print("No solution")
else :
affiche(sol, len(LINES), len(COLUMNS))
t2 = time.clock()
print('Duration : ' + "%.03f" %(t2-t1) + ' s\n')
def main(Fig = 0):
Donnees = charge(Fig)
solve(Donnees[0], Donnees[1])
main()
'''
#si la liste des clauses est trop importante, on peut faire appel a un solveur externe
print('p cnf ', numvariables, len(clauses))
with open("gen-nono.txt", "w") as f:
f.write('p cnf ' + str( numvariables ) +' '+ str( len(clauses))+'\n')
for c in clauses:
f.write( " ".join(map(lambda x: str(x),c)))
f.write( " 0\n")
os.system('c:/windows/cryptominisat.exe gen-nono.txt out-nono.txt')
with open("out-nono.txt", "r") as f:
lines = list(f)
assert len(lines) == 2
assert lines[0] == "SAT\n"
assignments = lines[1].split(" ")
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))
for l in range(NLINES) :
chars = list()
for c in columns :
if (l,c) in positives :
chars.append("#")
else :
chars.append(".")
print("".join(chars))
t2 = time.clock()
print('Duree : ' + "%.03f" %(t2-t1) + ' s\n')
'''