Nonogram et SAT Solver

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

Article lu   fois.

L'auteur

Profil ProSite personnel

Liens sociaux

Viadeo Twitter Facebook Share on Google+   

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 : Image non disponible                  Nonogram résolu : Image non disponible

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 (OU) chaque disjonction étant connectée à la suivante par une conjonction. (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. 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 !

Python
Sélectionnez

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')

'''

Vous avez aimé ce tutoriel ? Alors partagez-le en cliquant sur les boutons suivants : Viadeo Twitter Facebook Share on Google+   

  

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.