Consignes

La collaboration orale est encouragée, mais le partage de code et le copier/coller (via Discord, github, etc.) n'est pas autorisé et pourra être pénalisé.

Le rendu de ce TP se fera uniquement par TPLab et consistera en une archive (zip, tar, etc.) contenant un répertoire TP1-NOM avec :

Vous aurez compris que NOM devra être remplacé par votre nom (ou vos noms en cas de binômes) !

Tous vos fichiers doivent comporter une entête avec votre nom et votre groupe de TP.

Tout non respect d'une ou plusieurs de ces consignes entrainera automatiquement un retrait de points sur votre note !

Liens utiles

Préliminaires : simplesat.py, un solveur récursif naïf en Python

Cette première séance de travaux pratiques doit vous aidez à vous familiariser avec le problème de la satisfiabilité : SAT.

Étant donnée une formule (données en forme normale conjonctive), comme (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ ¬x3 ∨ x4) ∧ (x2 ∨ ¬x4) nous voulons savoir s'il est possible de satisfaire cette formule (càd la rendre vraie) en choisissant des valeurs booléennes pour x1, x2, x3 et x4.

Les fichiers .sat pour les formules en forme normale conjonctive

Les formules considérées seront toujours en forme normale conjonctive. Elle seront en général données dans des fichiers d'extension .sat.

Voici par exemple la représentation de la formule (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ ¬x3 ∨ x4) ∧ (x2 ∨ ¬x4) : 

# un exemple de formule toute simple dans un fichier SAT
x1 -x2 x3
-x1 -x3 x4
x2 -x4

Utilisation de simplesat

Le fichier simplesat-NOM.py contient un solveur SAT récursif naïf écrit en Python, utilisable uniquement en ligne de commandes.

Vous devrez le compléter (question 1) pour le rendre fonctionnel, mais voici comment l'utiliser pour chercher une solution à une formule : 

$ python3 ./simplesat-NOM.py FICHIER_FORMULE

où FICHIER_FORMULE est le fichier (au format SAT) qui contient la formule à considérer

Par exemple : 

$ python3 ./simplesat-NOM.py test2.sat
SATISFIABLE
-a b c d
$ python3 ./simplesat-NOM.py test3.sat
UNSATISFIABLE

Dans le premier cas, la formule est satisfiable avec les valeurs a=0, b=c=d=1, alors que dans le second cas, la formule n'est pas satisfiable.

Deux autres fonctionnalités pratiques de simplesat-NOM.py sont :

Représentation des formule FNC et code du solveur

En interne, les formules traitées par simplesat-NOM.py sont des listes de listes d'entiers non nuls.

Attention, l'entier associé à une variable est local au code Python. Suivant la formule utilisée, la variable x3 peut être représentée par un entier différent de 3. (Le littéral ¬ x3 sera bien entendu représentée par l'entier opposé à celui représentant x3.)

La première fonction définie dans simplesat-NOM.py est la fonction solve. Cette fonction ne fait que quelques lignes et les commentaires devraient vous aidez à comprendre comment elle fonctionne.

