Projet de LIF11 2015: vérification d'un additionneur binaire et résolution

Les 4 séances de TP de logique visent à implémenter un programme permettant de vérifier un circuit d'additionneur binaire. Il utilisera pour cela un solveur testant la (non)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. Cependant, contrairement à MiniSat, le solveur qui sera implémenté en TP utilisera directement le principe de résolution pour prouver l'insatisfiabilité de formules.

<note tip>Un forum est mis à votre disposition pour échanger sur le projet. Attention il ne s'agit pas de déposer du code source pour le mettre à disposition des autres, mais bien de poser / de répondre à des questions autour du projet.</note>

Le rendu intermédiaire consistera en une archive zip¹⁾ contenant:

• Le contenu de le projet de départ modifié par vos soins pour les deux premières parties.
• 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).

Le nom de l'archive sera de la forme nom1-nom2.zip où nom1 et nom2 sont les noms des deux étudiants du binôme.

Cette archive est à déposer sur spiral au plus tard le vendredi 13 novembre 2015 à 23h59 dimanche 15 novembre 2015 à 23h59.

La zone de dépôt pour le rendu intermédiaire est accessible ici: dépôt fermé

<note tip>Ce rendu intermédiaire concerne les parties 1 (prise en main) et 2 (modélisation) du projet</note>

Le rendu final 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).

Le nom de l'archive sera de la forme nom1-nom2.zip où nom1 et nom2 sont les noms des deux étudiants du binôme.

Cette archive est à déposer sur spiral au plus tard le vendredi 18 décembre 2015 à 23h59 dimanche 20 décembre 2015 à 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 pour le rendu final est accessible ici: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=5015155

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

L'archive inf3034l-2015-base.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-cpp 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 : main est utilisé pour construire le programme 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/resolution.hpp et /src/resolution.cpp sont encore quasiment vides et destinés à recevoir vos fonctions concernant le solveur par résolution.
  • /src/adder.hpp et /src/adder.cpp sont encore quasiment vides et destinés à recevoir vos fonctions concernant la génération de formules permettant de vérifier un additionneur.
  • 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 (normalement déjà vu en LIF7). 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 : modélisation. L'objectif est ici de fabriquer la formule qui correspond à la spécification de l'additionneur binaire à n-bit (c.f. TD2), de lire une implémentation de l'additionneur sous forme de formule, puis de créer une formule permettant de vérifier la correction de cette implémentation.
3. Troisième partie : résolution naïve . L'objectif de cette partie est réaliser un solveur naïf basé sur la méthode de résolution
4. Quatrième partie : optimisations. Il s'agit d'améliorer les performances du solveur en ajoutant des stratégies et des index permettant d'accélérer le processus de résolution.

<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, 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(), implémenter la méthode ostream& operator <<(ostream& out, const cnf_t& 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 tip> Par exemple, on aura var2lit(2,true) = var2lit(2) = 4, var2lit(2,false) = 5, neg(4) = 5, neg(5)=4, lit2var(4) = 2, lit2var(5) = 2, positif(4) = true et positif(5) = false. Plus généralement, on a les égalités suivantes entre les fonctions var2lit, positif et lit2var : ∀ v∈var_t, ∀ b∈ bool, positif(var2lit(v,b)) = b ∧ lit2var(var2lit(v,b)) = v </note>

<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 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. formule.hpp défini le type subs_t comme alias de map<string,formule>.

• 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 subs_t & 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 modifiée par l'application de la substitution.

<note tip>Attention, afin de simplifier la gestion de la mémoire, on suppose que chaque formule n'est utilisée qu'une seule fois, ce qui signifie que lorsqu'une variable est remplacée, elle l'est par une copie de la formule associée et pas par la formule directement.</note>

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=[A₁,B] 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'=[A'₁, … , A'_n-1,B'] le vecteur de taille n obtenu pour un additionneur de taille n-1, on va construire le vecteur résultat V =[A'₁, … , A'_n-1, A'_n,B'] 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, i.e. B' est le bit de poids le plus fort du vecteur V'. C'est-à-dire que B est la retenue de l'addition de pn et qn avec la retenue de pn-1 et qn-1.

