Projet de logique 2013

Les 4 séances de TP de logique visent à implémenter un programme testant la satisfiabilité d'une formule mise sous forme normale conjonctive (CNF), c'est-à-dire sous la forme d'un ensemble de clauses. Un exemple de tel solveur est MiniSat. Ce programme sera ensuite utilisé pour vérifier un circuit d'additionneur représenté à partir d'une spécification, tous deux représentés par des formules.

Ce programme va explorer l'espace de recherche (les combinaisons de valeurs possibles pour les variables) afin de déterminer la satisfiabilité de la formule testée.

Le rendu consistera en une archive .zip ou .tar.gz¹⁾ contenant:

• Le contenu de le projet de départ modifié par vos soins
• Un fichier etudiants.txt contenant les nom(s), prénom(s) et numéro(s) du/des étudiants ayant réalisé le projet (maximum 2 étudiants).
• Un fichier au format .pdf d'au maximum 5 pages A4 en police 11 pts²⁾, contenant:
  • une introduction (max. 0,5 page);
  • une description des difficultés rencontrées, des solutions apportées et une argumentation autour des choix techniques effectués;
  • une conclusion dans laquelle on pourra indiquer d'un point de vue plus personnel les apports et les manques du projet (max. 1 page).

Cette archive est à déposer sur spiral au plus tard le dimanche 22 décembre 2013 à 23h59³⁾. Il fortement recommandé de tester l'accès à la zone de dépôt avant la date butoir⁴⁾.

La zone de dépôt est accessible ici: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=2647044

Le non respect de ces consignes entraînera une sanction dans la note du projet.

L'archive lif11-2013-enonce.zip contient un projet C/C++. Ce projet de départ fourni contient une arborescence de projet avec :

• un fichier /Lisez-moi.txt qui décrit le contenu de l'archive;
• un dossier /UnitTest qui est une bibliothèque pour simplifier l'écriture des tests. Vous n'avez pas à vous intéresser à son contenu;
• un dossier /src qui contient les sources fournies :
  • /src/Makefile permet de construire le projet avec make, mais aussi de lancer les tests, de néttoyer le projet etc.
  • /src/main.cpp et /src/main-test.cpp sont les deux programmes exécutables du projet aux sens évidents : Resolution qui lit une formule et évalue sa satisfiabilité et run-test.
  • /src/formule.hpp et /src/formule.cpp donnent la structure d'arbre de syntaxe abstraite d'une formule et la structure de CNF. Quelques fonctions de base sont implémentées dont notamment formule2string copier qui constituent de bon exemples de fonctions récursives de parcours de l'arbre de syntaxe abstraite.
  • /src/sat.hpp et /src/sat.cpp sont encore quasiment vides et destinés à recevoir vos fonctions.
  • une collection d'autres fichiers dont certains seront générés automatiquement. Il n'est pas utile de les lire. Leur principal objectif est de définir une fonction lit_formule qui crée l'arbre de syntaxe abstraite à partir d'une formule sous fourme de chaîne (typiquement, saisie au clavier ou lue dans un fichier).

<note tip>Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une forge avec un hébergement de dépôts mercurial. Le projet fourni⁵⁾ peut être poussé vers cette forge.

• Pour créer un projet: http://forge.univ-lyon1.fr/projects/new
• Pour être ajouté à un projet, un étudiant doit s'être connecté au moins une fois sur http://forge.univ-lyon1.fr. Le manager du projet pourra alors l'ajouter via Configuration → Membres.
• L'url mercurial⁶⁾ de votre projet est accessible depuis Configuration → Dépôt
• Quelques slides pour la gestion de projet (regarder la partie forge)
• Voir l'aide sur la forge pour un scénario d'utilisation pour des TPs/projets

</note>

Le projet est divisé en quatre grandes étapes qui correspondent grossièrement aux 4 séances de TP prévues :

