X/ENS Informatique A MP 2016

ECOLE POLYTECHNIQUE -- ECOLES NORMALES SUPERIEURES

CONCOURS D'ADMISSION 2016

FILIERES

MP SPECIALITE INFO

COMPOSITION D'INFORMATIQUE ­ A ­ (XULCR)
(Duree : 4 heures)
L'utilisation des calculatrices n'est pas autorisee pour cette epreuve.
Le langage de programmation sera obligatoirement Caml.

Satisfiabilite des formules booleennes
Nous nous interessons ici au probleme bien connu de la satisfiabilite des formules booleennes,
appele SAT dans la litterature. Historiquement, SAT a joue un role preponderant dans le
developpement de la theorie de la complexite. De nos jours il intervient dans de nombreux
domaines de l'informatique ou des problemes combinatoires difficiles apparaissent, comme la
verification formelle, la recherche operationnelle, la bioinformatique, la cryptologie, l'apprentissage automatique, la fouille de donnees, et bien d'autres encore. Signe de son importance, SAT
et ses variantes ont leur propre conference internationale qui se tient tous les ans depuis pres de
20 ans.
Ce sujet se concentre sur une version restreinte de SAT, appelee k-SAT, dans laquelle les
formules booleennes considerees en entree sont en forme normale conjonctive avec au plus k
litteraux par clause. Le but est d'apporter aux candidats les rudiments de l'analyse de la complexite de k-SAT, en proposant des approches efficaces pour des valeurs specifiques de k ainsi
qu'une approche generale pour les valeurs de k arbitraires. Le sujet s'articule donc naturellement
autour des differentes valeurs de k : k = 1 pour la partie I, k = 2 pour la partie II, k  3 pour
la partie III. La partie IV fait le lien avec le probleme SAT lui-meme.

Preliminaires
Cette partie preliminaire introduit formellement les concepts et resultats utiles pour l'analyse.
Par complexite (en temps) d'un algorithme A on entend le nombre d'operations elementaires
(comparaison, addition, soustraction, multiplication, division, affectation, test, etc) necessaires
a l'execution de A dans le cas le pire. Lorsque ce nombre depend d'un ou plusieurs parametres
0 , · · · , r-1 , on dit que A a un temps d'execution en O(f (0 , · · · , r-1 )) s'il existe une constante
C > 0 telle que, pour toutes les valeurs de 0 , · · · , r-1 suffisamment grandes (c'est-a-dire plus
grandes qu'un certain seuil), pour toute instance du probleme de parametres 0 , · · · , r-1 , le
nombre d'operations elementaires est au plus C f (0 , · · · , r-1 ). On dit que la complexite est
lineaire quand f est une fonction lineaire des parametres 0 , · · · , r-1 . De meme, on dit que la
1

complexite est polynomiale quand f est une fonction polynomiale des parametres. Sauf mention
contraire dans l'enonce, le candidat n'aura pas a justifier de la complexite de ses algorithmes.
Toutefois il devra veiller a ce que cette complexite ne depasse pas les bornes prescrites.
Pour la programmation proprement dite, en plus des fonctionnalites de base du langage Caml
le candidat pourra utiliser les fonctions suivantes sans les programmer :
· do list: ('a -> unit) -> 'a list -> unit
do list f [a1; a2; ...; an] equivaut a begin f a1; f a2; ...; f an; () end
· map: ('a -> 'b) -> 'a list -> 'b list
map f [a1; a2; ...; an] renvoie la liste [f a1; f a2; ...; f an]
· it list: ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
it list f a [b1; ...; bn] renvoie la valeur de f (... (f (f a b1) b2) ...)
· list it: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
list it f [a1; ...; an] b renvoie la valeur de f a1 (f a2 (... (f an b) ...))

Formules booleennes. Une variable booleenne est une variable prenant ses valeurs dans l'ensemble {Vrai, Faux}. Une formule booleenne s'obtient en combinant des variables booleennes et
des connecteurs logiques Et (note ), Ou (note ), Non (note ¬), selon la grammaire suivante,
donnee directement dans le langage Caml :
type formule =
|Var of int
|Non of formule
|Et of formule * formule
|Ou of formule * formule;;
Ainsi les formules booleennes sont representees par des structures arborescentes en machine,
appelees arbres d'expression dans la suite. Voir la figure 1 pour un exemple.
Et

Ou

Non

x0

x1

x2

Figure 1 ­ L'arbre d'expression associe a la formule (¬x0 )  (x1  x2 ) de taille 6.
A noter que les variables d'une formule f sont indexees par des entiers, d'ou la ligne
Var of int dans la definition du type formule. Par defaut ces entiers seront supposes positifs
ou nuls, contigus, et commencant par 0. Ainsi, les variables de f seront denotees par exemple
x0 , · · · , xr-1 . La taille de f est le nombre total de variables booleennes et de connecteurs logiques qui la composent. C'est donc le nombre total n de noeuds composant l'arbre d'expression
associe, et on a naturellement r  n.

2

Valuations et equivalence logique. Etant donnees r variables booleennes x0 , · · · , xr-1 ,
une valuation est une application  : {x0 , · · · , xr-1 }  {Vrai, Faux}. Etant donnee une formule f utilisant ces r variables, le resultat de l'evaluation de f sur , note (f ), est obtenu
en affectant la valeur (xi ) a chaque variable xi . Deux formules f et g utilisant les variables
booleennes x0 , · · · , xr-1 sont dites logiquement equivalentes si (f ) = (g) pour toute valuation
 : {x0 , · · · , xr-1 }  {Vrai, Faux}.
Proprietes des connecteurs logiques. Rappelons que le connecteur ¬ est involutif, c'esta-dire que pour toute formule f :
· ¬¬f est logiquement equivalente a f .
Par ailleurs, en plus d'etre commutatifs et associatifs, les connecteurs logiques  et  sont
distributifs, c'est-a-dire que pour toutes formules f , g et h :
· f  (g  h) est logiquement equivalente a (f  g)  (f  h),
· f  (g  h) est logiquement equivalente a (f  g)  (f  h).
Dans ce sujet nous adoptons la convention que le connecteur ¬ est prioritaire sur  et , ce qui
permet par exemple d'ecrire ¬x0  (x1  x2 ) au lieu de (¬x0 )  (x1  x2 ) comme dans la figure 1.
Les lois de De Morgan decrivent la maniere dont  et  interagissent avec ¬. Pour toutes
formules f et g :
· ¬(f  g) est logiquement equivalente a ¬f  ¬g,
· ¬(f  g) est logiquement equivalente a ¬f  ¬g.

Le probleme SAT. Etant donnee une formule f a r variables x0 , · · · , xr-1 , le probleme SAT
consiste a determiner s'il existe une valuation  : {x0 , · · · , xr-1 }  {Vrai, Faux} telle que
(f ) = Vrai. Dans l'affirmative, la formule f est dite satisfiable. Dans la negative, f est dite
insatisfiable. Par exemple, la formule ¬x0  (x1  x2 ) de la figure 1 est satisfiable, tandis que
¬x0  (x1  x2 )  (x0  ¬x1 )  (x0  ¬x2 ) est insatisfiable.
Question 1 Pour chaque formule qui suit, dire si elle est satisfiable ou non, sans justification :
a) x1  (x0  ¬x0 )  ¬x1
b) (x0  ¬x1 )  (¬x0  x2 )  (x1  ¬x2 )
c) x0  ¬(x0  ¬(x1  ¬(x1  ¬x2 )))
d) (x0  x1 )  (¬x0  x1 )  (x0  ¬x1 )  (¬x0  ¬x1 )
Forme normale conjonctive. Dans la suite nous utiliserons essentiellement des formules
ecrites sous la forme suivante, appelee forme normale conjonctive (FNC) :
ni
m _
^

