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 (suites de OU), chaque disjonction étant connectée à la suivante par un 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.
- 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 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 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.
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.
#
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 :
#
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