1. Première partie : prise en main. Les premières fonctions à écrire comme numerote sont conceptuellement simples mais demandent un réel travail d'immersion et de prise en main du projet.
2. Deuxième partie : bases de SAT. Les algorithmes de test SAT travaillant sur des clauses, il faut tout d'abord récursivement convertir une formule arbitraire en forme normale conjonctive. Une version naïve du test de satisfiabilité est ensuite à réaliser
3. Troisième partie : modélisation . L'objectif est ici de fabriquer la formule qui correspond à la spécification de l'additionneur binaire à n-bit (c.f. TD2).
4. Quatrième partie : optimisations. Il s'agit d'améliorer les performances du solveur en ajoutant des stratégies et des index permettant de couper l'arbre de recherche.

<note important> Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci n'implique pas de devoir s'échanger les sources entre binômes. </note>

<note warning> Pour de l'aide sur les bases du C++ utiles à ce TP voir :

• l'introduction au C++
• le code d'exemple.

</note>

Le projet est fourni avec la bibliothèque UnitTest++ qui simplifie (grandement) l'expression et la gestion de tests unitaires. Un test peut être vu comme une fonction sans arguments dont on attend que le résultat s'évalue à true. Dans UnitTest++ un test est une macro de la forme TEST(nom_du_test) { code du test }. Dans le corps de cette fonction/macro certaines assertions CHECK(test) sont vérifiées. Il est possible de faire autant de CHECK que l'on veut dans un TEST, possiblement aucun. Le fichier main-test.cpp contient l'exemple initial suivant :

// Un test simple qui réussit
TEST(test1) {
  CHECK(2 == 1+1);
}
 
// Un test simple qui échoue
TEST(test2) {
  CHECK(2 == 1+2);
}

Le Makefile fourni dans le projet de départ permet d'exécuter les tests définis dans main-test.cpp simplement via make test.

• Prendre connaissance et comprendre le contenu du fichier Lisez-moi.txt. Prendre particulièrement attention à ce qu'il est DEMANDE DE NE PAS FAIRE .
• Comprendre le test TEST(lit_ecrit_formule).
• Lancer la compilation et l'exécution des tests via make test. Comprendre l'affichage produit. Ne pas s'inquiéter des warnings (relativement inoffensifs) produits lors de la compilation du code qui vous est fourni.

Les structures codant les clauses et les formules conjonctives (que l'on abrégera désormais CNF pour Conjunctive Normal Form) sont définies par des typedef utilisant différents conteneurs de la STL. Une cnf_t est un tableau dynamique (vector) qui contient des clauses cls_t représentées par des ensembles de littéraux (set), les littéraux lit_t étant codés par des entiers.

typedef unsigned int  var_t;
typedef int           lit_t;
typedef set<lit_t>    cls_t;
typedef vector<cls_t> cnf_t;

• La classe vector permet un accès en temps constant via ses indices avec c[i] comme les tableaux C et offre l'avantage d'être dynamique. On peut par exemple ajouter autant d'éléments que l'on veut avec c.push_back(). Le nombre d'élément d'un vector est donnée avec c.size().
• La classe set offre l'avantage de garantir l'unicité et un ordre total sur les éléments qu'il contient. En revanche, il est obligatoire d'utiliser les itérateurs pour parcourir son contenu, voir cet exemple.

• Avec un itérateur de type cls_t::const_iterator, écrire une fonction pour l'affichage de clauses, ayant la signature string cls2string(const cls_t& cl). implémenter la méthode ostream& operator«(ostream& out, const cls_t& cl) qui permettra d'afficher des élément sur un ostream comme cout et cerr. Voir l'exemple de l'affichage des éléments d’un conteneur.
• Écrire un TEST⁷⁾ qui crée une clause cl1 contenant les littéraux 1, 4, 7 et 6⁸⁾ et une autre clause cl2 de votre choix puis les affiche.
• Écrire un TEST avec les vérifications suivantes :
  • CHECK(cl1 != cl2);
  • CHECK(cl2 != cl1);
  • CHECK(cl1 == cl1);
  • CHECK(cl2 == cl2);
• Vérifier que les quatre tests s'évaluent à true.

• Avec un itérateur ou avec size(), écrire une fonction d'affichage pour les CNFs, ayant la signature string cnf2string(const cnf_t& c). implémenter la méthode ostream& operator«(ostream& out, const cnf_t& c). c. Cette méthode utilisera l'opérateur précédemment défini pour cls_t.
• Ajouter un TEST pour l'affichage d'une CNF c contenant les clauses cl1 et cl2.
• Écrire une fonction bool est_dans(const cls_t& cl, const cnf_t& c) permettant de tester l'appartenance d'une clause à une CNF.
• Écrire un TEST pour vérifier notamment que est_dans(cl1, c) et que est_dans(cl2, c).

Pour des raisons d'efficacité, il faut éviter de représenter les variables propositionnelles par des chaînes (classe string en C++) et leur préférer des entiers (var_t dans le projet). Il faut donc écrire une fonction void numerote(formule f, map<string,var_t> & corresp) permettant de numéroter les variables d'une formule. La classe map de la STL est un conteneur associatif qui permet, dans le cas de map<string,var_t>, de faire correspondre une unique variable à une chaîne⁹⁾. L'algorithme de numerote est le suivant :

• si la formule est une variable
  • si la variable a déjà un numéro, ne rien faire;
  • sinon, lui attribuer un numéro (on peut prendre la taille actuelle de corresp comme numéro) et ajouter la correspondance entre le nom de la variable et ce numéro dans corresp;
• sinon, appeler récursivement la fonction de numérotation sur le ou les argument(s).

Pour l'efficacité, on représentera également les littéraux (c'est-à-dire des variables avec ou sans négation) par des entiers :