lij ,

(1)

i=1 j=1

ou chaque litteral lij est soit une variable
x, soit sa negation ¬x, et ou les litteraux
W booleenne
i
sont regroupes en clauses disjonctives nj=1
lij . Par exemple, les formules a), b) et d) de la
question 1 sont des FNC.
Une FNC est appelee k-FNC lorsque chaque clause a au plus k litteraux, c'est-a-dire que
ni  k pour tout i  {1, · · · , m} dans l'equation (1). Notez qu'alors la formule est egalement
3

une k -FNC pour tout k  k. Par exemple, les formules a), b) et d) de la question 1 sont des
2-FNC. La variante de SAT appelee k-SAT prend uniquement en entree des formules en k-FNC.
C'est cette variante qui nous interesse dans ce sujet. Elle est equivalente a SAT du point de vue
de la theorie de la complexite quand k  3, comme nous le verrons dans la partie IV.
En machine nous representerons les FNC sous la forme de listes de listes. Plus precisement,
une FNC sera une liste de clauses et chaque clause sera une liste de litteraux :
type litteral =
|V of int (* variable *)
|NV of int;; (* negation de variable *)
type clause == litteral list;;
type fnc == clause list;;
Ainsi, une formule en k-FNC sera representee par une liste (de taille arbitraire) de listes de taille
au plus k chacune.
Question 2 Ecrire une fonction var max qui prend en entree une FNC f et renvoie le plus grand
indice de variable utilise dans la formule. La complexite de la fonction doit etre lineaire en la
taille de f .
var_max: fnc -> int

