Projet de logique

Année 2012-2013

Introduction

Les 4 séances de TP de logique visent à implémenter un programme testant la satisfiabilité d'une formule mise sous forme normale conjonctive, c'est-à-dire sous la forme d'un ensemble de clauses. La méthode utilisée par ce programme est le principe de résolution (voir Mémo 4) qui consiste à combiner des paires de clauses, l'une contenant un littéral et l'autre sa négation, pour en produire une nouvelle. Ainsi de (¬pp1 ∨ … ∨ px) et (pq1 ∨ … ∨ qy) on déduit (p1 ∨ … ∨ pxq1 ∨ … ∨ qy). On effectue cette déduction tant que possible jusqu'à :

  • soit l'obtention de la clause vide et on conclue que l'ensemble initial de clauses est insatisfiable;
  • soit l'impossibilité de déduire de nouvelles clauses et on conclue que l'ensemble initial de clauses est satisfiable;

Modalités de rendu

Le rendu consistera en une archive .zip ou .tar.gz1) 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 pts2), 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 vendredi 11 janvier 2013 à 23h593). Il fortement recommandé de tester l'accès à la zone de dépôt avant la date butoir4).

La zone de dépôt est accessible ici: http://spiralconnect.univ-lyon1.fr/spiral/spiral.html#/activities/goto_folder/1992964

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

Projet de départ

L'archive lif11-2012-enonce.zip (v1.1) 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/resolution.hpp et /src/resolution.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).

Organisation du projet

Le projet est divisé en trois 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 la résolution. La résolution travaillant sur des clauses, il faut tout d'abord récursivement convertir une formule arbitraire en forme normale conjonctive. Une version naïve de la méthode de résolution est ensuite à réaliser
  3. Troisième partie : optimisations. Il s'agit d'améliorer les performances de la résolution en ajoutant des stratégies et des index permettant de produire les résolvantes plus efficacement.

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. Le projet est à rendre après les vacances de Noël sous la forme d'une archive comme celle qui vous est fournie. Les modalités exactes du rendu seront données en temps utile.

Première partie : prise en main

Pour de l'aide sur les rudiments du C++ voir l'introduction au C++ et le code d'exemple.

Tests unitaires avec UnitTest++

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.

Exercices

  • 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.

Forme normale conjonctive

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.

Exercices sur les clauses

  • 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 TEST5) qui crée une clause cl1 contenant les littéraux 1, 4, 7 et 66) 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.

Exercices sur CNF

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

Arbre de syntaxe abstraite et litéraux

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îne7). 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.

Exercices sur les map

  • 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.

Exercices sur les littéraux

  • É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.
  • Tester ces fonctions avec UnitTest++.

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é.

Deuxième partie : bases de la résolution

Conversion d'une formule en CNF