• Les littéraux positifs sont représentés par les entiers naturels pairs. On injecte ainsi la variable p qui vaut 2 dans l'ensemble des littéraux positifs en multipliant par 2, le littéral p vaut ainsi 4 : c'est le 3ème entier pair associé à la 3ème variable.
• Les littéraux négatifs sont représentés par les entiers naturels impairs. Le littéral ~p vaut ainsi 5 : c'est le 3ème entier impair associé à la 3ème variable.

Il faut ainsi prêter garder à ne pas mélanger la proposition dont la string est p avec sa représentation numérotée dans un map<string,var_t>, ici 2, et les littéraux associés dont les formules sont p et ~p valant respectivement 4 et 5. Pour cela, il est vivement recommander d'utiliser systématiquement par la suite les fonctions var2lit et neg demandées en exercices.

• Regarder et comprendre le code de la fonction string formule2string(formule f) de transformation des formules en chaînes de caractères.
• Écrire la méthode void numerote(formule f, map<string,var_t> & m). On inspirera pour cela de formule2string ainsi que de l'exemple d'utilisation de map.
• Écrire un test unitaire qui vérifie le nombre de variables comptées lors de la numérotation de quelques formules.

• Écrire la fonction lit_t var2lit(var_t v, bool p = true) qui injecte une variable v dans l'ensemble des littéraux. Le booléen p indique si le littéral est positif ou négatif. La déclaration bool p = true permet d'affecter une valeur par défaut à ce paramètre ce qui permet de considérer alors var2lit comme une fonction à un seul argument.
• Écrire la fonction lit_t neg(lit_t l) qui prend un littéral et retourne sa négation. La fonction renvoie donc l+1 ou l-1 selon le cas.
• Écrire la fonction var_t lit2var(lit_t l) qui prend un littéral en argument et retourne sa variable.
• Écrire la fonction bool positif(lit_t l) qui renvoie true si le littéral passé en argument est un littéral positif.
• Tester ces fonctions avec UnitTest++.

<note important> Cette première partie donne les bases sur lesquelles s’appuyer dans la suite du projet. Ces bases doivent être solides. Bien garder les tests unitaires rédigés au fur et à mesure de l'avancement : ils permettent de s'assurer de la correction du code, de la non-régression lors des modifications et sont attendus dans le rendu final du projet comme la preuve que le programme a été convenablement testé. </note>

La transformation de Tseitin (c.f. TD du 07/10) permet d'obtenir à partir d'une formule f une CNF ayant la propriété d'être satisfiable si et seulement si f l'est. Cette transformation se fait via une fonction récursive tseitin, qui ajoute des clauses générées à une CNF passée en argument. Son principe de fonctionnement est le suivant: étant donnée f, la fonction renvoie un nouveau littéral l ainsi qu'une CNF c tels que c et l s'évaluent à vrai si et seulement si f s'évalue à vrai. La fonction tseitin(f) peut être algorithmiquement définie comme suit:

• tseitin(p) = (p,vide)
• tseitin(¬f) :
  • soit (p',c') = tseitin(f)
  • renvoyer (¬p',c')
• tseitin(f1 ∨ f2) :
  • soient (p1,c1) = tseitin(f1), (p2,c2) = tseitin(f2) et p un nouveau littéral
  • renvoyer (p, (¬p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1) ∧ (p ∨ ¬p2) ∧ c1 ∧ c2)
• tseitin(f1 ∧ f2) :
  • soient (p1,c1) = tseitin(f1), (p2,c2) = tseitin(f2) et p un nouveau littéral
  • renvoyer (p, (p ∨ ¬p1 ∨ ¬p2) ∧ (¬p ∨ p1) ∧ (¬p ∨ p2) ∧ c1 ∧ c2)
• tseitin(f1 ⇒ f2) :
  • soient (p1,c1) = tseitin(f1), (p2,c2) = tseitin(f2) et p un nouveau littéral
  • renvoyer (p, (¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2) ∧ c1 ∧ c2)
• tseitin(f1 ⇔ f2) :
  • soient (p1,c1) = tseitin(f1), (p2,c2) = tseitin(f2) et p un nouveau littéral
  • renvoyer (p, (¬p ∨ ¬p1 ∨ p2) ∧ (¬p ∨ p1 ∨ ¬p2) ∧ (p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1 ∨ ¬p2) ∧ c1 ∧ c2)

La CNF équisatifiable finale est obtenue comme suit:

• soit (l,c) = tseitin(f)
• la CNF est l ∧ c

On peut remarquer que les CNFs ne font que grossir, on peut ainsi passer la CNF en argument par référence : les ensembles de clauses c1 et c2 dans (p, … ∧ c1 ∧ c2) sont produites par les appels récursifs de tseitin. On passe également un compteur par référence var_t & next pour générer de nouvelles variables fraiches. Ainsi en C/C++ on définira les deux fonctions :

lit_t tseitin(formule f, const map<string, var_t> & m, cnf_t & c, var_t & next);
cnf_t tseitin(formule f);

<note tip> On donne l'exemple suivant avec f = (a ∨ b) ⇒ c, m le dictionnaire tel que a est numéroté par 0, b par 1, c par 2 (la prochaine variable fraîche est donc next = 3) et cl ={} un ensemble initialement vide de clauses. On a les appels récursifs suivants :

• tseitin((a ∨ b) ⇒ c, m, cl = {}, 3)
  • tseitin((a ∨ b), cl, 3)
    • tseitin(a, cl, 3) 0 est le lit positif correspondant à a, on ajoute rien à cl
    • tseitin(b, cl, 3) 2 est le lit positif correspondant à b, on ajoute rien à cl
  • on a les 2 branches de (a ∨ b) on ajoute donc (¬p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1) ∧ (p ∨ ¬p2) à cl pour obtenir cl = 7_0_2_6_1_6_3 et 6 est le littéral positif qui code (a ∨ b)
  • tseitin(c, cl = 7_0_2_6_1_6_3, 4) 4 est le lit positif correspondant à c, on ajoute rien à cl
• on a les 2 branches de (a ∨ b) ⇒ c on ajoute donc (¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2) à cl pour obtenir cl = 7_0_2_6_1_6_3_9_7_4_8_6_8_5 et 8 est le litéral positif qui code f

Il faut enfin ajouter {8} à cl pour obtenir finalement cl= 7_0_2_6_1_6_3_9_7_4_8_6_8_5_8 comme codage de Tseitin de (a ∨ b) ⇒ c. </note>

<note warning> La fonction tseitin a m comme paramètre en lecture seule (déclaration const map<string, var_t> & m), or si vous utilisez m[], comme pour un tableau, vous allez avoir une erreur assez peu intelligible car [] est une méthode qui peut modifier m. A la place, il faut utiliser find qui est une méthode en lecture seule.

</note>