Partie I. Resolution de 1-SAT
Commencons pas le cas le plus simple, a savoir k = 1. Ici chaque clause de la FNC est
formee d'un unique litteral li et donc impose un unique choix possible d'affectation pour la
variable xi : soit li = xi et dans ce cas xi doit valoir Vrai, soit li = ¬xi et dans ce cas xi doit
valoir Faux. La formule est alors satisfiable si et seulement s'il n'y a pas de contradiction dans
les choix d'affectation de variables imposes par ses differentes clauses. Afin d'effectuer ce test
efficacement, nous allons maintenir un tableau ou chaque case correspondra a une variable de
la formule (de meme indice que la case) et ou les valeurs seront des trileens : vrai, faux, ou
indetermine. Pour cela nous definissons le type trileen ci-dessous :
type trileen =
|Vrai
|Faux
|Indetermine;;
Grace au tableau de trileens, a chaque litteral li rencontre on peut determiner en temps constant
si la variable xi est deja affectee ou non, et dans l'affirmative, si sa valeur d'affectation est
compatible avec celle imposee par li .
Question 3 Ecrire une fonction un sat qui prend en entree une FNC f , supposee etre une
1-FNC, et qui renvoie un booleen valant true si et seulement si f est satisfiable. La complexite
de la fonction doit etre lineaire en la taille de f .
un_sat: fnc -> bool

4

Partie II. Resolution de 2-SAT
Nous venons de voir que 1-SAT est un probleme facile puisque resoluble en temps lineaire.
Nous allons maintenant voir que 2-SAT est egalement lineaire, bien que son traitement efficace
necessite plus de travail d'analyse et de codage. Nous allons en effet montrer comment reduire les
instances de 2-SAT a la recherche de composantes fortement connexes dans un graphe oriente. Ce
dernier probleme a un interet en soi et fait l'objet de la sous-partie II.1. La reduction proprement
dite sera detaillee dans la sous-partie II.2.

II.1

Recherche de composantes fortement connexes dans un graphe oriente

Soit G un graphe oriente. Rappelons qu'un tel objet est defini par deux ensembles finis :
l'ensemble V des sommets (ou noeuds) et l'ensemble E des aretes orientees (ou arcs orientes).
Chaque arete de E relie deux sommets dans un ordre precis. C'est donc un element de (V × V ).
La taille du graphe G est |V |+|E|, ou |V | et |E| designent respectivement le nombre de sommets
et le nombre d'aretes.
Par defaut les sommets de G sont indexes par les entiers 0 a |V | - 1 inclus. Ainsi, on pourra
les designer par v0 , v1 , · · · , v|V |-1 . En machine nous representons G par listes d'adjacence, plus
precisement par un tableau de listes d'entiers :
type graphe == int list vect;;
ou les indices du tableau correspondent a ceux des noeuds du graphe et ou la liste associee a la
case d'indice i dans le tableau contient les indices des successeurs du noeud vi dans le graphe,
c'est-a-dire les entiers j tels que (vi , vj )  E. Voir la figure 2 pour une illustration.
0

v5

v7

v2

v3

v0

v6
v1

v4

1

4

3

2

3

3

2

0

4

0

1

5

2

7

6

5

1

7

6

2

Figure 2 ­ Un exemple de graphe oriente avec, a droite, une representation par listes d'adjacence. Les composantes fortement connexes du graphe sont encadrees en pointilles.
Rappelons qu'un chemin d'un sommet s a un sommet t dans G est une suite finie de
sommets (s = vi0 , vi1 , · · · , vik-1 , vik = t) telle que (vil , vil+1 )  E pour tout l = 0, 1, · · · , k - 1.
Ici, k designe la longueur du chemin. Par exemple, le graphe de la figure 2 contient le chemin
(v6 , v5 , v7 , v6 , v1 , v3 , v2 ) de longueur 6 et le chemin (v0 ) de longueur nulle, mais pas le chemin
(v0 , v4 ) de longueur 1.
Une composante fortement connexe de G est un sous-ensemble S de ses sommets, maximal
pour l'inclusion, tel que pour tout couple de sommets (s, t)  S 2 il existe un chemin de s a t
dans G. Voir la partie gauche de la figure 2 pour une illustration. Le calcul des composantes
5