• Écrire la fonction additionneur suivante qui construira les formule Ai, en commençant par A1 jusqu'à An, puis An+1 (i.e. la dernière valeur de B):

  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

Une fois obtenues les formules de spécification de l'additionneur n-bits via additionneur, on peut les comparer à celle de l'additionneur à vérifier (que l'on appelera additionneur candidat). Pour cela, il suffit de vérifier que chaque sortie de l'additionneur candidat est équivalente à la sortie correspondante de la spécification.

Coder la fonction formule_verifier_additionneur qui génère une formule valide si et seulement si l'additionneur candidat passé en argument est correct. Si on suppose que les sorties de l'additionneur n-bits candidat sont notées A'1, … , A'n, A'n+1, on peut générer la spécification A1, … , An, An+1 via la fonction additionneur, puis construite la formule ( (A1 ⇔ A'1) ∧ … ∧ (An ⇔ A'n) ∧ (An+1 ⇔ A'n+1) ). Cette dernière formule est valide si et seulement si l'additionneur candidat est correct.

<note tip>La fonction main dans main.cpp utilisera la fonction formule_verifier_additionneur si on passe l'argument --check-adder en ligne de commande.</note>

La partie suivante vise à implémenter un solveur vérifiant la non satisfiabilité d'une formule (i.e. la validité de sa négation) via la méthode de résolution.

Afin de vous permettre de tester en ligne de commande l'état actuel du projet vous pouvez ajouter le code suivant à la fin de “formule.cpp”:

////////////////////////////////////////////////////////////////////////////////
// Code pour la réécriture en CNF équivalente d'une formule
cnf_t cnf_union(const cnf_t& lhs, const cnf_t& rhs){
  cnf_t res = lhs;
  res.reserve(lhs.size() + rhs.size());
  res.insert(res.end(), rhs.cbegin(), rhs.cend());  
  return res;
}
 
cnf_t cnf_product(const cnf_t& lhs, const cnf_t& rhs){
//product E x F = { (x union y) | x in E /\ y in F}
  cnf_t res;
  cls_t xy;
  for (auto& x : lhs){
      for (auto& y : rhs){
        xy.clear();
        set_union(x.cbegin(), x.cend(), y.cbegin(), y.cend(), std::inserter(xy, xy.end()));//
        res.push_back(xy);
      }
  }
  return res;
}
 
// Déclaration pour les appels mutuellement recursifs
cnf_t rewriteDNF(formule f, const map<string,var_t> & corresp, bool pos=true);
 
cnf_t rewriteCNF(formule f, const map<string,var_t> & c, bool pos) {
  cnf_t res;
  switch (f->op) {
    case o_variable:{
      res = { {var2lit(c.find(* (f->nom))->second, pos)} };
      return (res);
      }
    case o_non:
      return rewriteDNF(f->arg, c, !pos);
      break;
    case o_et: {
      cnf_t c1 = rewriteCNF(f->arg1, c, pos);
      cnf_t c2 = rewriteCNF(f->arg2, c, pos);
      return cnf_union(c1, c2);
      }
    case o_ou: {
      cnf_t c1 = rewriteCNF(f->arg1, c, pos);
      cnf_t c2 = rewriteCNF(f->arg2, c, pos);
      return cnf_product(c1, c2);
      } 
    case o_implique: {
      cnf_t c1 = rewriteDNF(f->arg1, c, !pos);
      cnf_t c2 = rewriteCNF(f->arg2, c, pos);
      return cnf_product(c1, c2);
    }
    case o_equivaut: {
      cnf_t c1a = rewriteDNF(f->arg1, c, !pos);
      cnf_t c2a = rewriteCNF(f->arg2, c, pos);
      cnf_t ca = cnf_product(c1a, c2a);
      cnf_t c1b = rewriteCNF(f->arg1, c, !pos);
      cnf_t c2b = rewriteDNF(f->arg2, c, pos);
      cnf_t cb = cnf_product(c1b, c2b);
      return cnf_union(ca, cb);
      }
    }
}
 
 
cnf_t rewriteDNF(formule f, const map<string,var_t> & c, bool pos) {
  cnf_t res;
  switch (f->op) {
    case o_variable:{
      res = { {var2lit(c.find(* (f->nom))->second, pos)} };
      return (res);
      }
    case o_non:
      return rewriteCNF(f->arg, c, !pos);
      break;
    case o_et: {
      cnf_t c1 = rewriteDNF(f->arg1, c, pos);
      cnf_t c2 = rewriteDNF(f->arg2, c, pos);
      return cnf_product(c1, c2);
      }
    case o_ou: {
      cnf_t c1 = rewriteDNF(f->arg1, c, pos);
      cnf_t c2 = rewriteDNF(f->arg2, c, pos);
      return cnf_union(c1, c2);
      } 
    case o_implique: {
      cnf_t c1 = rewriteCNF(f->arg1, c, !pos);
      cnf_t c2 = rewriteDNF(f->arg2, c, pos);
      return cnf_union(c1, c2);
    }
    case o_equivaut: {
      cnf_t c1a = rewriteCNF(f->arg1, c, !pos);
      cnf_t c2a = rewriteDNF(f->arg2, c, pos);
      cnf_t ca = cnf_union(c1a, c2a);
      cnf_t c1b = rewriteDNF(f->arg1, c, !pos);
      cnf_t c2b = rewriteCNF(f->arg2, c, pos);
      cnf_t cb = cnf_union(c1b, c2b);
      return cnf_product(ca, cb);
      }
    }
}