• Écrire la fonction lit_t tseitin(formule, map<string, int>, cnf_t, var_t) telle que décrite.
• Écrire les tests unitaires pour vérifier chacun des cas du switch (f→op) de la fonction précédente.
• Écrire la fonction cnf_t tseitin(formule f) qui appelle numerote et l'autre fonction tseitin.
• Écrire les tests unitaires vérifiant le nombre de clauses et de littéraux générés lors de cette transformation.

Au cours de l'exploration de l'espace de recherche, on peut représenter les interprétations des variables propositionnelles par un tableau qui à chaque numéro de variable fait correspondre une valeur (de type val_t):

• VRAI si la variable est affectée à vrai
• FAUX si la variable est affectée à faux
• INDETERMINEE si la variable n'est pas affectée

• Écrire la fonction val_t valeur_lit(vector<val_t>, lit_t) qui étant donnés le tableau des valeurs des variables suivant leur numéro et un littéral donne la valeur de ce littéral.
• Écrire la fonction val_t valeur_clause(vector<val_t>, cls_t) qui étant utilise la fonction précédente pour déterminer la valeur de la clause.
  Remarque: si la clause contient un littéral qui vaut VRAI, alors elle sa valeur est VRAI. Si tous les littéraux de la clause valent FAUX, alors la clause vaut FAUX. Sinon sa valeur est INDETERMINEE.
• Écrire la fonction val_t valeur_cnf(vector<val_t>, cnf_t) qui utilise la fonction précédente pour déterminer la valeur de la CNF.
  Remarque: si la CNF contient une clause qui vaut FAUX, alors elle vaut FAUX. Si toutes ses clauses valent VRAI, alors elle vaut VRAI. Sinon sa valeur est INDETERMINEE.

<note tip> Par exemple, pour évaluer la valeur de vérité de la formule f = (a ∨ b) ⇒ c, on a besoin de connaître les valeurs des variables a, b et c. Considérons la correspondance m = { a ↦ 0; b ↦ 1; c ↦ 2; d ↦ 3} et l’interprétation où a & c sont VRAI, b FAUX et d INDETERMINEE. Cette interprétation est représentée par le vecteur [VRAI | FAUX | VRAI | INDETERMINEE]. On a dans cet exemple valeur_lit(v, ¬c) = FAUX, valeur_lit(v, ¬b) = VRAI et valeur_lit(v, ¬d) = INDETERMINEE

</note>

Écrire la fonction récursive

bool cherche(vector<val_t> & valeurs, var_t suiv, const cnf_t & cnf); 

qui renvoie true si cnf est satisfiable, sachant que:

• valeur contient les valeurs des variables
• suiv est une variable non affectée. On considère que toutes les variables dont le numéro est inférieur au numéro de suiv ont une valeur dans valeurs.

La fonction procèdera comme suit:

1. si suiv est supérieur à la taille de valeurs, alors évaluer la CNF et renvoyer VRAI si elle est satisfaite.
2. sinon:
   1. mettre la valeur de suiv à VRAI dans valeurs
   2. Appeler récursivement la fonction avec suiv+1
      1. si l'appel récursif renvoie true la CNF est satisfiable et on peut renvoyer true
      2. sinon mettre la valeur de suiv à FAUX dans valeurs
   3. Appeler à nouveau récursivement la fonction avec suiv+1
      1. si l'appel récursif renvoie true la CNF est satisfiable et on peut renvoyer true
      2. sinon la CNF n'est pas satisfiable pour l'affectation courante: remettre la valeur de suiv à INDETERMINEE, puis renvoyer false.

<note warning>Dans la définition de la fonction cherche, on suppose que la longueur du tableau vector<val_t> & valeurs passé en paramètre est égale au nombre de variables (différentes) de la cnf. Ainsi:

• il n'y a pas besoin de faire de push_back ou de resize, l'allocation et l'initialisation est à la charge de la fonction qui appelle cherche ;
• on peut déterminer que toute les variables ont été affectées en comparant suiv et valeurs.size().

</note>

Modifier la fonction main de façon à:

1. transformer la formule lue en CNF équisatisfiable;
2. initialiser un tableau de valeurs à INDETERMINEE pour chaque identifiant de variable;
3. appeler la fonction cherche et afficher le résultat.