fortement connexes de G peut se faire naivement en testant l'existence d'un chemin dans le
graphe pour chaque couple de sommets. Cette approche revient a effectuer un parcours complet
du graphe au depart de chaque sommet, par consequent elle est trop couteuse en temps. D'autres
approches permettent de faire le meme calcul en temps lineaire en la taille du graphe, dont celle
de Kosaraju-Sharir que nous allons maintenant etudier. L'algorithme procede en deux etapes :
a) Il effectue un parcours en profondeur recursif de G et releve, pour chaque noeud visite vi , l'instant ti de fin de traitement du noeud. Cet instant se situe a la fin de
l'execution de la fonction de parcours sur le noeud vi , apres le retour des appels recursifs
sur ses successeurs dans le graphe. Le code Caml correspondant est fourni ci-dessous :
la fonction dfs tri prend un graphe g en entree et renvoie la liste des indices des
sommets du graphe, ordonnee dans l'ordre inverse de leurs instants de fin de traitement (notez la ligne 8, qui insere l'indice du sommet courant en tete de liste au
moment de la fin de son traitement par la fonction de parcours recursif dfs rec) :
1 let dfs_tri g =
2
let deja_vu = make_vect (vect_length g) false in
3
let resultat = ref [] in
4
let rec dfs_rec i =
5
if not deja_vu.(i) then begin
6
deja_vu.(i) <- true; 7 do_list dfs_rec g.(i); (* voir page 2 pour la definition de do list *) 8 resultat := i :: !resultat; 9 end in 10 for i = 0 to vect_length g - 1 do dfs_rec i done; 11 !resultat;; dfs_tri: graphe -> int list
b) Il effectue un deuxieme parcours en profondeur, cette fois du graphe G obtenu en renversant le sens de toutes les aretes de G. Les differents sommets de depart du parcours sont
choisis non pas dans un ordre arbitraire comme a l'etape a) mais dans l'ordre decroissant
des instants ti . Pour chaque sommet de depart vi , l'ensemble des sommets visites par le
parcours en profondeur de G a partir de vi forme une composante fortement connexe du
graphe initial G.
Illustrons l'algorithme sur l'exemple de la figure 2 :
a) Le parcours en profondeur du graphe initial G, en considerant les sommets de depart par
ordre croissant d'indice comme dans la fonction dfs tri (ligne 10), choisit d'abord v0
comme point de depart. Le sous-graphe parcouru est alors le sommet v0 seul. Ensuite, le
parcours reprend au sommet v1 et visite le sommet v4 , puis revient a v1 et visite v3 puis
v2 , puis revient a v3 puis a v1 et s'arrete. Enfin, le parcours reprend au sommet v5 et
visite les sommets v7 puis v6 avant de revenir a v7 puis a v5 pour s'arreter. Les instants de
fin de traitement des sommets lors du parcours recursif sont donc dans l'ordre suivant :
t0 < t4 < t2 < t3 < t1 < t6 < t7 < t5 . La liste renvoyee par dfs tri est donc [5; 7; 6; 1; 3; 2; 4; 0]. 6 (2) b) Le parcours en profondeur du graphe renverse G , en considerant les sommets de depart dans l'ordre inverse de (2), choisit d'abord v5 et visite ainsi v6 et v7 , ce qui donne la composante {v5 , v6 , v7 }. Ensuite le parcours reprend du sommet v1 et visite ainsi v4 , ce qui donne la composante {v1 , v4 }. Ensuite le parcours reprend du sommet v3 et visite ainsi v2 , ce qui donne la composante {v2 , v3 }. Enfin le parcours reprend du sommet v0 et s'arrete la, ce qui donne la composante {v0 }. Codage de l'algorithme. L'etape a) de l'algorithme est deja codee dans dfs tri. Question 4 Justifier formellement la complexite lineaire (en la taille du graphe) de la fonction dfs tri. Rappelons que la taille du graphe est la somme de son nombre de sommets et de son nombre d'aretes. Pour pouvoir effectuer l'etape b) il faut d'abord renverser le graphe. Question 5 Ecrire une fonction renverser graphe qui prend en entree un graphe et qui renvoie un autre graphe dans lequel les sommets sont les memes et le sens de toutes les aretes est inverse. La complexite de la fonction doit etre lineaire en la taille du graphe fourni en entree. renverser_graphe: graphe -> graphe
Question 6 Ecrire une fonction dfs cfc qui code l'etape b) de l'algorithme. Elle prend en
entree le graphe renverse construit a la question precedente, ainsi que la liste d'entiers renvoyee
par dfs tri sur le graphe de depart. Elle renvoie une liste dans laquelle chaque element est
une liste d'entiers contenant les indices des sommets d'une composante fortement connexe du
graphe, sans doublons. La complexite de la fonction doit etre lineaire en la taille du graphe.
dfs_cfc: graphe -> int list -> int list list
Question 7 Ecrire enfin une fonction cfc qui prend en entree un graphe et qui renvoie une liste
de listes d'entiers contenant l'ensemble des composantes fortement connexes du graphe, chaque
composante fortement connexe etant stockee dans l'une des listes d'entiers. La complexite de la
fonction doit etre lineaire en la taille du graphe.
cfc: graphe -> int list list

Correction de l'algorithme. Nous dirons qu'une composante fortement connexe C de G
est subordonnee a une autre composante fortement connexe C  s'il existe des sommets vi  C
et vi  C  et un chemin de vi a vi dans G. Comme C et C  sont des composantes fortement
connexes, cela revient a dire qu'il existe des chemins dans G de n'importe quel sommet de C  a
n'importe quel sommet de C.
Question 8 Montrer que la relation etre subordonnee a est une relation d'ordre (pas forcement
totale) sur l'ensemble des composantes fortement connexes de C.

7

A chaque composante fortement connexe C on associe un instant tC de fin de traitement
comme ceci :
tC = max ti ,
vi C

