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 :

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

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 !

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 l_2,N variables logiques pour décrire les différentes configurations de la deuxième ligne. Supposons que l_2,i décrive la configuration suivante 2b, 2n, 1b, 2n, 1b. On appelle c_2,i les cases de la deuxième ligne du nonogram.
On aura une liste d'implications :
l_2,i Vrai => c_2,0 Faux
l_2,i Vrai => c_2,1 Faux
l_2,i Vrai => c_2,2 Vrai
l_2,i Vrai => c_2,3 Vrai
l_2,i Vrai => c_2,3 Faux
....
....

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

Elles se traduiront en DIMACS en :
-l_2,i -c_2,0 0
-l_2,i -c_2,1 0
-l_2,i c_2,2 0
-l_2,i c_2,3 0
-l_2,i -c_2,3 0
....
....

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

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

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▲

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▲

# 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

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.

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