<note important> A la fin de cette partie, le projet dispose de toutes les fonctionnalités pour vérifier la satisfiabilité (et donc aussi la validité) d'une formule. L'efficacité algorithmique de la méthode dépend des stratégies de recherche implémentée dans cherche et de simplification que l'on peut apporter lors du calcul de valeurs de la CNF, pour éviter d'effectuer trop de calculs. C'est l'objet de la quatrième partie du projet.

Avant cela on va coder dans la troisième partie une application qui utilise le solveur: un vérificateur d'additionneur binaire n-bits. </note>

Dans cette partie, on modélise un additionneur n-bits (la spécification, cf TD2) qui est utilisé pour vérifier un additionneur dont la représentation est donnée dans un fichier.

La génération d'une spécification pour l'additionneur n-bits fait utilise des substitutions. Une substitution sera représentée par une map<string,formule> qui à chaque variable substituée associe la formule qui la remplacera.

• En s'appuyant sur la définition de l'application d'une substitution (cf mémo 1), coder la fonction récursive

  formule applique(formule f, const map<string,formule> & substitution)

  qui fabrique la formule sur laquelle la substitution à été appliquée à partir de la formule de départ et de la substitution à appliquer. Attention, la formule de départ ne doit pas être modéfiée par l'application de la substitution.

La première étape pour vérifier un additionneur n-bits consiste à générer sa spécification sous forme de formules.

On considère que les 2 * n entrées sont données par les variables p1 … pn et q1 … qn et que les (n+1) sorties sont codées par les formules A1 … An, B (B est le dernier bit de a somme, celui avec le poids le plus fort).

On utilisera les formules suivantes qui expriment la somme et la retenue pour un additionneur qui calcule la somme de trois entrée à 1 bit :