ou les ti sont definis comme a l'etape a) de l'algorithme. Par exemple, dans l'exemple de la
figure 2 on a :
t0 = t{v0 } < t3 = t{v2 ,v3 } < t1 = t{v1 ,v4 } < t5 = t{v5 ,v6 ,v7 } . t0 que = t{vpour < tous t3 = sommets t{v2 ,v3 }  tj .
Question 10 Montrer que l'ordre total sur les composantes fortement connexes de G defini
par les instants de fin de traitement tC est compatible avec l'ordre partiel etre subordonnee
a, c'est-a-dire que pour toutes composantes C et C  telles que C est subordonnee a C  , on a
tC  tC  .
Question 11 En utilisant les resultats des questions precedentes, montrer que le parcours en
profondeur du graphe renverse G a l'etape b) de l'algorithme extrait les composantes fortement
connexes de G les unes apres les autres, dans l'ordre des tC decroissants. Pour cela on pourra
s'appuyer sur les observations simples suivantes sans les demontrer :
· Les composantes fortement connexes de G sont les memes que celles de G.
· La relation d'ordre etre subordonnee a dans G est inversee par rapport a celle dans G.

II.2

Des composantes fortement connexes a 2-SAT

La reduction d'une instance de 2-SAT a un calcul de composantes fortement connexes dans
un graphe repose sur l'observation simple que toute clause (li  lj ) est logiquement equivalente a
(¬li )  lj , elle-meme equivalente a sa contraposee (¬lj )  li . Lorsqu'une clause est formee d'un
seul litteral li , il suffit de l'exprimer sous la forme equivalente (li  li ), ce qui donne (¬li )  li ,
qui est sa propre contraposee. Cette observation suggere la procedure suivante pour construire
un graphe oriente G a partir d'une 2-FNC f a r variables (notees x0 , · · · , xr-1 ) :
· Pour chaque variable xi on ajoute les sommets v2i et v2i+1 a G, qui representent respectivement le litteral xi et le litteral ¬xi .
· Pour chaque clause de type (li ) on ajoute une arete a G, soit du sommet v2i+1 au sommet
v2i si li = xi , soit du sommet v2i au sommet v2i+1 si li = ¬xi .
· Pour chaque clause de type (li  lj ) ou les litteraux li , lj contiennent des variables xi , xj
distinctes, on ajoute deux aretes a G, choisies en fonction des cas suivants :
-- si li = xi et lj = xj , alors on ajoute les aretes (v2i+1 , v2j ) et (v2j+1 , v2i ),
-- si li = xi et lj = ¬xj , alors on ajoute les aretes (v2i+1 , v2j+1 ) et (v2j , v2i ),
-- si li = ¬xi et lj = xj , alors on ajoute les aretes (v2i , v2j ) et (v2j+1 , v2i+1 ),
-- si li = ¬xi et lj = ¬xj , alors on ajoute les aretes (v2i , v2j+1 ) et (v2j , v2i+1 ).
· Enfin, pour chaque clause de type (li  lj ) ou les litteraux li , lj contiennent la meme
variable xi = xj , soit on elimine directement la clause si elle est de la forme (xi  ¬xi )
ou (¬xi  xi ), soit on se ramene au cas d'une clause de type (li ) si elle est de la forme
(xi  xi ) ou (¬xi  ¬xi ).
Par exemple, sur la formule x0  (x1  ¬x0 ), la procedure donne un graphe avec quatre sommets :
v0 , v1 , v2 , v3 , et trois aretes : (v1 , v0 ), (v3 , v1 ), (v0 , v2 ), comme illustre dans la figure 3.
Question 12 Donner le resultat de la procedure ci-dessus sur la formule (x1  x2 )  x0  (x2 
¬x2 )  (¬x2  x0 ).
Question 13 Ecrire une fonction deux sat vers graphe qui prend en argument une FNC f ,
supposee etre une 2-FNC, et qui renvoie le graphe G obtenu par la procedure ci-dessus. On
8

v0

v1

v2

v3

Figure 3 ­ Le graphe obtenu a partir de la formule x0  (x1  ¬x0 ).
pourra utiliser la fonction var max codee a la question 2. Pour simplifier, on supposera qu'aucune
clause n'est repetee dans f et qu'aucune clause n'est de type (li lj ) ou li , lj contiennent la meme
variable xi = xj . La complexite de la fonction deux sat vers graphe doit etre lineaire en la
taille de f .
deux_sat_vers_graphe: fnc -> graphe
Question 14 Supposons que la 2-FNC initiale f soit satisfiable et soit  une valuation telle
que (f ) = Vrai. Montrer qu'alors, pour tous sommets vi , vj situes dans une meme composante fortement connexe de G, les variables booleennes xi/2 et xj/2 correspondantes verifient
(xi/2 ) = (xj/2 ) si (i - j) est pair et (xi/2 ) = ¬(xj/2 ) si (i - j) est impair. Ici la
notation · designe la partie entiere inferieure.
Question 15 En deduire que si f est satisfiable, alors il n'existe pas de variable xi dont les deux
sommets correspondants v2i et v2i+1 se trouvent dans la meme composante fortement connexe
du graphe G.
Reciproquement, on peut montrer que s'il n'existe pas de variable xi de f dont les deux
sommets correspondants v2i et v2i+1 se trouvent dans la meme composante fortement connexe
du graphe G, alors en attribuant la meme valeur booleenne a tous les litteraux impliques dans
chacune des composantes fortement connexes de G, on construit une valuation  telle que (f ) =
Vrai. Ceci fournit un critere simple pour decider de la satisfiabilite de f .
Question 16 Ecrire une fonction deux sat qui prend en entree une FNC f , supposee etre une
2-FNC, et qui renvoie un booleen indiquant si f est satisfiable ou non. La complexite de la
fonction doit etre lineaire en la taille de f .
deux_sat: fnc -> bool

Partie III. Resolution de k-SAT pour k arbitraire
Nous allons maintenant decrire un algorithme pour la resolution de k-SAT dans le cas general.
Le principe de base de l'algorithme est de faire une recherche exhaustive sur l'ensemble des
valuations possibles des variables de la formule. Pour chaque valuation consideree on evalue la
formule : si le resultat est Vrai alors on renvoie Vrai, si le resultat est Faux alors on rejette la
valuation courante et on passe a la suivante. L'algorithme est en fait un peu plus malin que cela :
il evalue la formule egalement pour des valuations partielles et decide, soit d'accepter la valuation
partielle courante si le resultat de l'evaluation est deja Vrai, soit de la rejeter precocement si le

9

resultat est deja Faux, soit enfin de completer la construction de la valuation si le resultat de
l'evaluation est encore Indetermine.
Pour coder les valuations partielles en machine nous allons utiliser des tableaux de trileens.
Rappelons que le type trileen a ete introduit dans la partie I. Ce type nous fait travailler
non plus dans l'algebre binaire de Boole, ou les variables prennent leurs valeurs parmi les deux
booleens habituels, mais dans l'algebre ternaire dite de Kleene, ou les variables prennent leurs
valeurs parmi les trois trileens. Les nouvelles tables de verite des connecteurs ,  et ¬ sont
donnees dans la figure 4.
ab
a

Vrai
Indet.
Faux

Vrai
Vrai
Indet.
Faux

b
Indet.
Indet.
Indet.
Faux

Faux
Faux
Faux
Faux

ab
a

Vrai
Indet.
Faux

Vrai
Vrai
Vrai
Vrai

b
Indet.
Vrai
Indet.
Indet.

Faux
Vrai
Indet.
Faux

a

¬a

Vrai
Indet.
Faux

Faux
Indet.
Vrai

Figure 4 ­ Tables de verite des connecteurs logiques usuels sur les trileens. Les valeurs d'affectation des variables sont respectivement Vrai, Indet(ermine), Faux.
Question 17 Ecrire trois fonctions : et, ou, non, qui codent respectivement les connecteurs
logiques , , ¬ sur les trileens. La complexite de chaque fonction doit etre constante.
et: trileen -> trileen -> trileen
ou: trileen -> trileen -> trileen
non: trileen -> trileen
Supposons maintenant que les variables d'une FNC prennent leurs valeurs parmi les trileens.
Une recurrence immediate montre alors qu'une clause disjonctive de la formule vaut Vrai
quand l'un au moins de ses litteraux vaut Vrai, Faux quand tous ses litteraux valent Faux,
et Indetermine dans tous les autres cas. Une autre recurrence immediate montre que la FNC
elle-meme vaut Vrai quand toutes ses clauses valent Vrai, Faux quand au moins l'une de ses
clauses vaut Faux, et Indetermine dans tous les autres cas.
Question 18 En vous appuyant sur la remarque ci-dessus et sur les fonctions de la question 17,
ecrire une fonction eval qui prend en entree une FNC f ainsi qu'un tableau de trileens t, et qui
renvoie un trileen indiquant si le resultat de l'evaluation de f sur la valuation partielle fournie
dans t est Vrai, Faux ou Indetermine. On supposera que t a la bonne taille. La complexite de
la fonction doit etre lineaire en la taille de la formule.
eval: fnc -> trileen vect -> trileen
Nous pouvons maintenant decrire l'algorithme de recherche exhaustive avec terminaison
precoce. Pour iterer sur l'ensemble des valuations nous utilisons une approche recursive consistant a parcourir en profondeur les branches d'un arbre binaire sans le construire explicitement.
Chaque niveau i de l'arbre correspond a l'affectation de la variable xi , comme illustre dans la
figure 5 pour le cas de 3 variables.

10

x0
Vr
ai

ux
Fa

Vra
i

x
Fau

x
Fau

Vra
i

x1

Vrai

Vrai

Vrai

Faux

Faux

Faux

Faux

Vrai

x2

Figure 5 ­ Arbre parcouru lors de la recherche exhaustive parmi les valuations des variables
x0 , x1 , x2 .
Au depart la valeur Indetermine est affectee a toutes les variables. Le parcours commence a
la racine. A chaque noeud de l'arbre visite, avant toute affectation de la variable correspondante,
un appel a la fonction eval est fait pour tester si le resultat de l'evaluation est :
· Vrai, auquel cas l'exploration s'arrete et la formule est satisfiable,
· Faux, auquel cas l'exploration de la branche courante de l'arbre s'interrompt
prematurement pour reprendre au niveau du parent du noeud courant,
· Indetermine, auquel cas l'exploration de la branche courante de l'arbre se poursuit normalement.
Comme indique precedemment, pour stocker la valuation partielle courante on utilise un
tableau de trileens dans lequel les variables non encore affectees prennent la valeur Indetermine.
Question 19 Ecrire une fonction k sat qui prend en entree une FNC f et qui renvoie un booleen
valant true si f est satisfiable et false sinon. La fonction doit coder la methode de recherche
exhaustive avec terminaison precoce decrite ci-dessus. Sa complexite doit etre en O(n 2n ), ou n
est la taille de f . En outre, un soin particulier doit etre apporte a la clarte du code, dans lequel
il est recommande d'inserer des commentaires aux points cles.
k_sat: fnc -> bool

Partie IV. De k-SAT a SAT
Des le debut du sujet nous avons laisse de cote le probleme SAT au profit de sa variante
k-SAT. Comme toute instance du deuxieme probleme est egalement une instance du premier,
k-SAT est a priori une version restreinte de SAT. En fait il n'en est rien car, comme nous allons
le voir dans cette partie, toute instance de SAT peut etre transformee en une instance de kSAT (pour k  3) par un algorithme de complexite polynomiale. Ainsi, l'algorithme code a la
question 19, ou tout autre algorithme exponentiel optimise pour k-SAT, peut en fait resoudre
n'importe quelle instance de SAT avec la meme complexite.

11

Pour la transformation proprement dite, la premiere etape consiste a mettre en FNC la
formule booleenne consideree. En effet, toute formule booleenne peut etre mise en FNC et une
approche evidente pour ce faire est d'utiliser les proprietes des connecteurs logiques rappelees
dans la partie preliminaire.
Question 20 Pour chacune des formules suivantes, utiliser l'involutivite de la negation, l'associativite et la distributivite des connecteurs  et , ainsi que les lois de De Morgan pour
transformer la formule en FNC. Seul le resultat du calcul est demande :
a) (x1  ¬x0 )  ¬(x4  ¬(x3  x2 ))
b) (x0  x1 )  (x2  x3 )  (x4  x5 )
L'exemple b) de la question 20 se generalise a des formules de taille arbitraire, ce qui montre que
l'approche ci-dessus n'est pas efficace puisque la FNC obtenue peut avoir une taille exponentielle
en la taille n de la formule booleenne f de depart. Nous allons donc adopter une autre strategie,
qui sera d'introduire de nouvelles variables et de remplacer f par une autre formule f  qui est
equisatisfiable, c'est-a-dire que f  est satisfiable si et seulement si f l'est. La formule f  sera en
FNC et sa taille sera polynomiale en n. La procedure pour construire f  a partir de f fonctionne
en deux temps :
1. On commence par appliquer les lois de De Morgan recursivement a l'arbre d'expression
associe a f , de maniere a faire descendre toutes les negations au niveau des noeuds parents des variables. Soit f  la nouvelle formule ainsi obtenue, qui par construction est
logiquement equivalente a f . Par exemple, si f est la formule a) de la question 20, alors
f  = (x1  ¬x0 )  (¬x4  (x3  x2 )).
2. Ensuite on applique recursivement les regles de reecriture suivantes a l'arbre d'expression
de f  :
· si f  =     , alors on pose f  =     , ou  et   sont les versions reecrites de
 et   respectivement,
