Jaffuel—Simonin Aurore MP2I
TP 22/ Devoir Maison
1 ) ETUDE THEORIQUE
1) On peut mettre une formule sous une forme FNC équisatisfiable via la transformation de Tseitin
avec une complexité linéaire en la taille de la formule, ce qui n’impactera pas la complexité globale.
2) Cela est sémantiquement équivalent à un faux (neutre pour ou). En effet, rajouter un élément
faux dans une disjonction ne change pas la table de vérité de la disjonction.
3) Cela est sémantiquement équivalent à un vrai (neutre pour et). En effet, rajouter un élément vrai
dans une conjonction ne change pas la table de vérité de la conjonction.
4) On a alors v(l)=V.
5) φ=cu^c1^c2 ^...^cn où cu est la clause unitaire.
Soit φ satisfiable. Alors il existe v telle que v(φ)=V, v(l)=V. On a v(¬l)=F.
On retire ¬l : cu = ¬l est impossible car l’on aurait v(φ)=F.
Soit ci contenant ¬l. ci n’est pas une clause unitaire et est une clause disjonctive donc ci = ¬l ou c.
v(¬l)=F fait que v(ci) = v(c) car faux est le neutre pour le ou. Donc v(ci) est inchangée donc par
extension v( φ’)=V encore. (avec φ’ la formule ainsi formée).
Retirer toutes les clauses contenant l retire des sous-clauses disjonctives qui auraient été vraies car
v(l)=V donc retirer ces clauses dans une FNC ne change pas le fait que v(φ)=V. (car T est le neutre
pour et). Donc v(pu(φ,l)) = V. pu(φ,l) est satisfiable.
Réciproque : Soit pu(φ,l) satisfiable. Il existe v telle que v(pu(φ,l))=V.
On construit une valuation v’ telle que v’(x) = v(x) pour x!=l et v’(l)=V.
On construit φ’ en ajoutant des clauses disjonctives ci contenant l. On a alors v’(ci) = V et donc
v’(φ’) = V. Par ailleurs v(¬l)=F donc rajouter des ¬l dans des clauses disjonctives ne changera pas la
la valuation de φ’’ ainsi formée v’(φ’’) = V=v’(φ).
Donc φ est satisfiable.
6) Si φ est satisfiable, alors il existe une valuation v telle que v(φ)=V donc v(l)=V. On construit
elim(φ,l) en éliminant toutes les clauses dans lesquelles l apparaît. Chacune de ces clauses est une
clause disjonctive car φ est sous FNC donc chacune de ces clauses est vraie. Les retirer de la
conjonction qu’est φ n’aura donc aucun impact sur la valuation v et on aura v(elim(φ,l))=V.
elim(φ,l) est satisfiable.
Réciproque : Si elim(φ,l) est satisfiable alors il existe une valuation v telle que v(elim(φ,l))=V. On
considère une valuation v’ telle que v’(x)=v(x) pour x!=l et v’(l)=V.
On construit φ en ajoutant des clauses dans lesquelles l apparaît. Chacune de ces clauses est une
clause disjonctive car φ est sous FNC donc chacune de ces clauses ci vérifie v’(ci)=V. Les rajouter
dans la conjonction qu’est φ n’aura donc aucun impact sur la valuation v’ et on aura v’(φ)=V. φ est
satisfiable.
7) La transformation pu(φ ,l) revient à attribuer une valeur vraie à l. De façon symétrique, on peut
imaginer la transformation pu(φ ,¬l).
Soit φ = c1^c2^...^cn
Si φ est satisfiable alors il existe une valuation v telle que v(φ)=V.
Alors, pour k allant de 1 à n, v(ck) = Vrai car φ est sous FNC.
pu(φ^x,x) = c’1^c’2^...^c’p^x où les clauses c’i avec i de 1 à p sont les clauses de φ ne contenant
pas x auxquelles on a enlevé les occurrences de ¬ x.
Si x = T, alors pu(φ^x,x) = c’1^c’2^...^c’p.
Chaque clause c’i est une clause ck de φ auquelle a été éventuellement enlevée les occurrences de ¬
x. Or v(¬ x)=F donc si v(ck)=V, c étant une clause disjonctive dont faux est le neutre alors v(c’i)=V.
D’où v(pu(φ^x,x))=V.
Donc pu(φ^x,x) est satisfiable.
Si x = ﬩, en posant y = ¬ x on a le même raisonnement et on a pu(φ^¬ x,¬ x) est satisfiable.
On a bien φ est satisfiable implique pu(φ^x,x) est satisfiable ou pu(φ^¬ x,¬ x) est satisfiable.
Réciproquement :
Si pu(φ^x,x) est satisfiable : il existe une valuation v telle que :
v(pu(φ^x,x))=V.
pu(φ^x,x) = c’1^c’2^...^c’p^x où les clauses c’i avec i de 1 à p sont les clauses de φ ne contenant
pas x auxquelles on a enlevé les occurrences de ¬ x.
v(pu(φ^x,x))=V=> Pour tout i de 1 à p, v(c’i)=V et v(x)=V.
On rajoute des clauses c’’j (avec j allant de 1 à r) pour ravoir les clauses originales de φ contenant x
(sans les négations de x pour l’instant). Or ces clauses sont vraies car v(x)=V donc la formule ainsi
construite donne :
v( c’1^c’2^...^c’p^c’’1^...^c’’r)= V.
Rajouter à ces clauses des ¬ x pour retrouver φ ne changera pas leur caractère vrai car ce sont des
clauses disjonctives.
On aboutit à v(φ)=V donc φ est satisfiable.
On peut poser y = ¬ x. Le raisonnement est identique sur y. On aboutit à v(φ)=V.
Voici le détail :
Si pu(φ^ ¬ x, ¬ x) est satisfiable : il existe une valuation v telle que :
v(pu(φ^ ¬ x,¬ x))=V.
pu(φ^¬ x, ¬ x) = c’1^c’2^...^c’p^ ¬ x où les clauses c’i avec i de 1 à p sont les clauses de φ ne
contenant pas x auxquelles on a enlevé les occurrences de x.
v(pu(φ^x,x))=V=> Pourtout i de 1 à p, v(c’i)=V et v(¬ x)=V. Donc v(x) = V.
On rajoute des clauses c’’j (avec j allant de 1 à r) pour ravoir les clauses originales de φ contenant ¬
x (sans les x pour l’instant). Or ces clauses sont vraies car v(¬ x)=V donc la formule ainsi construite
donne :
v( c’1^c’2^...^c’p^c’’1^...^c’’r)= V.
Rajouter à ces clauses des x pour retrouver φ ne changera pas leur caractère vrai car ce sont des
clauses disjonctives.
On aboutit à v(φ)=V donc φ est satisfiable.
On a bien pu(φ^x,x) est satisfiable ou pu(φ^ ¬ x, ¬ x) est satisfiable => φ est satisfiable.
On a prouvé la double implication donc on a bien l’équivalence.
8) Algorithme 1 : DPLL
Entrées : Une formule φ sous FNC.
Sortie : Vrai ssi φ est satisfiable.
Si φ ne contient aucune clause alors
return True
Sinon si φ contient une clause vide alors
return False
Sinon si φ contient une clause unitaire l alors
return dpll (pu(φ,l))
Si φ contient un littéral pur l alors
return dpll (elim( φ,l))
Sinon
φ contient au moins une variable x
return dpll (pu( φ^x, x)) ou dpll(pu(φ^ ¬ x, ¬ x))
Fin
9) Cas de base 1 et 2 : Immédiat pour φ contenant aucune clause ou pour une clause vide : Retour
du résultat.
Dans les autres cas, à chaque appel récursif une variable est éliminée, donc on finit forcément par
ne plus avoir de variables et arriver à un cas de base : l’algorithme termine bien. (On peut
considérer le nombre de variables comme un variant récursif).
10) C’est un algorithme de backtracking car on explore ici l’arbre des possibilités : en notant x la
première variable, on essaye d’abord avec x vrai, en explorant récursivement et en faisant de même
avec les autres variables, et si cela n’aboutit pas on essaye avec x faux.
PARTIE 3.1 CHOIX DE L’HEURISTIQUE
19) Heuristiques :
1) Pour chaque variable xi, calculer Q(xi) = |nb_occ (xi) – nb_occ(neg(xi))|.
Pour que le choix d’une variable ait beaucoup d’influence sur la valuation, il faut qu’elle soit très
présente et que sa négation le soit le moins possible.
Car si la négation est aussi très présente, cela augmente les chances d’avoir la situation où x et ¬ x
sont dans une même clause (disjonctive) : un des deux est forcément à vrai donc la clause est vraie
quelle que soit la valuation de x.
On peut donc calculer Q(xi) pour chaque variable xi et ¬(xi) et prendre celle qui maximise le
résultat.
2) Pour chaque chaque clause contenant la variable x, regarder le nombre de variables n_var autres
que x. Chaque clause étant disjonctive, plus n_var est grand, plus il y a de chances qu’au moins une
variable soit vraie et que la clause soit vraie. Donc il est préférable de choisir une variable x telle
que les n_var pour chaque clause soient faibles.
Par exemple, avec
φ = (x ou y ou (¬ z) ) et (¬ x ou ¬ t ) et (t ou z).
Choisir y = T simplifie φ en :
φ = T et (¬ x ou ¬ t ) et z = (¬ x ou ¬ t ) et z
En estimant que chaque variable a 50 % de chances d’être vraie, pour avoir φ vraie il faut
- z vraie (50%)
- x faux (50%) ou t faux (50 %)
Soit une espérance de 0,5 x (0,5 + 0,5) = 0,5 d’être vraie.
Alors que choisir ¬ t = true (choix privilégié par cette heuristique) permet de simplifier φ en :
φ = (x ou y ou (¬ z) ) et (¬ x) et T = (x ou y ou (¬ z) ) et (¬ x)
En estimant que chaque variable a 50 % de chances d’être vraie, pour avoir φ vraie il faut
- ¬ x vraie (50%)
- x ou y ou (¬ z) (50 % chacune)
Soit une espérance de 0,5 x (0,5 +0,5+ 0,5) = 0,75 d’être vraie, ce qui est meilleur.
4) HORN-SAT
21) Chaque clause de φ n’étant pas unitaire, chaque clause contient au moins deux littéraux. Au plus
un de ces littéraux est un littéral positif, donc chaque clause contient au moins un littéral négatif.
Pour que φ, qui est la conjonction de ces clauses, soit satisfaite, on peut prendre la valuation qui à
chaque variable associe faux : toutes leurs négations seront alors vraies donc toutes les clauses de φ
seront vraies, donc φ sera vraie.
22) Algorithme 1 V2 (Horn-Sat) :
Remarque : A chaque appel récursif, on ne fait que supprimer des clauses ou des littéraux de
certaines clauses donc la condition chaque clause contient au plus un littéral positif reste vraie : On
garde une instance de Horn, donc le dernier cas où il n’y a pas de clause unitaire est trivial d’après
la question précédente : la formule est satisfiable. De plus, la taille de φ diminue ainsi à chaque
appel.
Entrées : Une instance φ de Horn.
Sortie : Vrai ssi φ est satisfiable.
Si φ ne contient aucune clause alors
return True
Sinon si φ contient une clause vide alors
return False
Sinon si φ contient une clause unitaire l alors
return dpll (pu(φ,l))
Sinon
Return True (D’après la question 21)
Complexité :
(a) Les calculs hors appels récursifs sont (pour un appel):
Des tests en parcourant φ (Complexité linéaire en la taille de φ) :
Si φ ne contient aucune clause alors
Si φ contient une clause vide alors
Si φ contient une clause unitaire l alors
Si φ contient un littéral pur
φ contient au moins une variable x
Retours en complexité constante :
return true
return false
Appel à pu(φ,l) : Appels à contient_l ou supprime de complexités O(taille clause) récursivement sur
les clauses de φ donc complexité globale O(taille φ).
Soit au total une complexité hors appels récursifs en O(taille φ).
(b) Nombre d’appels récursifs :
A chaque appel récursif, on diminue de 1 le nombre de variables propositionnelles, donc le nombre
d’appels est en O(taille φ).
Soit une complexité totale en O((taille φ)2), ce qui est polynomial.