Sudoku !

Voilà voilà pour ceux que ça intéresse : http://pastebin.com/Fn6D3Ybr (pas eu le courage de setup un repo git pour un fichier x) ) Si des gens ont des idées pour optimiser encore et toujours (notamment au niveau de la structure de donnée si possible) je suis preneur Bonne soirée

Je n'ai pas les droits d'accès

J'ai pu lister les solutions, et subséquemment les compter, mais pas les compter sans les trouver ! Concernant l'exemple de ton tuto, j'ai trouvé 434 solutions, toutes valides, toutes différentes, à moins d'une grosse bourde. S'il y a un (des) amateur(s), j'aimerais confirmation.

Je n'ai pas les droits d'accès

Désolé, voici le bon url : https://zestedesavoir.com/tutoriels/476/le-backtracking-par-lexemple-resoudre-un-sudoku/

C'est étonnant. Peux-tu s'il te plait donner la grille de départ et 2/3 exemples de solutions que tu trouves ?

Voici la grille : 9..1....5..5.9.2.18…4........8.......7.........26..92..3....6…2..9....19.457.

et quelques résultats (obtenus avec la version basique de l'algorithme)

• les 3 premiers : 934172685765893241812645397429581763658739124173426859297358416546217938381964572 934172685765893241812645397649581723528739164173426859297358416456217938381964572 934172685765893241812645793423589167596731428178426359249357816657218934381964572
• les 3 derniers : 976132845435897261812645793149583627628719354753426189297358416564271938381964572 976132845435897261812645793159483627628719354743526189297358416564271938381964572 976132845435897261812645793623489157598713624147526389259378416764251938381964572

Je viens de vérifier de mon coté, et je trouve également 434 solutions. Le problème vient donc de la grille du tuto (je ne me souviens plus d'où elle vient exactement).

Merci de l'avoir signalé, je vais essayer de remplacer par une grille valide dès que j'ai du temps.

J'ai un peu galéré avant d'en arriver là, mais c'est le but du jeu. Je voudrais poursuivre en expérimentant d'autres méthodes qui ne demandent pas de prérequis dont la compréhension me poserait quelques difficultés (Yoch, ton post du 10 décembre !), méthodes pouvant le cas échéant s'appliquer à des problèmes du même type.

Des conseils ?

Le premier post du topic, fin de section III, donne diverses pistes à explorer. Dis nous celle qui t'intéresse et on pourra essayer de t'orienter un peu plus. Tout dépend de ce que tu es intéressé d'apprendre, voici quelques infos complémentaires concernant les prérequis :

• pour utiliser clpfd, il faut connaitre un peu prolog ;
• le problème de couverture exacte est facile à comprendre (cf. wikipédia), modéliser un sudoku à partir de là est moins évident (mais on peut te guider si nécéssaire), en revanche l'implantation d'un solveur DLX est plutôt technique (mais reste faisable si tu es motivé) ;
• pour utiliser un solveur SAT, il faut comprendre ce qu'est un problème SAT (ce n'est pas très difficile contrairement aux apparences, tu peux regarder par exemple les explications données ici dans la partie briefing), et savoir l'exprimer sur une grille de sudoku ;
• pour faire de la programmation linéaire sur entiers, on travaille généralement avec un langage nommé GMPL, ça peut être sympa de voir ça si le domaine t'intéresse ;
• pour modéliser un jeu humain, je te laisse voir par toi même .

Bien sûr, cette liste n'est pas exhaustive, c'est juste que je n'ai pas d'autre idée.

Je vais entrer en religion ! Je veux dire que j'ai pas mal de lecture avant de me décider. Pour commencer, je vais tâter de la littérature SAT. Prolog, je l'ai étudié dans les années 80, mais il ne m'en reste rien. À suivre …

Premiers essais :

La structure de données utilisée est une liste (la formule) de listes (les clauses).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

def traiterFormule(formule,assignations):
    " propagation - version initiale - sans backtracking "   
    # la formule initiale n'est pas conservée
    if formule == []:       
        print('\nfin',formule)
        return True
    formuleNouvelle = []  
    #la variable choisie est :
    # - la variable contenue dans la première clause de longueur 1
    # - ou la variable de rang 1 dans une clause de longueur >1
    # - cas de la première clause vide non traité     
    variable = choix(formule)[0]
    negationVariable = -(variable)  
    #permet de suivre l'évolution de la propagation
    print('booléen vrai :',variable,formule)
    #propagation proprement dite
    for f in range (0,len(formule)):
        clause = formule[f]        
        if negationVariable in clause :
            clause.remove(negationVariable)
            formuleNouvelle.append(clause)
        elif variable not in clause:
            formuleNouvelle.append(clause)  
    #liste des booléens vrais - à nuancer        
    assignations[abs(variable)-1] = variable   
    #permet de suivre l'évolution des assignations"
    print('assignations :',assignations)  
    return traiterFormule(formuleNouvelle,assignations)  

Ce code fonctionne bien sur les exemples du lien ci-dessus (de l'art de la SATisfaction) pour lesquelles une simple propagation permet de conclure. Je vais maintenant m'interroger sur plusieurs points :

• l'algorithme réduit la liste initiale au fur et à mesure de la propagation, cela ne permettra sans doute pas de revenir en arrière (solution :conserver la liste initiale et "marquer" les booléens traités ?)
• je m'interroge sur la condition d'arrêt de la propagation (première apparition d'une clause vide ?)
• enfin l'exemple de code donné pour le parsing, en OCaml, est quasi-inexploitable pour qui ne connait pas ce langage, malgré les commentaires. Je vais essayer de m'y coller, mais ça ne me réjouit guère.

À suivre …

Là tu t'es carrément engagé dans l'implémentation d'un solveur SAT. C'est hyper intéressant en soit, mais tu aura du mal à obtenir quelque chose de praticable pour résoudre un sudoku.

Ce que je voulais pointer, c'est les explications sur le concept de SAT-problem, et le format CNF. Une fois que tu as intégré ceci, tu peux déja modéliser toutes sortes de problèmes (dont le sudoku), et employer un solveur existant pour faire le travail de résolution. C'est nettement plus facile et plus amusant.

Si tu code en python, je t'engage à regarder du coté de pycosat qui est un binding vers un solveur plutôt bon. D'ailleurs ça tombe bien, il y a parmi les codes d'exemple la résolution du sudoku.

J'avais différé la lecture de documents liés à pycosat, notamment SAT based sudoku solver in python du Dr. Ilan Schnell, ainsi que a SAT-based sudoku solver de Tjark Weber, dans l'attente de la réalisation d'un solveur SAT, même non praticable ! Je ne desespère pas, mais j'ai besoin d'aide, et puis j'ai la chance d'avoir du temps, même compte tenu de la loi de Hofstadter : « Il faut toujours plus de temps que prévu, même en tenant compte de la Loi de Hofstadter. »

Ceci dit, je vais essayer de mener de pair l'exploration pycosat. Et si tu as le temps de répondre aux questions ci-dessus …

À suivre …

Je vais maintenant m'interroger sur plusieurs points :

• l'algorithme réduit la liste initiale au fur et à mesure de la propagation, cela ne permettra sans doute pas de revenir en arrière (solution :conserver la liste initiale et "marquer" les booléens traités ?)

Pour revenir en arrière, il faut forcément sauvegarder les données d'une façon. Le plus simple est de backtrack sur des copies complètes de la liste des clauses, mais c'est coûteux.

• je m'interroge sur la condition d'arrêt de la propagation (première apparition d'une clause vide ?)

Je n'ai plus tous les détails en tête, mais si je me souviens bien c'est soit ça (auquel cas fail), soit qu'il n'y a plus de clauses non unitaires (auquel cas on a une solution).

• enfin l'exemple de code donné pour le parsing, en OCaml, est quasi-inexploitable pour qui ne connait pas ce langage, malgré les commentaires. Je vais essayer de m'y coller, mais ça ne me réjouit guère.

Un parser basique pas trop fiable (marche uniquement si les clauses tiennent toutes sur une seule ligne, c'est généralement le cas) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

def cnf_parser(filename):
    with open(filename, 'r') as fp:
        # get header
        for line in fp:
            if line.startswith('c'):
                continue
            elif not line.startswith('p cnf'):
                raise RuntimeError('not a valid CNF file')
            else:
                V, C = map(int, line[5:].split())
                break
        M = [set([int(nb) for nb in line.split()][:-1])
                 for line in fp
                 if not line.startswith('c')]
        assert len(M) == C
        assert len(get_vars(dct)) == V
        return M

EDIT: Pour info, j'avais posté un code python minimaliste pour DPLL sur le topic cité plus haut.

EDIT: Pour info, j'avais posté un code python minimaliste pour DPLL sur le topic cité plus haut.

Désolé, mais je n'ai pas trouvé.

Pour ce qui concerne pycosat, c'est bon ! J'ai adapté le code d'Ilan Schnell à la résolution de grilles 25*25. En test, une grille de cette taille essoufle python (itertools décèle au moins 4000 solutions, et le noyau s'arrête). Je ne vois d'ailleurs pas l'intérêt de proposer ce genre de grilles à des étudiants, ce qui est le cas. Je vais essayer d'écrire les clauses pour des sudokus d'autres types (jigsaw, killer, comparison). En fait, le sudoku ne m'intéresse pas, c'est la méthode et la mise en oeuvre qui me motivent. Au programme bientôt, le solitaire (on peut le formaliser cnf ?).

À suivre …

EDIT: Pour info, j'avais posté un code python minimaliste pour DPLL sur le topic cité plus haut.

Désolé, mais je n'ai pas trouvé.

Ici, il y a un lien vers : http://paste.awesom.eu/yoch/nMQ

Pour ce qui concerne pycosat, c'est bon ! J'ai adapté le code d'Ilan Schnell à la résolution de grilles 25*25. En test, une grille de cette taille essoufle python (itertools décèle au moins 4000 solutions, et le noyau s'arrête).

Ce n'est sans doute pas python qui flanche, mais picosat (la lib C qui tourne derrière). Enfin, faudrait voir.

Je ne vois d'ailleurs pas l'intérêt de proposer ce genre de grilles à des étudiants, ce qui est le cas.

Que veux tu dire ? D'ailleurs, tu cherche à résoudre une grille, ou à en générer (j'essaie de comprendre pourquoi > 4000 solutions) ?

Je vais essayer d'écrire les clauses pour des sudokus d'autres types (jigsaw, killer, comparison). En fait, le sudoku ne m'intéresse pas, c'est la méthode et la mise en oeuvre qui me motivent. Au programme bientôt, le solitaire (on peut le formaliser cnf ?).

Probablement.

J'essaie seulement de résoudre les grilles de sudoku. Ayant adapté le code de d'Ilan Schnell à la résolution d'une grille 25*25, j'ai trouvé une grille de cette taille ici, avant-dernière page. C'est un document que je suppose destiné à des étudiants. Voici la grille :

Il y a seulement 28 cases affectées. Par simple curiosité, en utilisant itertools, j'ai voulu connaître le nombre de solutions (en affectant une valeur au paramètres nombre de solutions, il y a moyen de le borner - sup. - puisqu'il retourne le nombre exact s'il est inférieur à la valeur du paramètre). Ça coince à 4000.

Voilà l'explication.

En tout cas merci pour ta patience et ta promptitude, tu dois maintenant te sentir bien seul sur ce forum.

Lorsque tu dis "ça coince", il s'agit d'un plantage ou d'un freeze ?

Je ne sais pas exactement comment picosat s'y prend pour générer toutes les solutions (basiquement, on ajoute à chaque fois la négation de la solution trouvée), mais il est possible qu'il n'y a plus de solution, et qu'il ait du mal à démontrer UNSAT (c'est souvent plus difficile que de trouver une solution lorsqu'elle existe). Mais bon, il ne devrait pas planter non plus.

Ce que tu peux essayer, c'est d'ajouter des dévoilés de façon incrémentale jusqu'à avoir une seule solution (et voir si ça coince aussi).

J'essaie seulement de résoudre les grilles de sudoku. Ayant adapté le code de d'Ilan Schnell à la résolution d'une grille 25*25, j'ai trouvé une grille de cette taille ici, avant-dernière page. C'est un document que je suppose destiné à des étudiants. Voici la grille :

.......................23…21................2..........21..............................5........19…3..........9..........1.........................................4.......................13......7......8…12....................15............1................................................11.3............1......23.........................................................10.............25..........................................19.....................................1.2...............................1............................................................................1.............................................25....

Il y a seulement 28 cases affectées. Par simple curiosité, en utilisant itertools, j'ai voulu connaître le nombre de solutions (en affectant une valeur au paramètres nombre de solutions, il y a moyen de le borner - sup. - puisqu'il retourne le nombre exact s'il est inférieur à la valeur du paramètre). Ça coince à 4000.

Arbraz je ne te pourrai pas te dire pourquoi ça coince mais ta grille comporte un très grand nombre de solutions (j'ai arrêté mon solver au bout de 1 000 000 mais il y en a bien plus je pense).

Avec 28 indices révélés cela me parait logique car le nombre minimum d'indices révélés pour avoir une grille 25x25 à solution unique est certainement plus élevé, il est de 17 pour une grille 9x9. Ils ont peut-être fourni cet exemple pour obtenir au moins une solution rapidement.

Si tu souhaites tester des grilles 25x25 à solution unique, j'en ai rassemblé 50 ici. Mais par contre elles seront bien plus dures à résoudre.

Yoch, s'agissant du code DPLL dont tu m'as donné le lien, je suis en train de le décortiquer pour mieux le comprendre, et j'ai quelques interrogations :

1

dct = deepcopy(dct)

• intérêt dans le code de deepcopy
• j'imagine que le choix d'une structure de dictionnaire est un choix d'efficacité (lisibilité du code ? rapidité d'exécution ?)
• l'algorithme renvoie l'existence ou non d'une solution, mais pas la solution si elle existe ; comment procéder (doit-on considérer que la solution est constituée des seuls littéraux vrais, auquel cas, les clauses de longueur 1 et les littéraux purs en constituent un sous-ensemble) ? Au-delà, je coince !

À suivre …

1. pour copier intégralement le dictionnaire avant d'aller plus loin, afin de pouvoir revenir en arrière sans embêtements (ce n'est pas ce qu'il y a de plus efficace…) ;
2. simplicité surtout ;
3. oui, la solution est constituée des littéraux vrais, mais dans mon code je ne les garde pas (si ma mémoire est juste), d'où la solution de facilité de renvoyer simplement SAT/UNSAT.

Je ne maîtrise pas la récursivité ! Mon objectif est d'utiliser DPLL pour des problèmes mis sous forme cnf, autrement dit utiliser un code que je comprends, pycosat étant un plus en termes de rapidité/efficacité. Concernant l'algorithme DPLL, je constitue une liste des littéraux solution, en les ajoutant à chacune des étapes 1 et 2(les clauses unitaires, les littéraux purs). Concernant l'étape 3 (le littéral d'occurrences max), j'ajoute, et j'enlève le cas échéant :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11

    dct[maxi+1] = {l}
    # Étape 3-1
    if l not in solution : solution.append(l)  
    if DPLL(dct,solution):        
        return True
    else :  
        # Étape 3-2
        solution.remove(l)
        dct[maxi+1] = {-l}        
        iter += 1
        return DPLL(dct,solution)

Ceci ne me semble pas - n'est pas correct - puisque je n'assure pas le backtracking en ne supprimant pas les éléments qu'il faut de la liste "solution". Tu dis aussi, yoch, que cette méhode "n'est pas ce qu'il y a de plus efficace". Veux-tu bien me mettre sur la voie, l'une ou l'autre ou les deux. J'aimerais vraiment conclure.

Merci

À suivre …