· si f  =     , V
alors on introduit
x dans
Vq une nouvelle variable
Vbooleenne
Vqla formule
p
p

et on pose f = i=1 (i  x)  j=1 (j  ¬x), ou  = i=1 i et  = j=1 j sont
les versions reecrites de  et   respectivement.
Par exemple, en reprenant la formule f  obtenue dans l'exemple de l'etape 1, on a f  =
(x1  x5 )  (¬x0  ¬x5 )  (¬x4  x6 )  (x3  ¬x6 )  (x2  ¬x6 ) en introduisant les nouvelles
variables x5 et x6 .
Question 21 Montrer que les formules f et f  sont equisatisfiables.
Question 22 Ecrire une fonction negs en bas qui effectue l'etape 1 ci-dessus, c'est-a-dire qu'elle
prend en argument une formule f et renvoie une autre formule f  logiquement equivalente et
dans laquelle tous les connecteurs ¬ ont des variables pour fils dans l'arbre d'expression. La
fonction negs en bas doit avoir une complexite lineaire en la taille de f .
negs_en_bas: formule -> formule
On se donne a present une nouvelle fonction var max, qui prend une formule en argument et
qui renvoie le plus grand indice de variable utilise dans la formule. La complexite de la fonction
est lineaire en la taille de la formule.