La transformation de Tseitin (c.f. CM du 23/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 frâiches. Ainsi en C/C++ on définira les deux fonctions :

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

Une erreur s'était glissée dans la définition précédente : il faut bien lire … ∧ c1 ∧ c2 pour les clauses produites et non … ∧ p1 ∧ p2 comme indiqué avant la correction.

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.

Exercices

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

Calcul de résolvantes

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. On traite le cas où un tel littéral n'existe pas en renvoyant -18). 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 clauses9)
    • 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.
lit_t pivot(const cls_t& cl1, const cls_t& cl2);
cls_t resolvante(const cls_t& cl1, lit_t l, const cls_t& cl2);

Exercices

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

Méthode de résolution par ajout de clauses à une CNF

Implémenter l'algorithme de recherche d'un arbre de résolution par ajout de clauses dans une CNF (voir 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 resolution(const cnf_t& cls);

Exercices

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

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.

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 resolution 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 troisième partie du projet.

Troisième partie: optimisations

Priorité aux petites clauses

Les résolvantes avec des petites clauses sont celles qui ont le plus de chances de:

  1. générer la clause vide
  2. générer une clause qui subsume des clauses existantes.

Pour cela, on utilise une file de priorité pour stocker les clauses à traiter afin de considérer les petites clauses en premier. La classe priority_queue de la STL est très semblable à la classe queue, la différence essentielle est qu'elle est paramétrée par la classe de comparaison qui permet de trier les objets stockés selon leur priorité. La déclaration de la classe de comparaison est un peu particulière : c'est un foncteur (objet-fonction, functor pour function-object en anglais). En pratique c'est une classe pour laquelle on définit operator() et qui s'utilise comme une fonction. Dans l'exemple suivant, on déclare une première file q qui classe les entiers selon l'ordre par défaut (à savoir, l'ordre naturel 0 < 1 < 2 < 3 …) et une suivante pq qui utilise un ordre personnalisé mycomp où les entier impairs sont triés en premiers 1 < 3 < 5 < … < 0 < 2 < 4 …

#include <iostream>
#include <queue>
using namespace std;
 
struct mycomp {
  inline bool operator() (const size_t& lhs, const size_t& rhs) const{
    if (lhs%2 != rhs%2)
      return (lhs%2==1);
    else
      return (lhs<rhs);
  }
};
 
int main (int argc, char* argv[]){
  priority_queue<size_t, vector<size_t>> q;               //ordre par défaut 
  priority_queue<size_t, vector<size_t>, mycomp> pq;      //ordre personnalisé
 
  for(size_t i = 5; i < 10; ++i){
    q.push(i); pq.push(i);
  }
  for(size_t i = 0; i < 5; ++i){
    q.push(i); pq.push(i);
  }  
 
  size_t x,y;
  while(!q.empty()){
    x = q.top(); y = pq.top();
    cout << "x = " << x << ", y = " << y << endl;  
    q.pop(); pq.pop();
  }
 
  return 0;
}

Exercices

  • Sur le modèle donné, écrire la fonction inline bool operator() (const cls_t& lhs, const cls_t& rhs) const du foncteur de comparaison less_prioritary entre clauses qui classe d'abord les clauses selon la taille;
  • Modifier la fonction resolution précédente pour que la pile q soit désormais une priority_queue utilisant le foncteur less_prioritary précédemment défini;
  • Écrire les tests unitaires vérifiant le bon comportement de la fonction resolution en donnant priorité aux petites clauses.

Subsomption

On peut remarquer que si une clause C1 est incluse dans une clause C, toute résolvante de C avec une autre clause C2 contiendra soit C1, soit la résolvante de C1 et C2. Si C1 est dans la CNF courante, il est inutile de calculer des résolvantes avec C. Il s'agit d'écrire une fonction qui renvoie vrai si cl1 est incluse dans cl2 :

bool subsume(const cls_t& cl1, const cls_t& cl2);

Ensuite, il faut modifier la fonction resolution pour:

  1. Ne pas ajouter à la CNF des clauses qui sont subsumées par (qui contiennent) au moins une clause déjà dans la CNF;
  2. Lors de l'ajout d'une clause dans la CNF, supprimer de la CNF les clauses qui sont subsumées strictement (qui contiennent strictement) la clause ajoutée.

L'algorithme résultant en pseudo-code est le suivant :

Entrée : cnf l'ensemble initial de clauses;
Variable locale : q la pile des clauses restant à traiter;
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 t.q. cl' ⊆ cl)
      • ∀ cl2 ∈ cnf
        • cl_r = resolvante(cl, cl2)
        • q.push( cl_r )
      • ∀ cl3 ∈ cnf
        • si cl ⊆ cl3
          • cnf.erase(cl3)
      • cnf.push( cl )
  • fin tant que
  • renvoyer false

Exercices

  • Écrire la fonction subsume qui teste l'inclusion de clauses.
  • Écrire les tests unitaires vérifiant le bon comportement de la fonction subsume.
  • Copier et renommer la fonction resolution existante puis apporter la première modification indiquée, à savoir le test ∄ p' ∈ cnf. p' ⊆ p.
  • Vérifier la non-régression de votre modification avec les tests unitaires existants.
  • (optionnel) Évaluer la différence de performance entre les deux versions.
  • Copier et renommer la fonction resolution existante puis apporter la seconde modification indiquée, à savoir le test si p' ⊆ p' ' pour chaque p' ' ∈ cnf .
  • Vérifier la non-régression de de votre modification avec les tests unitaires existants.
  • (optionnel) Évaluer la différence de performance entre les trois versions.

Indexation

Créer un index, appelé index multiple, sous la forme d'un tableau dont les indices sont les littéraux de la CNF et les cases contiennent la liste des clauses contenant le littéral concerné. Cet index peut être utilisé pour trouver facilement les clauses avec lesquelles on peut calculer une résolvante.

Un deuxième index, appelé index simple, peut être créé sous la forme d'un tableau dont les indices sont les littéraux de la CNF et les cases contiennent la liste des clauses telles que leur plus petit littéral est l'indice de la case. Cet index peut être utilisé pour restreindre le nombre de clauses à regarder pour en trouver une qui peut subsumer une clause C. En effet, si C' subsume C, alors le premier littéral de C' est un des littéraux de C.

Structure d'index

Plutôt que de stocker les clauses directement dans les index, on stocke l'indice de la clause dans la CNF. Cela permet d'accélérer les opérations de mises à jour des index.

typedef cnf_t::size_type cls_ref_t;
typedef  typedef vector< set<cls_ref_t> > idx_t;

Cela complique en revanche la gestion de la suppression des clauses: en effet, lorsqu'une clause est supprimée dans la cnf, cela invalide les index des clauses suivantes10). On désactivera donc la suppression de clauses. Afin de pouvoir comparer les performances à la fin du projet, on gardera de côté la version sans index mais avec suppression des clauses subsumées.

Exercices

  • Construction et utilisation de l'index simple:
    • Écrire une fonction
      void add_clause(cnf_t & cnf, idx_t & idx_simple, const cls_t & c)

      qui ajoute une clause dans la cnf et rajoute sa référence (i.e. son numéro de case) dans l'ensemble des clauses de son premier littéral dans idx_simple.

    • Désactiver la suppression des clauses dans resolution.
    • Écrire des tests unitaires pour vérifier son bon fonctionnement.
    • Écrire une fonction
      bool est_subsumee(const cnf_t & cnf, const idx_t & idx_simple, const cls_t & c)

      qui vérifie s'il existe dans la CNF une clause qui subsume la clause c.

    • Écrire des tests unitaires pour vérifier son bon fonctionnement.
    • Utiliser est_subsumee dans resolution à la place du premier est d'inclusion (∄ cl' ∈ cnf t.q. cl' ⊆ cl) .
  • Construction de l'index multiple et utilisation pour le calcul du pivot:
    • Modifier la fonction add_clause en ajoutant un paramètre correspondant à l'index multiple:
      void add_clause(cnf_t & cnf, idx_t & idx_simple, idx_t & idx_multiple, const cls_t & c)
    • Écrire des tests unitaires pour vérifier son bon fonctionnement.
    • Utiliser l'index multiple pour trouver les résolvantes à ajouter aux clauses à traiter en utilisant la remarque suivante: une clause C peut être combinée avec une autre clause C' en utilisant un littéral l ∈ C comme pivot si et seulement si C' se trouve référencée dans l'index multiple dans la case du littéral ¬ l
  • Comparer les performance des deux versions du solveur “resolution”:
    • Celle qui supprime les clauses de la CNF qui sont subsumée par la clause qui va être ajoutée
    • Celle qui ne fait pas cette suppression, mais qui utilise les index pour le premier test de subsomption (∄ cl' ∈ cnf t.q. cl' ⊆ cl) et le calcul des résolvantes.

Références

Mise à jour du projet

  • v0, 18/10/12 : version initiale par EC;
  • v1, 21/10/12 : alignement sujet/code et réorganisation par RT;
  • v11, 23/10/12 : suppression des méthodes de cls2string et cnf2string, on se limite à l'opérateur operator« pour cls_t et cnf_t;
  • v12, 20/11/12 : correction mineure Tseitin et exemple afférant;
  • v13, 04/12/12 : ajout du pseudo-code de lalgo de resolution, détails sur les optimisations “priorité aux petites clauses” et “subsomption”;
  • v14, 20/12/12 : ajout de détails concernant l'utilisation des index
1)
pas de rar ou autre format exotique
2)
pas de fichier en police 14 ou 16 pts pour faire du remplissage, cela se voit au premier coup d'oeil
3)
la zone de dépôt sera automatiquement fermée à ce moment
4)
l'excuse “je n'avais pas accès au dépôt” ne sera pas acceptée
5)
Ce test ne contient pas de CHECK, on fera une simple vérification visuelle.
6)
Vous pouvez pour cela utiliser la notation des initializer_list avec par exemple cl1 = { 7, 6, 1, 4, 1};.
7)
C'est ainsi une fonction partielle dont on définit le graphe.
8)
Une autre convention est possible, comme renvoyer une paire ou passer un booléen par référence
9)
i.e. les itérateurs parcourent entier représentant les littéraux dans l'ordre croissant
10)
ou, si on a procédé par échange de la clause à supprimer et de la dernière clause de la cnf por éviter le décalage, cela invalide l'index de la clause échangée