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 zip1) contenant:
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.gz2) contenant:
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 18 décembre 2015 à 23h59 dimanche 20 décembre 2015 à 23h594). Il fortement recommandé de tester l'accès à la zone de dépôt avant la date butoir5).
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 :
/Lisez-moi.txt
qui décrit le contenu de l'archive;/unittest-cpp
qui est une bibliothèque pour simplifier l'écriture des tests. Vous n'avez pas à vous intéresser à son contenu;/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.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 fourni6) peut être poussé vers cette forge.
</note>
Le projet est divisé en quatre grandes étapes qui correspondent grossièrement aux 4 séances de TP prévues :
numerote
sont conceptuellement simples mais demandent un réel travail d'immersion et de prise en main du projet.<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 :
</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
.
TEST(lit_ecrit_formule)
.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;
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()
.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.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.TEST
avec les vérifications suivantes :CHECK(cl1 != cl2);
CHECK(cl2 != cl1);
CHECK(cl1 == cl1);
CHECK(cl2 == cl2);
true
.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
.TEST
pour l'affichage d'une CNF c
contenant les clauses cl1
et cl2
.bool est_dans(const cls_t& cl, const cnf_t& c)
permettant de tester l'appartenance d'une clause à une CNF.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îne10).
L'algorithme de numerote
est le suivant :
corresp
comme numéro) et ajouter la correspondance entre le nom de la variable et ce numéro dans corresp
;Pour l'efficacité, on représentera également les littéraux (c'est-à-dire des variables avec ou sans négation) par des entiers :
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.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.
string formule2string(formule f)
de transformation des formules en chaînes de caractères.void numerote(formule f, map<string,var_t> & m)
. On inspirera pour cela de formule2string
ainsi que de l'exemple d'utilisation de map.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.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.var_t lit2var(lit_t l)
qui prend un littéral en argument et retourne sa variable.bool positif(lit_t l)
qui renvoie true
si le littéral passé en argument est un littéral positif.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>
.
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 :
La génération de cette spécification par récurrence pour n-bits peut être définie comme suit:
applique
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);
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:
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 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 à cltseitin(b, m, cl, 3)
2 est le lit positif correspondant à b, on ajoute rien à clcl = 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 à clcl = 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>
lit_t tseitin(formule, map<string, int>&, cnf_t&, var_t&)
telle que décrite.switch (f→op)
de la fonction précédente.void tseitin(formule f, map<string, int>&, cnf_t&)
qui appelle l'autre fonction tseitin
.
<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 :
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: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);
pivot
.resolvante
.
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 :
Le prototype formel C++ attendu est le suivant :
bool unsat(cnf_t f);
tautologie
qui vérifie si une clause est valide (auquel cas il est n'est pas intéressant de l'ajouter à la CNF)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>
unsat
.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:
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);
formule.hpp
(replacement du type cnf_t
et fonctions additionnelles). Implémenter ces fonctions additionnelles dans formule.cpp
.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; }
add(…)
et cnf(…)
pour créer et maintenir cet index.cls
avec les clauses d'une CNF cnf
:vector<cls_t> resolvantes(const cls_t & cls, const cnf_t & cnf);
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.
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; };
cnf_t
ainsi que les fonctions cnf(...)
et add(...)
pour refléter ce changement.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.
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:
false
si c1 et c2 sont les mêmes clausesunsat
: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
.
hg pull https://forge.univ-lyon1.fr/hg/inf3034l-2015-base
CHECK
, on fera une simple vérification visuelle.cl1 = { 7, 6, 1, 4, 1};
.