12

Question 23 Ecrire une fonction formule vers fnc qui prend en argument la formule f 
obtenue a l'issue de l'etape 1 et qui renvoie la FNC f  construite comme a l'etape 2. La complexite
de la fonction formule vers fnc doit etre polynomiale en la taille de f  .
formule_vers_fnc: formule -> fnc
Question 24 Justifier les complexites des fonctions negs en bas et formule vers fnc. On
pourra par exemple montrer que le nombre de clauses formees dans formule vers fnc est egal
au nombre de litteraux dans la formule f  .
Ainsi, il suffit de combiner les fonctions des questions 22 et 23 pour convertir n'importe
quelle formule booleenne f en une FNC f  equisatisfiable en temps polynomial.

*
* *
De maniere similaire, on peut convertir la FNC f  en une 3-FNC f  equisatisfiable en temps
polynomial. L'approche est la suivante
: toute clause de f  avec au plus 3 litteraux reste inWni
changee, tandis que toute clause j=1 lij avec ni > 3 devient :
(li1  li2  xi1 )  (¬xi1  li3  xi2 )  · · ·  (¬xi(ni -4)  li(ni -2)  xi(ni -3) )  (¬xi(ni -3)  li(ni -1)  lini ),
ou xi1 , · · · , xi(ni -3) sont de nouvelles variables introduites specialement pour cette clause. On
peut alors montrer que la formule f  ainsi obtenue est de taille polynomiale en la taille de f  et
equisatifsiable. Des lors, l'instance initiale de SAT est transformee en une instance de 3-SAT (et
donc de k-SAT pour n'importe quel k  3) equisatisfiable et de taille polynomiale.
La methode decrite dans la partie IV du sujet transforme toute instance de SAT en une
instance de 3-SAT equisatisfiable en temps polynomial. Des lors, la fonction eval de la question 18 permet, etant donnees une formule booleenne f quelconque de taille n a r variables
x0 , · · · , xr-1 et une valuation  : {x0 , · · · , xr-1 }  {Vrai, Faux}, de verifier en temps polynomial (en n, rappelons que l'on a r  n) si (f ) = Vrai. Ainsi, du point de vue de la theorie
de la complexite, le probleme SAT se trouve etre dans la classe de complexite NP. Cette classe
est constituee precisement des problemes dont on peut verifier la solution en temps polynomial
quand cette derniere existe. Cela ne veut pas dire qu'une telle solution peut etre trouvee (ni
meme son existence determinee) en temps polynomial. Les problemes pour lesquels c'est le cas
forment la classe de complexite appelee P. Clairement, on a PNP puisque si l'on peut trouver
une solution en temps polynomial alors on peut a fortiori verifier en temps polynomial qu'on a
bien une solution. Savoir si P est egal a NP est une question encore ouverte a ce jour et sans
conteste l'une des plus fameuses en informatique fondamentale.
Parmi les problemes de la classe NP, certains sont particulierement difficiles, au moins
aussi difficiles que tous les autres. Ces problemes sont dits NP-complets. Formellement, un
probleme P1  NP est dit NP-complet s'il existe une reduction polynomiale de chaque
probleme P2  NP vers ce probleme, c'est-a-dire un algorithme qui transforme toute instance u de
P2 en une instance v de P1 en temps polynomial, de telle sorte que la reponse ("oui" / "non")
de P1 sur l'instance transformee v est la meme que celle de P2 sur l'instance initiale u. Un
probleme NP-complet permet ainsi de resoudre les instances de n'importe quel autre probleme
de la classe NP. D'ou l'importance des problemes NP-complets, puisque si l'un d'eux s'averait
13