• S = t ⇔(u ⇔ w) : cette formule est vraie si le chiffre des unités de la somme des valeurs de t,u et w est 1 (première formule de l'exercice 2.1 du TD2)
• R = (t ⇒ (u ∨ w)) ∧ (¬t ⇒ (u ∧ w)) : cette formule est vrai si la retenue de la somme des valeurs de t, u et w est 1 (deuxième formule de l'exercice 2.1 du TD2).

La génération de cette spécification par récurrence pour n-bits peut être définie comme suit:

• Additionneur 1-bit : on retourne le vecteur V=[B,A1] de taille 2 avec
  • A1 = S [ p1/t, q1 / u, ⊥ / w], on calcule cette formule en construisant la substitution [ p1/t, q1 / u, ⊥ / w] en en l'appliquant à S avec la méthode applique
  • B = R [ p1/t, q1 / u, ⊥ / w], idem que précédemment, sauf que c'est R qui est modifiée et plus S.
• Additionneur n-bits : soit V'[B',A'n-1,…,A'1] le vecteur de taille n obtenu pour un additionneur de taille n-1, on va construire le vecteur résultat V =[B,An,An-1,…,A1] de taille n+1
  • A1 à An-1 : on ne change rien : A'i=Ai ;
  • An = S [ pn / t, qn / u, B' / w ], B' est le dernier bit de sortie d'un additionneur à n-1-bit que l'on va l'additionner aux bits pnet qn. Autrement dit, B', est la retenue de la somme de pn-1et qn-1 quand on pose l'addition ;
  • B = R [ pn / t, qn / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à n-1-bits, c'est le bit de poids le plus fort du vecteur V', c'est la retenue de l'addition de pn et qn evec la retenue de pn-1et qn-1.

• Écrire la fonction additionneur suivante qui construira les formule Ai en commençant par 1 :

  vector<formule> additionneur(int taille);

• Écrire les tests unitaires associé et vérifier pour n=2 que votre formule est bien celle d'un additionneur binaire
• Modifier ensuite le main de façon à accepter un argument --check-adder. Si cet argument est présent on supposera par convention que le fichier de formules contient les formules A'1, … , A'n, B'n d'un additionneur n-bits. On appellera la fonction additionneur(n) pour récupérer les n+1 formules de la spécification correspondante. On construira la formule ¬( (A1 ⇔ A'1) ∧ … ∧ (An ⇔ A'n) ∧ (Bn ⇔ B'n) ). On testera la satisfiabilité de cette formule: si elle est insatisfiable, l'additionneur passé en argument est correct.

<note tip>Vous disposez de la fonction lit_formules qui fonctionne similairement à lit_formule, mais en lit plusieurs d'un coup et renvoie un vector<formule> (c.f. parser.hpp).</note>

<note tip>En testant votre programme, même avec des additionneurs très petits, vous verrez que le temps de calcul est élevé. La partie suivante vise à améliorer cette situation. La partie suivante est indépendante de la présente, le deux peuvent donc être travaillées en parallèle.</note>

L'exploration de l'espace de recherche implémentée précédement ne teste la satisfaction de la forme conjonctive que lorsque la valeur de toutes les variables est connue. Un moyen d'améliorer l'efficacité du solveur consiste à tester systématiquement la valeur de la CNF à chaque affectation de variable de façon à éviter d'explorer un morceau de l'arbre de recherche dont on sait qu'il mènera toujours à des évaluation de la CNF valant FAUX.

Modifier la fonction cherche pour tester la satisfaction à chaque affectation de variable de façon à détecter au plus tôt les combinaisons de valeurs partielles insatisfiables. Si la CNF vaut FAUX, alors on peut renvoyer directement false sans faire l'appel récursif. Attention, il faut bien penser à remettre id_var à INDETERMINEE avant de renvoyer false, sous peine de fausser la suite de l'exploration de l'arbre de recherche.

Remarque: cette remise à zéro fait partie du “retour arrière” lors de l'exploration de l'arbre de recherche.

Pour améliorer l'efficacité des tests de satisfiabilité, l'étape suivante consiste à indexer les clauses par les littéraux qui les contiennent. Plus précisément, il s'agit de construire une structure qui associe à chaque littéral la liste des clauses dans lequel il apparaît. Il suffit de tester uniquement cette liste lors de l'affectation d'un littéral à faux pour vérifier si l'affectation rend la forme conjonctive insatisfaite.

La structure d'indexation proposée consiste en un tableau contenant des listes de clauses. Les indice du tableau correspondent aux numéros des littéraux.

• Écrire une fonction

  vector<vector<cls_t> > indexe_clauses(const cnf_t& cnf)

  qui renvoie une telle structure initialisée en fonction de la forme conjonctive passée en argument.

• Écrire une fonction

  bool contient_insatisfaite(var_t variable, const vector<val_t>& valeurs,const vector<vector<cls_t> >& index_clauses)

  • index_clauses est la structure d'indexation des clauses
  • variable est le numéro d'une variable. On appelle l le littéral correspondant à variable et prenant la valeur FAUX
  • valeurs est le tableau des valeurs affectées aux variables
  • la fonction renvoie true si une des clauses contenant l s'évalue à FAUX dans l'interprétation courante (i.e. valeurs).
• Remplacer les appels à valeur_cnf dans cherche par une utilisation de la fonction contient_insatisfaite.

L'objectif de cette optimisation est, étant données certaines valeurs choisies pour les variables n°1 à n, d'affecter les variables dont la valeur est INDETERMINEE et qui doivent nécessairement prendre une certaine valeur pour que la CNF aie une chance de s'évaluer à VRAI.

Pour cela, on s'appuie sur la remarque suivante. Soit une clause L1 ∨ … ∨ Lk. Si tous les littéraux de cette clause valent FAUX, sauf un certain Lj qui vaut INDETERMINEE, alors cette clause ne pourra s'évaluer à VRAI que si Lj prend la valeur VRAI. On dira que cette clause est devenue unitaire. Il est ainsi inutile de tester les valeurs pour la variable V de Lj: si Lj est un littéral positif, V doit prendre la valeur VRAI, si Lj est un littéral négatif, elle doit prendre la valeur FAUX.

On peut également remarquer que si Lj se voit affecter la valeur VRAI, alors ¬Lj a pour valeur FAUX. Cela peut avoir deux conséquences:

• La CNF peut s'évaluer à FAUX auquel cas on sait que les valeurs choisies pour les variables n°1 à n ne permettront pas de montrer que la CNF est satisfiable;
• Une ou plusieurs autres clauses peuvent devenir unitaires, ceci entrainant l'affectation d'autres variables et ainsi de suite jusqu'à ce que la CNF s'évalue à FAUX ou qu'aucune clause ne soit rendue unitaire.

On peut définir une fonction propage qui va se charger d'effectuer la propagation unitaire. A la manière de contient_insatisfaite, elle va s'appuyer sur l'index des clauses pour trouver rapidement les clauses à traiter. En effet, à l'exception des clauses qui sont unitaire dès le début, une clause ne peut être rendue unitaire que si un de ses littéraux est affecté à FAUX. On peut donc, lors de l'affectation d'une valeur à une variable, savoir, grâce à l'index, quelles sont les clauses à tester pour savoir si elles sont unitaires.

Lors du retour arrière, il est important de défaire le travail effectué par la propagation unitaire. Comme celle-ci peut toucher des variables dont les numéros ne se suivent pas forcément, il faudra stocker la liste des variables à remettre à zéro au cas où le choix de valeur ayant déclenché la propagation unitaire ne permet pas de montrer que la CNF est satisfiable.

1. Créer une nouvelle fonction

   vector<var_t> propage(lit_t lit, vector<val_t> & valeurs, cnf_t & cnf, vector<vector<cls_t> > & index)

   Cette fonction renvoie la liste des variables affectées. Par convention, si cette liste est vide on supposera que la propagation a mené à une contradiction. La fonction aura le comportement suivant:

   • Initialiser le vector résultat à un vector vide
   • Initialiser un vector<lit_t> contenant au départ lit. Cette structure contiendra la liste courante des littéraux que l'on veut affecter à VRAI.
   • Tant qu'il reste des littéraux à traiter:
     • Retirer un littéral L des littéraux à traiter
       • Vérifier si le littéral a déjà une valeur. Si c'est le cas, ne rien faire.
     • Ajouter la variable V correspondant à L dans le vector résultat
     • Affecter la bonne valeur à V
     • Utiliser l'index pour accéder aux clauses à vérifier (pour propagation unitaire ou contradiction¹⁰⁾ )
       • Pour chaque clause unitaire trouvée, ajouté le littéral qui n'a pas de valeur dans les littéraux à traiter
       • Si une clause s'évalue à FAUX alors la CNF aussi et la propagation unitaire s'arrête. On remet alors à INDETERMINEE la valeur des variables du vector résultat, puis on renvoie un vector vide.
   • Renvoyer le résultat
2. Modifier la fonction cherche de façon à utiliser propage au lieu de contient_insatisfaite
   • En particulier, bien penser à remettre la valeur des variables affectée par propage à INDETERMINEE lors des retours arrière.

• Jean Gallier: Logic for Computer Science: Foundations of Automatic Theorem Proving.

Faire fonctionner le projet sous Windows nécessite l'utilisation de Cygwin (installé en salle TP Nautibus, à vérifier pour les salles Ariane). La compilation peut se faire en invoquant make comme sous Linux. Sous Cygwin, les lettres des lecteurs sont des répertoires dans /cygdrive. Ainsi pour aller dans le répertoire U:\LIF11\projet il faut faire cd /cygdrive/u/LIF11/projet

Il faut par ailleurs modifier le Makefile en changeant l'option -std=c++0x en -std=gnu++0x.

La version de g++ fournie avec MacOSX est parfois trop vieille pour fonctionner avec l'option -std=c++0x. Il alors faut installer une version plus récente du compilateur (e.g. g++-4.7) avec Homebrew, Macports ou encore Fink.

Pour compiler il faut ensuite faire (dans le cas où le g++ installé est la version 4.7): make CXX=g++-4.7, ou bien make CXX=g++-4.7 test pour exécuter les tests.

• v0, 09/10/13 : version initiale par EC;
• v1, 14/10/13: maj date rendu, dépôt spiral, projet initial et lien forge.
• v2, 15/10/13: ajout de fonctions: lit2var et positif.
• v3, 16/10/13: informations compilation Windows/MacOSX
• v4, 16/11/13: aide sur erreur m[] qui n'est pas const
• v5, 24/11/13: modif partie sur additionneur
• v6, 18/12/13: mise à jour de la description de la fonction cherche dans sa première version