Il faut également remplacer main.cpp par la version suivante: main.cpp.

Ajouter la ligne suivante après les #include dans le fichier formule.hpp:

#include <algorithm> 

Enfin il faut ajouter la ligne suivante après la déclaration de writeDimacs dans formule.hpp:

// fonction de transformation en CNF, version equivalente exponentielle ////////
cnf_t rewriteCNF(formule f, const map<string,var_t> & corresp, bool pos=true);

Il est ensuite possible d'appeler ./verifier --no-tseitin --use-minisat pour tester la validiter d'une formule, ou ./verifier --check-adder --no-tseitin --use-minisat pour vérifier un additionneur.

<note important>Il y a un bug dans la fonction writeDimacs (dans formule.cpp): il faut remplacer la ligne

      out << ( (positif(l)?1:-1) * lit2var(l) ) << " ";

par la ligne

      out << ( (positif(l)?1:-1) * (1+lit2var(l)) ) << " ";

</note>

<note tip>Le projet de base sur la forge et l'archive inf3034l-2015-base.zip ont été mis à jour en intégrant ces modifications</note>

La transformation de Tseitin (c.f. TD du 19/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);
void tseitin(formule f, const map<string, var_t> & m, cnf_t & c);

<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), m, cl, 3)
    • tseitin(a, m, cl, 3) 0 est le lit positif correspondant à a, on ajoute rien à cl
    • tseitin(b, m, 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). Au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 4.
  • tseitin(c, m, 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 littéral positif qui code f (au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 5, mais comme on ne tirera plus de variable fraîche par la suite, cela ne se voit pas)

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 void tseitin(formule f, map<string, int>&, cnf_t&) qui appelle 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.

<note tip>Si le programme minisat est disponible en ligne de commande sur votre machine, vous pouvez dès à présent tester votre approche en utilisant l'argument --use-minisat. Le programme appellera minisat pour tester la (non-)satisfiabilité de la formule de vérification</note>

Une fois la CNF obtenue, il est possible d'utiliser la méthode de résolution pour tester son insatisfiabilité. Cette méthode consiste à combiner des clauses entre elles pour essayer de déduire la clause vide. La clause obtenue par combinaison de deux clauses est appelée résolvante

Le calcul des résolvante est la première brique réellement liée à la résolution proprement dite. Le calcul des résolvantes est effectué ainsi :

• Une première fonction pivot, étant données deux clauses cl1 et cl2, trouve un littéral l de cl1 tel que ¬l est présent dans cl2. Cette fonction prend les deux clauses en paramètre, ainsi qu'un paramètre l_pivot qui est un littéral passé par référence. Si l existe, la fonction reverra true et affectera l_pivot à l. Sinon la fonction renvoie simplement false. On codera de préférence cette fonction avec un algorithme linéaire dans la taille des clauses, en s'appuyant sur les remarques suivantes:
  • les représentations des littéraux sont triées dans les clauses¹¹⁾
  • si n représente un littéral l, alors ¬l est représenté par n+1 ou n-1.
• Une seconde fonction resolvante, étant données deux clauses et un littéral dans la première clause, calcule la clause qui est la résolvante des deux premières.

bool pivot(cls_t c1, cls_t c2, lit_t & l_pivot);
cls_t resolvante(cls_t c1, cls_t c2, lit_t l_pivot);

• Écrire la fonction pivot.
• Écrire la fonction resolvante.
• Écrire les tests unitaires pour ces fonctions.

Implémenter l'algorithme de recherche d'un arbre de résolution par ajout de clauses dans une CNF (voir cours/TD). On utilisera par exemple une pile avec un vector<clause> sous-jacent pour stocker les clauses à traiter. Ce vecteur sera initialisé avec les clauses contenues dans la CNF résultant de la traduction de la formule de départ via la transformation de Tseitin. Ensuite on répète tant que possible la recherche, le calcul et l'ajout de résolvante. L'algorithme en pseudo-code est le suivant :

Entrée : cnf l'ensemble initial de clauses, que l'on complète au fur et à mesure;
Variable locale : q la pile des clauses restant à traiter, quand elle est vide on a saturé l'espace de recherche;
Résultat : true si on peut dériver la clause vide, false sinon;
Algorithme :

• ∀ cl ∈ cnf
  • q.push( cl )
• cnf = ∅
• tant que (¬q.empty( ))
  • cl = q.pop( )
  • si (cl≡⊥)
    • renvoyer true
  • si (cl ≢⊤ et cl ∉ cnf)
    • ∀ cl2 ∈ cnf
      • cl_r = resolvante(cl, cl2)
      • q.push( cl_r )
    • cnf.push( cl )
• fin tant que
• renvoyer false

Le prototype formel C++ attendu est le suivant :

bool unsat(cnf_t f);

• Écrire la fonction tautologie qui vérifie si une clause est valide (auquel cas il est n'est pas intéressant de l'ajouter à la CNF)
• Écrire la fonction directement_impliquee_par qui vérifie si une clause est dans la CNF. Une version plus optimisée (voir partie 4) consistera à vérifier si la clause ne contient pas une clause présente dans la CNF. Si une clause est directement impliquée par la CNF, il est inutile de la traiter.

<note important>La signature de cette fonction doit comporter des références (&), contrairement au fichier resolution.cpp fourni à l'origine:

bool directement_impliquee_par(cls_t & c, cnf_t & f);

</note>

• Écrire la fonction unsat.
• Écrire les tests unitaires vérifiant le bon comportement de la fonction unsat.

<note tip>Une clause est équivalente à ⊤ si elle contient un littéral et sa négation. D'après la manière dont son codés les littéraux et les clauses, si p et ¬p sont dans une clause, ils se suivent lorsqu'on parcourt la clause. On peut ainsi détecter les clauses équivalentes à ⊤ via un simple parcours de la clause en comparant le littéral courant à la négation de celui qui vient d'être lu.</note> <note important> A la fin de cette partie, le projet dispose de toutes les fonctionnalités pour vérifier l'insatisfiabilité (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 unsat et de simplification que l'on peut apporter lors du calcul des résolvantes, pour éviter d'en introduire des inutiles. C'est l'objet de la quatrième partie du projet. </note>

L'objectif de cette partie est de rendre plus efficace le solveur résolution naïf, en utilisant les optimisations suivantes:

• indexation des clauses
• suppression des clauses contenant au moins une autre clause présente dans la CNF
• heuristique de choix de clause

Afin de pouvoir enrichir facilement les structures de données des CNFs, on en fait un type abstrait, c'est à dire que l'on ajoute les fonctions suivantes, qui devront remplacer les utilisations des fonctions/méthodes correspondantes la classe cnf_t (qui était jusqu'ici un vector<cls_t>).

struct cnf_t {
  vector<cls_t> _clauses;
};
vector<cls_t>::const_iterator cbegin(const cnf_t& c);
vector<cls_t>::const_iterator cend(const cnf_t& c);
cnf_t cnf(vector<cls_t> cls);
void add(cnf_t & cnf, cls_t cls);
unsigned int size(const cnf_t & cnf);

1. Effectuer les changements indiqués ci-dessus dans formule.hpp (replacement du type cnf_t et fonctions additionnelles). Implémenter ces fonctions additionnelles dans formule.cpp.
2. Remplacer les appels xxx.cbegin(), xxx.cend(), etc, par des appels appropriés à ces fonctions.

On souhaite à présent construire un index afin de trouver directement les clauses avec lesquelles on peut trouver une résolvante pour une clause c donnée. Cet index va indiquer pour chaque littéral quelles sont les clauses qui le contiennent. Pour faciliter la gestion mémoire, on numérote les clauses en utilisant l'indice auquel elles apparaissent dans le vecteur _clauses. L'index stockera ainsi pour chaque littéral une liste des numéros des clauses qui le contiennent:

struct cnf_t {
  vector<cls_t> _clauses;
  vector<vector<unsigned int> > _index;
}

1. Modifier la structure de CNF conformément au code ci-dessus. Mettre à jour les fonctions add(…) et cnf(…) pour créer et maintenir cet index.
2. Implementer resolvantes, qui utilise l'index pour calculer toutes les résolvantes d'une clause cls avec les clauses d'une CNF cnf:

   vector<cls_t> resolvantes(const cls_t & cls, const cnf_t & cnf);

3. Modifier unsat pour utiliser resolvantes au lieu de pivot et resolvante.

On peut remarquer que si une clause c est présente dans la CNF, il est inutile de traiter des clauses qui contiennent c. On souhaite utiliser cette remarque pour éviter d'ajouter de telles clauses.

1. Modifier directement_impliquee_par(...) pour tester non si la clause appartient à la CNF, mais si une clause de la CNF est contenue dans la clause testée. On pourra pour cela implémenter la fonction suivante (à déclarer dans formule.hpp et à coder dans formule.cpp):

bool contient(const cls_t & c1, const cls_t & c2);

On peut remarquer que les clauses contenues dans la clause c que l'on veut tester possèdent tous leur littéraux en commun avec c. En particulier, leur premier littéral est dans c.

Créer un deuxième index pour stocker pour chaque littéral l les (numéro des) clauses c telles l est le plus petit littéral dans c:

struct cnf_t {
  vector<cls_t> _clauses;
  vector<vector<unsigned int> > _index;
  vector<vector<unsigned int> > _index2;
};

1. Modifier la structure cnf_t ainsi que les fonctions cnf(...) et add(...) pour refléter ce changement.
2. Utiliser ensuite cet index dans directement_impliquee_par(...) pour ne parcourir que les clauses dont le premier littéral apparaît dans la clause à tester.

On peut remarquer que combiner de petites clauses pour obtenir de nouvelles résolvantes a plus de chances de mener à la clause vide. On souhaite donc changer l'ordre de la file de traitement des clauses en donnant la priorité aux clauses plus petites. Pour cela on va utiliser le conteneur priority_queue de la STL. Ce conteneur nécessite une fonction de comparaison permettant de savoir si une clause est plus prioritaire qu'une autre.

1. Implémenter la fonction suivante qui renvoie true si c1 est moins prioritaire que c2 (i.e. c1 est plus grande en taille que c2):

   bool moins_prioritaire(const cls_t & c1, const cls_t & c2)

   Remarque: priority_queue utilise un ordre total et strict. Il faut donc:

   • avoir un deuxième critère de comparaison si les clauses ont la même taille (par exemple comparer le numéro du plus petit littéral qui n'est pas commun aux deux clauses)
   • renvoyer false si c1 et c2 sont les mêmes clauses
2. Ajouter le code suivant avant la fonction unsat:

   class compare_clauses {
   public:
     bool operator() (const cls_t & c1, const cls_t & c2) {
       return moins_prioritaire(c1,c2);
     }
   };

   changer ensuite la déclaration de la file de traitement dans unsat par

   priority_queue<cls_t, vector<cls_t>, compare_clauses >

   Il pourra être nécessaire de changer quelques appels de fonction, l'API de priority_queue étant légèrement différente de celle de vector.