etre dans P alors tous les autres y seraient egalement et l'on aurait P=NP. A contrario, si l'on
avait P6=NP alors aucun probleme NP-complet ne serait resoluble en temps polynomial.
Historiquement, SAT fut le premier probleme a etre identifie comme etant NP-complet. C'est
le fameux theoreme de Cook-Levin (1971). Ce resultat explique l'importance qu'a eue SAT dans
le developpement de la theorie de la complexite. La transformation decrite dans la partie IV
du sujet donne une reduction polynomiale de SAT a 3-SAT. Des lors, 3-SAT (ainsi que k-SAT
pour tout k  3) est egalement NP-complet. Par consequent, l'algorithme exponentiel de la
question 19 permet de resoudre toutes les instances de tous les problemes de la classe NP.
A contrario, si P6=NP alors il n'existe pas d'algorithme permettant de resoudre chacune des
instances de 3-SAT (ou de k-SAT pour k  3) en temps polynomial. On comprend des lors
l'ampleur du fosse qui separe les petites valeurs de k (k = 1, 2), pour lesquelles des algorithmes
lineaires existent comme decrit dans les parties I et II du sujet, des valeurs plus grandes (k  3),
pour lesquelles il n'existe peut-etre pas d'algorithme polynomial. Ceci est l'un des nombreux
effets de seuil observes dans la complexite du probleme SAT et de ses variantes.

*
* *

14