La deuxième fonction, utilisée par la fonction solve est simplify_formula. Cette fonction prend en argument une formule (càd une liste de listes d'entiers, voir plus haut) et un littéral (càd un entier non nul). Cette fonction doit simplifier la formule lorsqu'on suppose que le littéral fourni est vrai.

Par exemple, si on suppose que le littéral x2 est vrai :

avant simplification : (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ ¬x3 ∨ x4) ∧ (x2 ∨ ¬x4)
après simplification : (x1 ∨ x3) ∧ (¬x1 ∨ ¬x3 ∨ x4)

En effet,

La fonction simplify_formula doit reconstruire une liste de clauses à partir de la liste de clauses F :

ATTENTION, il ne faut pas modifier la formule ou les clauses, mais en recréer de nouvelles. C'est pour cela qu'on crée une nouvelle formule simplified_F et qu'il faudra recopier tous les littéraux de chaque clause pour en créer de nouvelles.

Vous ne devez par exemple pas utiliser la méthode remove des listes Python !

Je vous rappelle également que la bonne manière d'insérer un élément dans une liste est d'utiliser la méthode append. N'utilisez pas L = L+[element] !

  1. Complétez le corps de la fonction simplify_formula et testez la. Vous pouvez pour cela utiliser l'option -T ou --test pour lancer la fonction de tests : 

    $ python3 ./simplesat-NOM.py test0.sat --test 1
simplification avec 1
avant : [[1, 2, -3], [2, 3, -4], [3, 4, 1], [4, -1, 2], [-1, -2, 3], [-2, -3, 4], [-3, -4, -1], [-4, 1, -2]]
après : [[2, 3, -4], [4, 2], [-2, 3], [-2, -3, 4], [-3, -4]]

    N'hésitez pas à modifier la fonction de tests.

  2. Testez le solveur sur la formule précédente (x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ ¬x3 ∨ x4) ∧ (x2 ∨ ¬x4).

    Le résultat est il bien correct ?

Attention, pour donner un argument négatif, il faut ajouter "--" après --test ou -T. Sinon, le -1 est interprété comme une option de la commande ! 

$ python3 ./simplesat-NOM.py FICHIER_FORMULE --test -- -1
simplification avec -1
avant : [[1, 2, -3], [2, 3, -4], [3, 4, 1], [4, -1, 2], [-1, -2, 3], [-2, -3, 4], [-3, -4, -1], [-4, 1, -2]]
après : [[2, -3], [2, 3, -4], [3, 4], [-2, -3, 4], [-4, -2]]

(Attention, il faut remplacer FICHIER_FORMULE par un nom de fichier !)

  1. La formule (a ∨ ¬b) ∧ (¬b ∨ ¬c) ∧ (¬a ∨ ¬c) ∧ (¬a ∨ ¬b ∨ c) ∧ (a ∨ b ∨ ¬c) est elle satisfiable ?

    Créez un fichier question2-NOM.sat que vous joindrez à votre archive pour tester.

  2. Y'a t'il d'autres solution que celle trouvée ? Comment procédez vous pour les trouver sans utiliser l'option -A / --all ? (Indice: il faudra rajouter des clauses pour interdire la solution trouvée)

Pour créer un fichier .sat, vous pouvez utiliser n'importe quel éditeur de texte : SublimeText, Gedit, nano, etc.

Rechercher toutes les solutions

Pour les petites formules, il est parfois intéressant de chercher toutes les solutions à un problème. Pour ceci, vous pouvez donner l'argument -A ou --all à simplesat-NOM.py.

Testez plusieurs fois simplesat-NOM.py avec l'option -A sur la formule précédente) en mélangeant aléatoirement la formule avec l'option -r / --randomize. (Cette option modifie simplement l'ordre des clauses de la formule et celui des littéraux des clauses, mais ne change pas la sémantique de la formule.)

Que constatez vous ? Proposez une explication.

1. Quelques problèmes de satisfiabilité

Il est possible d'encoder de nombreux problèmes comme des problèmes de satisfiabilité. Par exemple, les règles d'un sudoku s'expriment comme des contraintes logiques :

Bien sûr, il faut utiliser un programme pour générer une telle formule !

Écrivez un programme qui génère un fichier SAT à partir d'une grille de sudoku, et qui affiche la grille obtenu à partir de la solution trouvée par le solveur.

Attention, ceci se rapproche plutôt d'un mini projet que d'une simple question. Ne commencer à y réfléchir qu'une fois que vous avez fait le reste du TP !

(Pour information, mon fichier Python qui permet de faire ceci fait un peu moins de 150 lignes, dont une moitié sert à lire / écrire la grille.)

1.1. L'énigme de Einstein

Comme simplesat-NOM.py ne peut pas (encore) gérer un tel nombre de variables / clauses (voici un exemple de fichier SAT correspondant à une grille de sudoku), nous allons regarder un autre problème "amusant" : une variante de l'énigme d'Einstein.

échauffement

Ce problème est extrait du lien suivant : http://villemin.gerard.free.fr/LogForm/Integram.htm.

On suppose que les 4 cartes suivantes sont les 4 as :

1 2 3 4

Et on dispose des indices suivants :

  1. En 2, il n'y a ni l'as de trèfle, ni l'as de pique.

  2. L'as de trèfle est plus à droite que l'as de carreau.

  3. L'as de carreau et l'as de cœur ne sont pas à côté l'un de l'autre.

L'objectif de la question suivante sera de répondre à Quelles sont les positions des as ? La solution est elle unique ?

  1. Écrivez (à la main) un fichier SAT pour résoudre le problème.

    • il y aura 16 variables :

      • X_1_trefle pour l'as de trèfle est en position 1

      • X_2_trefle pour l'as de trèfle est en position 2

      • ...

      • X_3_coeur pour l'as de cœur est en position 3

      • ...

    • le premier indice donne 2 clauses ne contenant qu'un seul littéral chacune

    • le deuxième indice donne 4 clauses qu'il vous faudra transformer en FNC (c'est facile) :

      • X_4_trefle ⟶ X_1_carreau ∨ X_2_carreau ∨ X_3_carreau

      • X_3_trefle ⟶ X_1_carreau ∨ X_2_carreau

      • X_2_trefle ⟶ X_1_carreau

      • ¬X_1_trefle (en effet, l'as de trèfle ne peut pas se trouver en position 1)

    • le troisième indice donne 6 clauses de 2 littéraux chacune. Une de ces clauses est ¬(X_2_carreau ∧ X_3_coeur). (Là encore, la transformation en FNC est simple.)

    Il y a souvent plusieurs choix possibles pour exprimer les contraintes. Formellement, l'indice 1 s'exprime par les 2 clauses (-X_2_trefle) ∧ (-X_2_pique), mais la clause (X_2_coeur ∨ X_2_carreau) pourrait aussi être utilisée.

    Cette deuxième possibilité est une conséquence de l'indice 1 et de la contrainte logique (X_2_pique ∨ X_2_coeur ∨ X_2_carreau ∨ X_2_carreau). Autrement dit, interpréter l'indice par cette clause nécessite une étape de raisonnement de la part de l'utilisateur, alors que la première solution est directe.

    Il vous faudra aussi ajouter d'autres contraintes. La plus complexe sera pour dire, par exemple, qu'il n'y a qu'un seul as de pique. Les clauses correspondantes, au format SAT, sont les suivantes. Elles expriment le fait qu'on ne peut pas trouver 2 as de piques sur les positions 1, 2, 3 et 4. 

    # il y a au plus un as de pique
-X_1_pique -X_2_pique
-X_1_pique -X_3_pique
-X_1_pique -X_4_pique
-X_2_pique -X_3_pique
-X_2_pique -X_4_pique
-X_3_pique -X_4_pique

    Avec une utilisation judicieuse du copier/coller, l'écriture de ce fichier ne devrait pas vous prendre trop de temps. Je vous conseille également de mettre des commentaires pour expliquer à quoi correspond chaque groupe de clauses.

  2. Cherchez une solution au problème avec simplesat-NOM.py, et vérifiez qu'elle est bien cohérente avec les indices.

    Documentez (dans le fichier README) et corrigez les bugs éventuels que vous trouvez.

L'option -X / --exclude-negative-lit de simplesat-NOM.py permet de n'afficher que les variables vraies des solutions. Cela facilite l'interprétation des solution pour cette question (ou la suivante) : si l'as de pique est en position 3, les littéraux -X_1_pique, -X_2_pique et -X_4_pique n'apparaitront pas dans la solution affichée.

Le problème de Einstein

Voici maintenant une variante de l'énigme d'Einstein.

On suppose que 5 maisons sont alignée, en positions 1, 2, 3, 4, 5:

1 2 3 4 5
./Images/small_house-1.png ./Images/small_house-2.png ./Images/small_house-3.png ./Images/small_house-4.png ./Images/small_house-5.png

Chaque maison est habitée par une personne :

  • qui a un animal,

  • qui boit une boisson particulière,

  • qui écoute un style de musique,

  • qui exerce un métier.

Et les indices sont les suivants :

  1. le musicien a une tortue ;

  2. le propriétaire de la maison jaune écoute du jazz ;

  3. la personne qui écoute du hardrock a un chat ;

  4. la maison en bois se trouve juste à gauche de la maison blanche ;

  5. le chercheur habite dans la maison en briques ;

  6. le footballeur habite juste à coté de l'immeuble ;

  7. la personne qui écoute de la musique classique est voisine de celle qui boit de la bière ;

  8. la personne qui écoute du hiphop boit du thé ;

  9. la personne qui habite dans la maison du milieu boit beaucoup de soda ;

  10. le footballeur habite dans la première maison ;

  11. la personne qui écoute de la musique classique est voisine de la personne qui a des poissons ;

  12. le boulanger écoute de la chanson française ;

  13. la personne qui a un hamster est voisine de celle qui écoute du jazz ;

  14. l'architecte boit de l'eau ;

  15. le propriétaire de la maison en bois aime bien le whisky.

L'objectif de la question suivante est de répondre à Qui est le propriétaire du zèbre ?

L'expression de ce problème comme problème de satisfiabilité utilisera 125 variables ! Il est donc préférable de générer la formule avec un programme.

Les variables

Les variables seront toutes de la forme E_i_a pour dire "l'attribut a est à l'Emplacement i"

Les attributs sont les types de maisons (5 possibilités), animaux (5 possibilités), boissons (5 possibilités), styles de musique (5 possibilité) et métiers (5 possibilités). Il y a donc 25 attributs et 5 emplacements possibles. Cela fait bien un total de 25 × 5 = 125 variables.

Par exemple, la formule E_3_musicien ∧ E_3_brique indique que le musicien habite dans la maison en briques, et que cette maison est en position 3.

Les indices

La plupart des indices sont de la forme "les attributs a et b sont au même endroit". Par exemple, le premier indice est équivalent à "le musicien et la tortue sont au même endroit".

On peut exprimer ceci par la formule

(E_1_musicien ⟷ E_1_tortue) ∧
(E_2_musicien ⟷ E_2_tortue) ∧
(E_3_musicien ⟷ E_3_tortue) ∧
(E_4_musicien ⟷ E_4_tortue) ∧
(E_5_musicien ⟷ E_5_tortue)

qu'il vous faudra transformer en FNC (10 clauses de 2 littéraux).

Nous allons utiliser 4 types d'indices :

Les fonctions left_of, next_to et exact sont déjà définies dans le fichier zebra-NOM.py.

Les contraintes

Il faut à ceci ajouter 3 autres contraintes logiques :

Les fonctions no_duplicates et single_attr_pos sont déjà définies dans le fichier zebra-NOM.py.

  1. Récupérez le fichier zebra-NOM.py et

    • écrivez le corps de la fonction same_position (voir ci dessus),

    • écrivez le corps de la fonction all_attr_pos (voir ci dessus),

    • complétez avec les appels pertinents pour chacun des indices.

    L'exécution de ce programme 

    $ python3 zebra-NOM.py
...

    affiche la formule CNF correspondant au problème de Einstein.

  2. Lancez simplesat-NOM.py sur la formule obtenue.

    Vous pouvez sauvegarder la formule générée par le programme zebra-NOM.py dans un fichier avec une redirection du shell : 

    $ python3 zebra-NOM.py > formule-zebre.sat

    Comme simplesat-NOM.py peut lire la formule sur l'entrée standard, vous pouvez aussi utiliser une redirection 

    $ python3 zebra-NOM.py | python3 simplesat-NOM.py

  3. Répondez à la question "Qui est le propriétaire du zèbre ?".

L'ordre des clauses d'une formule est parfois important.

Essayer de résoudre le problème en mélangeant la formule (option -r / --random), ou simplement en mettant les contraintes logiques (appels aux fonctions all_attr_pos, no_duplicates et single_attr_pos) avant les indices pour constater une grosse différence de temps de calcul !

De la même manière, remplacer "tous les attributs sont à un emplacement" ("constraint_1) par la contrainte "tous les emplacements ont un attribut"

(E_1_chanson ∨ E_1_classique ∨ E_1_hardrock ∨ E_1_hiphop ∨ E_1_jazz) ∧
(E_1_biere ∨ E_1_eau ∨ E_1_soda ∨ E_1_the ∨ E_1_whisky) ∧
............. ∧
(E_2_chanson ∨ E_2_classique ∨ E_2_hardrock ∨ E_2_hiphop ∨ E_2_jazz) ∧
............. etc. .............

donne une formule équivalente (grâce à no_duplicates et single_attr_pos), mais où la satisfiabilité est beaucoup plus dure pour l'algorithme naïf.

Normalement, il n'y a qu'une seule solution au problème ! Si vous lancez simplesat-NOM.py avec l'option -A / --all, vous devriez obtenir 2 solutions. (Le propriétaire du zèbre est le même dans les deux.)

Essayez de comparer les solutions afin de trouver le bug que j'ai introduit dans le fichier zebra-NOM.py.

2. Algorithme DPLL

La première avancée sur les solveurs a été l'algorithme DPLL. L'idée principale est d'ajouter une phase de simplification avant chaque choix du solveur. Cette étape est parfois appelée BCP, pour Boolean Constraint Propagation.

L'algorithme DPLL proposait 2 simplifications :

En pratique, seule la première simplification est importante. La seconde demande en général trop de calculs.

La propagation des clauses unitaires consiste à identifier les clauses avec un unique littéral dans la formule :

... ∧ ... ∧ (L) ∧ ... ∧ ...

Pour satisfaire cette formule, le littéral L doit forcément être à vrai. On peut donc l'ajouter à la solution courante et simplifier la formule avec la fonction simplify_formula écrite précédemment.

Bien entendu, on peut faire cette simplification jusqu'à ce que la formule ne contienne plus de clause unitaire.

  1. Ajoutez les quelques lignes suivantes au tout début de la fonction solve, juste après la docstring : 

        # boolean constraints propagation
    if bcp:
        F, sol2 = BCP(F)
        sol.extend(sol2)

    Ceci permettra d'appeler automatique la fonction de simplification à chaque étape.

  2. Complétez le corps de la fonction BCP(F). Cette fonction doit renvoyer 2 choses :

    • la formule simplifiée au maximum,

    • la liste des littéraux qui ont servi à cette simplification.

    Pour information, le corps de ma fonction fait 12 lignes, en comptant les 2 lignes "sol = []" et "return F, sol".

  3. Pour tester, vous pouvez utiliser l'option -D / --DPLL de simplesat-NOM.py.

    Décrivez les tests que vous effectuez et comparez l'efficacité du solveur optimisé avec le solveur non optimisé.

Comparez l'efficacité du solveur naïf optimisé avec minisat et documentez vos résultats.

Vous pouvez utiliser la formule de l'énigme de Einstein, le fichier modélisant une grille de sudoku. Pour des fichiers plus gros, voici par exemple une archive de fichiers modélisant le problème des n reines, pour plusieurs valeurs de n. Les fichiers sont donnés au format SAT (extension .sat) et DIMACS (extension .cnf).

minisat lit la formule dans un fichier au format DIMACS. simplesat-NOM.py peut transformer un fichier .sat au format DIMACS avec l'option -C / --convert. Vous pouvez donc sauvegarder le fichier DIMACS avec une redirection : 

$ python3 simplesat-NOM.py -C formule.sat > formule.cnf
$ minisat formule.cnf

Pour obtenir la solution trouvée, il faut fournir un second nom de fichier à minisat pour qu'il y écrive le résultat : 

$ minisat formule.cnf formule.sol
$ cat formule.sol
...

Testez d'autres optimisations comme :

Pour optimiser encore plus, il faudrait utiliser un langage compilé (C ou C++) et remplacer la version récursive par une version itérative utilisant des structures de données spécialisées. Vous pouvez aller voir le TP2 de l'année 2020 pour découvrir ce à quoi ça pourrait ressembler !

Pour optimiser encore plus, il faudrait par exemple implémenter le conflict-driven clause learning.

3. Autres problèmes de satisfiabilité : arithmétique

Étant donné un circuit booléen, il est facile de calculer la sortie à partir des entrées. Avec un solveur, on peut essayer de faire l'inverse : étant donné le résultat, trouver une entrée correspondante !

Les entiers d'un ordinateur sont simplement des suites de (32 ou 64) bits. Les opérations sont faites par des circuits, c'est à dire des opérations logiques sur ces bits. Nous allons essayer d'inverser les circuits correspondant à des opérations arithmétique.

3.1. Inverser l'addition

Par exemple, l'addition de 2 nombres écrits en binaire se fait en additionnant leurs bits avec la retenue colonne par colonne.

Pour additionner les nombres ak ... a1 a0 et bk ... b1 b0, on peut "poser l'addition"

cn .......... c2 c1 c0 (retenues, "carry" en anglais)
an .......... a2 a1 a0 (1er nombre)
+ bn .......... b2 b1 b0 (2ème nombre)
sn .......... s2 s1 s0 (somme)

Les formes normales conjonctives des formules s ⇔ (a ⊕ b ⊕ c) et cc ⇔ (a ∧ b) ∨ (a ∧ c) ∨ (b ∧ c) sont respectivement

(¬a ∨ ¬b ∨ ¬c ∨ s) ∧ (¬a ∨ ¬b ∨ c ∨ ¬s) ∧ (¬a ∨ b ∨ ¬c ∨ ¬s) ∧ (a ∨ ¬b ∨ ¬c ∨ ¬s) ∧
(a ∨ b ∨ c ∨ ¬s) ∧ (a ∨ b ∨ ¬c ∨ s) ∧ (a ∨ ¬b ∨ c ∨ s) ∧ (¬a ∨ b ∨ c ∨ s)

et

(¬a ∨ ¬b ∨ ¬c ∨ cc) ∧ (¬a ∨ ¬b ∨ c ∨ cc) ∧ (¬a ∨ b ∨ ¬c ∨ cc) ∧ (a ∨ ¬b ∨ ¬c ∨ cc) ∧
(a ∨ b ∨ c ∨ ¬cc) ∧ (a ∨ b ∨ ¬c ∨ ¬cc) ∧ (a ∨ ¬b ∨ c ∨ ¬cc) ∧ (¬a ∨ b ∨ c ∨ ¬cc)

Téléchargez le fichier addition-NOM.py.

  1. Écrivez une fonction xor3(s, a, b, c) qui affiche les clauses correspondant à l'opération (sur des bits) s := a ⊕ b ⊕ c.

    Inspirez vous pour cela de la fonction carry3(cc, a, b, c) qui affiche les clauses correspondant à l'opération cc := (a ∧ b) ∨ (a ∧ c) ∨ (b ∧ c).

  2. Complétez le fichier addition-NOM.py pour générer un problème SAT correspondant au circuit addition de résultat s :

    • générer toutes les clauses (i=0, ..., n) pour sk := ak ⊕ bk ⊕ ck et ck+1 := (ak ∧ bk) ∨ (ak ∧ ck) ∨ (bk ∧ ck) en utilisant xor3 et carry3.

      Attention, pour la fonction carry3, le premier argument correspond à la retenue de la colonne suivante. Vous devrez donc l'appeler avec, par exemple, les arguments "c_3", "a_2", "b_2" et "c_2".

    • imposer les valeurs de s_0, s_1, ... pour obtenir le résultat s.

    • s_0 correspond à la parité de s,

    • s_1 correspond à la parité de s // 2,

    • s_2 correspond à la parité de s // 4,

    • s_3 correspond à la parité de s // 8,

    • etc.

  3. Vérifiez que vous obtenez une solutions correcte pour l'addition a + b == 7, sur 4 bits.

    Documentez (dans le fichier README) et corrigez les bugs éventuels que vous trouvez.

    Pour ceci, vous devez lancer le programme avec 2 arguments : la valeur de n (nombre de bits) et la valeurs de s (somme voulue). 

    $ python3 addition-NOM.py 4 7 > add-7.sat

    permettra de générer les clauses correspondantes dans le fichier add-7.sat.

    Il est possible d'utiliser les redirections des shells Unix pour éviter d'avoir à sauvegarder un fichier à chaque fois : 

    $ python3 addition-NOM.py 4 7 | python3 simplesat-NOM.py -v
>>> the formula contains 17 clauses and 70 variables, for a total of 262 literals
SATISFIABLE
-c_1 -c_5 s_1 s_2 s_3 -s_4 a_1 -b_1 -c_2 a_2 -b_2 -c_3 a_3 -b_3 -c_4 -a_4 -b_4

  4. Testez (sur des petites valeurs) en utilisant l'option -A / --all pour vérifiez que vous trouvez bien le bon nombre de solutions pour a + b == s. (Il y a exactement s+1 manières d'obtenir s comme la somme de 2 nombres : 0+s, 1+(s-1), 2+(s-2), ..., s + 0.)

Documentez (dans le fichier README) et corrigez les bugs éventuels que vous trouvez.

3.2. Inverser la multiplication

Inverser un circuit additionneur n'est pas très intéressant. Par contre, inverser un circuit multiplicateur l'est plus. Vérifier la satisfiabilité correspondant à a × b = p (pour un p donné) revient à chercher des facteurs de p, càd à factoriser p !

Générer les clauses correspondant à une multiplication est un peu plus complexe que pour l'addition. Le fichier multiplication-NOM.py le fera pour vous.

  1. Ajoutez, tout à la fin du fichier, les clauses pertinentes pour forcer les valeurs de p_0, p_1, ... p_{n} aux bits de p. (C'est identique à ce que vous avez fait pour forcer les valeurs de s_0, ... dans la question précédente.)

    Vérifiez que vous arrivez bien à factoriser le nombre 48 en 2 nombres de 4 bits : 

    $ python3 multiplication-NOM.py 4 4 48 | python3 simplesat-NOM.py -r
SATISFIABLE
x_17 -x_13 -x_15 -a_2 -q_2_2 p_5 -p_6 -q_2_1 -q_1_2 -x_8 -q_1_0 -x_1 -x_9
-q_3_0 -x_6 -q_2_0 -q_2_3 b_1 -q_1_1 -a_1 x_12 -q_0_2 a_3 -x_10 -x_4 -b_0
-q_0_0 -x_16 -x_18 -x_20 -a_0 p_4 -q_1_3 -x_19 -q_3_3 -x_2 -x_7 -q_0_1
-x_11 q_3_2 -p_2 -x_5 -q_0_3 -p_3 -x_14 q_3_1 -x_3 -p_0 -p_7 -p_1 -b_3 b_2

    Attention, il y a plusieurs solutions (la factorisation n'est pas unique) et vous n'obtiendrez pas forcément le même résultat. Vous devrez donc extraire les variables a_i et b_j de la solution pour retrouver les valeurs de a et b

  2. Vérifiez que pour les clauses correspondant à un nombre premier ne sont pas satisfiable.

    Documentez (dans le fichier README) et corrigez les bugs éventuels que vous trouvez.

  1. utilisez simplesat avec l'option DPLL pour vérifier que des nombres sont premiers.

  2. À partir que quelles valeurs de n1, n2 et p est-ce que cela devient trop lent (résultat en 30 secondes environ) ? (Vous pouvez trouvez la liste de tous les nombres premiers ici: allprimes (L. Silvestre))

    À combien de variables / clauses est-ce que cela correspond ? (Vous pouvez utiliser l'option -v / --verbose de simplesat-NOM.py pour afficher cette information.)

    À votre avis, est-ce une bonne méthode pour tester si un nombre est premier ?

  3. Testez les mêmes fichiers avec le programme minisat (paquet Ubuntu / Debian minisat), un SAT solveur très optimisé écrit en C++. À partir de quelles valeurs de n1 et n2 est-ce que minisat devient trop lent ?

    minisat lit la formule dans un fichier au format DIMACS. simplesat-NOM.py peut transformer un fichier .sat au format DIMACS avec l'option -C / --convert: 

    $ python3 multiplication-NOM.py 10 10 179 | python3 simplesat-NOM.py -C - formule.cnf
$ minisat formule.cnf

    Pour obtenir la solution trouvée, il faut fournir un second nom de fichier à minisat pour qu'il y écrive le résultat : 

    $ python3 multiplication-NOM.py 10 10 179 | python3 simplesat-NOM.py -C - formule.cnf
$ minisat formule.cnf formule.sol
$ cat formule.sol
...

    Pour les experts du shell, vous pouvez même utiliser les "substitutions de processus" pour éviter d'avoir passer par des fichier : 

    $ minisat <(python3 multiplication-NOM.py 10 10 179 | python3 simplesat-NOM.py -C) >(cat)