Formules en FNC¶
On considère les types suivants permettant de représenter une formule en forme normale conjonctive (FNC) :
struct litteral {
int ident;
bool negatif;
};
typedef struct litteral litteral;
struct clause {
int nlitteraux;
litteral *litteraux;
};
typedef struct clause clause;
struct formule {
int nclauses;
clause *clauses;
};
typedef struct formule formule;
Un littéral est une variable, d'identifiant ident, éventuellement niée si
negatif vaut true. Une clause est un tableau de nlitteraux littéraux
(leur disjonction) et une formule est un tableau de nclauses clauses (leur
conjonction).
On identifie ainsi l'ensemble des variables \(\mathcal{V}\) à \(\N\), ce qui revient à considérer que les variables se notent \(X_0, X_1, \dots\).
Question 1
Allouez et créez la formule
Corrigé
On alloue la formule, son tableau de clauses, puis le tableau de littéraux de chaque clause. Deux petites fonctions évitent de répéter les mêmes lignes.
// alloue la clause i de f, avec n littéraux (non initialisés)
void alloue_clause(formule *f, int i, int n)
{
f->clauses[i].nlitteraux = n;
f->clauses[i].litteraux = malloc(n * sizeof(litteral));
}
void fixe_litteral(formule *f, int i, int j, int ident, bool negatif)
{
f->clauses[i].litteraux[j].ident = ident;
f->clauses[i].litteraux[j].negatif = negatif;
}
formule *exemple(void)
{
formule *f = malloc(sizeof(formule));
f->nclauses = 3;
f->clauses = malloc(3 * sizeof(clause));
alloue_clause(f, 0, 2); // X0 ∨ ¬X1
fixe_litteral(f, 0, 0, 0, false);
fixe_litteral(f, 0, 1, 1, true);
alloue_clause(f, 1, 3); // X1 ∨ ¬X2 ∨ ¬X0
fixe_litteral(f, 1, 0, 1, false);
fixe_litteral(f, 1, 1, 2, true);
fixe_litteral(f, 1, 2, 0, true);
alloue_clause(f, 2, 1); // ¬X2
fixe_litteral(f, 2, 0, 2, true);
return f;
}
Question 2
Écrire une fonction
void libere_formule(formule *f);
qui libère toute la mémoire d'une formule f (on considère que f
lui-même est un pointeur vers le tas).
Corrigé
void libere_formule(formule *f)
{
for(int i = 0; i < f->nclauses; i++) {
free(f->clauses[i].litteraux);
}
free(f->clauses);
free(f);
}
On libère dans l'ordre inverse des allocations : une fois f->clauses
libéré, on ne peut plus accéder aux tableaux de littéraux.
Question 3
Écrire une fonction
int num_variables(formule *f);
qui renvoie le plus petit entier \(n\) tel que les variables
présentes dans f sont de numéro \(< n\).
Corrigé
int num_variables(formule *f)
{
int n = -1;
for(int i = 0; i < f->nclauses; i++) {
for(int j = 0; j < f->clauses[i].nlitteraux; j++) {
if (f->clauses[i].litteraux[j].ident > n)
n = f->clauses[i].litteraux[j].ident;
}
}
return n+1;
}
On renvoie 0 pour une formule sans variable. Pour l'exemple, on obtient 3.
Question 4
Écrire une fonction
void affiche_formule(formule *f);
qui affiche une formule.
Corrigé
On note ~ la négation, | la disjonction et & la conjonction.
void affiche_formule(formule *f)
{
for(int i = 0; i < f->nclauses; i++) {
if (i > 0)
printf(" & ");
printf("(");
for(int j = 0; j < f->clauses[i].nlitteraux; j++) {
if (j > 0)
printf(" | ");
litteral l = f->clauses[i].litteraux[j];
printf("%sX%d", l.negatif ? "~" : "", l.ident);
}
printf(")");
}
printf("\n");
}
Pour l'exemple, on obtient (X0 | ~X1) & (X1 | ~X2 | ~X0) & (~X2).
Valuation¶
Si on sait que les variables présentes dans f sont
d'indice \(< n\), on peut représenter une valuation pour
f comme un tableau bool *v de taille n tel que
v[i] = true si et seulement si \(v(X_i) = 1\).
Question 5
Écrire des fonctions
bool evalue_litteral(litteral *l, bool *valuation);
bool evalue_clause(clause *c, bool *valuation);
bool evalue(formule *f, bool *valuation);
telles que l'appel à evalue(f, v) renvoie la valeur de \([f]_v\).
Corrigé
bool evalue_litteral(litteral *l, bool *valuation)
{
if (l->negatif)
return !valuation[l->ident];
return valuation[l->ident];
}
bool evalue_clause(clause *c, bool *valuation)
{
bool v = false;
for(int i = 0; i < c->nlitteraux; i++)
v = v || evalue_litteral(&c->litteraux[i], valuation);
return v;
}
bool evalue(formule *f, bool *valuation)
{
bool v = true;
for(int i = 0; i < f->nclauses; i++) {
v = v && evalue_clause(&f->clauses[i], valuation);
}
return v;
}
Conformément aux conventions sur la FNC, une clause vide (disjonction
vide) est fausse et une formule sans clause (conjonction vide) est vraie.
Grâce à l'évaluation paresseuse de || et &&, l'évaluation s'arrête
dès qu'un littéral vrai ou une clause fausse est rencontré.
Énumération¶
Pour énumérer les valuations sur \(n\) variables, on va
identifier un tableau bool *v de taille \(n\) avec
le nombre écrit en binaire \(N(v) = \sum_{i=0}^{n-1} v[i] 2^i\).
Question 6
Écrire une fonction
bool suivante(int n, bool *valuation);
telle que suivante(n, v), où v est un tableau de n valeurs,
place dans v le nombre \(N(v)+1\) et renvoie true si \(N(v) < 2^n-1\). Si
\(N(v) = 2^n-1\), la fonction renvoie false.
Corrigé
On ajoute 1 en binaire : les 1 de poids faible deviennent des 0 et le premier 0 devient un 1. S'il n'y a pas de 0, on était à \(2^n - 1\).
bool suivante(int n, bool *valuation)
{
int j = 0;
while(j < n && valuation[j]) {
j++;
}
if (j == n)
return false;
for(int i = 0; i < j; i++)
valuation[i] = false;
valuation[j] = true;
return true;
}
À partir du tableau v rempli de false (et donc \(N(v) = 0\)) et en utilisant
la fonction précédente, on peut énumérer toutes les valuations facilement.
Par exemple, la table de vérité de la formule f de la question 1 s'obtient
avec :
bool v[3] = { false, false, false };
do {
printf("%d-%d-%d | %d\n", v[0], v[1], v[2], evalue(f, v));
} while(suivante(3, v));
qui affiche les valeurs de \(X_0\), \(X_1\), \(X_2\) puis celle de \(f\) :
0-0-0 | 1
1-0-0 | 1
0-1-0 | 0
1-1-0 | 1
0-0-1 | 0
1-0-1 | 0
0-1-1 | 0
1-1-1 | 0
Question 7
Écrire une fonction
bool tautologie(formule *f);
qui indique si f est une tautologie.
Corrigé
On teste les \(2^n\) valuations, en s'arrêtant à la première qui rend f
fausse. On n'oublie pas de libérer la valuation avant de renvoyer le
résultat.
bool *valuation_nulle(int n)
{
bool *v = malloc(n * sizeof(bool) + 1); // + 1 : évite un malloc(0)
for(int i = 0; i < n; i++)
v[i] = false;
return v;
}
bool tautologie(formule *f)
{
int n = num_variables(f);
bool *v = valuation_nulle(n);
bool resultat = true;
do {
if (!evalue(f, v)) {
resultat = false;
break;
}
} while(suivante(n, v));
free(v);
return resultat;
}
Cette fonction est en \(O(2^n |f|)\) où \(|f|\) est le nombre total de
littéraux de f.
Question 8
Écrire une fonction
bool *satisfiable(formule *f);
qui renvoie une valuation modèle de f si f est satisfiable
et qui renvoie NULL si f n'est pas satisfiable.
Corrigé
bool *satisfiable(formule *f)
{
int n = num_variables(f);
bool *v = valuation_nulle(n);
do {
if (evalue(f, v))
return v;
} while(suivante(n, v));
free(v);
return NULL;
}
La valuation renvoyée est allouée sur le tas : c'est à l'appelant de la libérer. Pour l'exemple, on obtient la valuation nulle.
Question 9
Écrire une fonction
bool consequence(formule *f, formule *g);
qui indique si f est conséquence logique de g.
Corrigé
\(f\) est conséquence logique de \(g\) (\(g \models f\)) si et seulement si tout modèle de \(g\) est un modèle de \(f\). On énumère donc les valuations sur les variables des deux formules, à la recherche d'un contre-exemple.
int max(int a, int b)
{
return a > b ? a : b;
}
bool consequence(formule *f, formule *g)
{
int n = max(num_variables(f), num_variables(g));
bool *v = valuation_nulle(n);
bool resultat = true;
do {
if (evalue(g, v) && !evalue(f, v)) {
resultat = false;
break;
}
} while(suivante(n, v));
free(v);
return resultat;
}
Par exemple, \(\neg X_2\) est conséquence de la formule \(f\) de la question 1, mais pas l'inverse ; et toute formule est conséquence d'une formule insatisfiable comme \(X_0 \wedge \neg X_0\).