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

• en omettant les clauses qui contiennent lit,

• en remplaçant les clauses qui contiennent -lit par la même clause, sans -lit,

• en laissant les autres clauses inchangées. -

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 :

   $ ./naivesat-NOM.py test.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 (x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃ ∨ x₄) ∧ (x₂ ∨ ¬x₄).

   Le résultat est il bien correct ?

$ ./naivesat-NOM.py test.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], [2, 3, -4], [3, 4], [-2, -3, 4], [-4, -2]]

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 ? (Indice: il faudra rajouter des clauses pour interdire la solution trouvée)

Pour les petites formules, il est parfois intéressant de chercher toutes les solutions à un problème.

1. En partant du code de la fonction solve, écrivez une fonction all_solutions qui affiche toutes les solutions, au fur et à mesure qu'elle les trouve.

   Cette fonction aura exactement le même "squelette" que solve, mais :

   • elle ne renvoie pas de solution, elle les affiche avec la fonction print_sol,

   • elle explore toujours les deux alternative "+lit" et "-lit".

   Il ne sera donc plus possible d'utiliser le or du Python qui ne calcule pas la seconde alternative.

2. Essayez (sans y passer trop de temps) de renvoyer le nombre de solutions trouvées.

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 coeur est en position 3

     • ...

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

   • 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 très facile.)

   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 en 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 :

   ~  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 naivesat-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.

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

   • écrivez le corps de la fonction implies,

   • écrivez le corps de la fonction constraints_1,

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

   Ce programme, lorsqu'on le lance avec

   $ ./zebra-NOM.py
   ...

   affiche à l'écran la formule CNF correspondant au problème de Einstein.

2. lancez naivesat-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

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

   et utiliser naivesat-NOM.py comme précédemment, "brancher" les 2 programmes zebra-NOM.py et naivesat-NOM.py avec

   $ ./zebra-NOM.py | ./naivesat-NOM.py

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

Créez un fichier xor3-NOM.sat approprié, et en utilisant votre fonction all_solutions, vérifiez que les solutions sont effectivement les valeurs de a, b, c et s qui vérifient la formule s ⇔ (a ⊕ b ⊕ c).

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

É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).

1. 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 s_k := a_k ⊕ b_k ⊕ c_k et c_k+1 := (a_k ∧ b_k) ∨ (a_k ∧ c_k) ∨ (b_k ∧ c_k)

   • imposer les valeurs de s₀, s₁, ... pour obtenir le résultat s.

   • s₀ correspond à la parité de s,

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

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

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

   • etc.

2. 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 pouvez lancer le programme avec 2 arguments : la valeur de n (nombre de bits) et la valeurs de s (somme voulue).

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

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

$ ./addition-NOM.py 4 7 | ./naivesat-NOM.py -v
>>> the formula contains 17 clauses and 70 variables, for a total of 262 literals
SATISFIABLE
~r1 ~r5 s1 s2 s3 ~s4 a1 ~b1 ~r2 a2 ~b2 ~r3 a3 ~b3 ~r4 ~a4 ~b4

Testez (sur des petites valeurs) en utilisant la fonction all_solutions 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.

1. Ajoutez, tout à la fin du fichier, les clauses pertinentes pour forcer les valeurs de p₀, p₁, ... p__n aux bits de p. (C'est identique à ce que vous avez fait pour forcer )

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

   $ ./ multiplication.py 4 4 48 | ./naivesat-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. À partir que quelles valeurs de n1 et n2 est-ce que la naivesat-NOM.py devient trop lent (résultat en 30 secondes environ) ?

   À combien de variables / clauses est-ce que cela correspond ?

2. 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. naivesat-NOM.py peut sauvegarder une formule au format DIMACS avec l'option -O / --output:

   $ ./multiplication.py 10 10 179 | ./naivesat-NOM.py -O "" formule.cnf
   $ minisat formule.cnf

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

   $ minisat <(./multiplication.py 10 10 179 | ./naivesat-NOM.py -O)

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

   $ ./multiplication.py 10 10 179 | ./naivesat-NOM.py -O "" formule.cnf
   $ minisat formule.cnf formule.sol

   Pour éviter de passer par un fichier, vous pouvez faire une autre substitution de processus :

   $ minisat <(./multiplication.py 10 10 179 | ./naivesat-NOM.py -O) >(cat)

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é 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 naivesat-NOM.py.

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

4. Comparez l'efficacité du solveur naif optimisé avec minisat et documentez vos résultats.