Table des matières

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 (¬p ∨ p1 ∨ … ∨ px) et (p ∨ q1 ∨ … ∨ qy) on déduit (p1 ∨ … ∨ px ∨ q1 ∨ … ∨ qy). On effectue cette déduction tant que possible jusqu'à :

Modalités de rendu

Le rendu consistera en une archive .zip ou .tar.gz1) contenant:

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 :

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.

<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. 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. </note>

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

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;

Exercices sur les clauses

Exercices sur CNF

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 :

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

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

Exercices sur les littéraux

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

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:

La CNF équisatifiable finale est obtenue comme suit:

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);

<note>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.</note>

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

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>

Exercices

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 : 

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

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 :

Le prototype formel C++ attendu est le suivant : 

bool resolution(const cnf_t& cls);

Exercices

<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 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. </note>

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

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 :

Exercices

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

Références

Mise à jour du projet

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