X/ENS Informatique A MP 2016

Thème de l'épreuve Satisfiabilité des formules booléennes
Principaux outils utilisés logique, programmation, algorithmes de graphes
Mots clefs forme normale conjonctive, clauses, littéraux, satisfiabilité, composantes fortements connexes, algorithme de Kosaraju-Sharir

Corrigé

(c'est payant, sauf le début): - - - - - - - - - - - - - - - - - - - - - - - - -

Extrait gratuit du corrigé

(télécharger le PDF)
           

Énoncé complet

(télécharger le PDF)
                                         

Rapport du jury

(télécharger le PDF)
              

Énoncé obtenu par reconnaissance optique des caractères


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 

Extrait du corrigé obtenu par reconnaissance optique des caractères


 X/ENS Informatique A MP 2016 -- Corrigé Ce corrigé est proposé par Benjamin Monmege (enseignant-chercheur à l'université) ; il a été relu par Vincent Puyhaubert (professeur en CPGE). Ce sujet s'intéresse à des algorithmes testant la satisfiabilité d'une formule de la logique propositionnelle. Ce problème célèbre et crucial dans un grand nombre d'applications, allant de la vérification de programmes à l'intelligence artificielle, est difficile : il s'agit d'un problème « NP-complet », c'est-à-dire qu'il est possible de vérifier en temps polynomial si une valuation des variables satisfait la formule, mais qu'on ne connaît pas à ce jour d'algorithme en temps polynomial testant la satisfiabilité d'une formule dans le cas général. · Dans une partie préliminaire, les notations sont introduites, ainsi que la notion cruciale de formule en forme normale conjonctive (FNC). Il s'agit d'une conjonction de clauses, chaque clause étant une disjonction de littéraux. On parle de formule en k-FNC lorsque chaque clause de la formule possède au plus k littéraux. · La partie I propose l'écriture d'un algorithme en temps linéaire pour résoudre le problème dans le cas particulier de formules en 1-FNC. · La partie II étudie ensuite les formules en 2-FNC. L'algorithme de satisfiabilité étudié utilise une modélisation des formules sous forme de graphe. La satisfiabilité d'une formule est alors réduite à la vérification d'une propriété des composantes fortement connexes du graphe. La partie commence donc par étudier une implémentation de l'algorithme de Kosaraju­Sharir pour calculer les composantes fortement connexes d'un graphe, ainsi que sa correction et sa complexité. La preuve de correction proposée par l'énoncé contient une question (la 9) qui s'avère fausse. Le reste de la partie est cependant traitable en l'état, bien que la question 10 soit plus ardue sans l'aide de la question 9. Le lien avec les formules en 2-FNC est fait par la suite, afin d'obtenir un algorithme de complexité linéaire. · La partie III étudie ensuite un algorithme consistant à tester systématiquement toutes les valuations possibles, dans le cas général d'une formule en FNC. L'ensemble de valuations, de taille exponentielle, est naturellement structuré sous la forme d'un arbre binaire et l'on utilise cette structure pour permettre une exploration partielle de l'arbre afin d'accélérer le calcul. · Finalement, la partie IV montre que toute formule de la logique propositionnelle peut être encodée en temps polynomial en une formule en FNC, et même plus précisément en 3-FNC comme l'explique la conclusion du sujet. Ce sujet est remarquable, si on oublie la question 9 fausse. Il permet de travailler en profondeur la partie logique du programme, tout en posant des questions de programmation de difficulté croissante. Il aborde également un problème classique sur les graphes et permettra donc une révision de ces différents sujets. Dans le corrigé, les codes sont écrits en OCaml plutôt qu'en Caml Light, comme le demandait pourtant l'énoncé, car c'est le langage devenu obligatoire aux concours à partir de la session 2019. En particulier, plutôt que d'utiliser les fonctions do_list, map, it_list et list_it rappelées par l'énoncé, on utilisera leur équivalent dans OCaml : List.iter, List.map, List.fold_left et List.fold_right. Indications 2 Attention à ne pas confondre l'indice de variable maximal avec le nombre de clauses ou la taille maximale d'une clause. Bien analyser aussi le cas d'une clause ou d'une formule vide. 3 Si k est le plus grand indice d'une variable, la formule possède k + 1 variables et il faut donc allouer un tableau de cette taille pour stocker la valuation. 4 Dénombrer les appels à la fonction dfs_rec et majorer la complexité de chaque appel si on ne comptabilise pas la complexité des appels récursifs à dfs_rec. 6 Suivre une écriture proche de la fonction dfs_tri pour effectuer un parcours en profondeur. Plutôt que la boucle for en ligne 10 de la fonction dfs_tri, opter pour une fonction récursive supplémentaire qui parcourt la liste des sommets donnée en argument de dfs_cfc. 7 Combiner les fonctions dfs_tri, renverser_graphe et dfs_cfc. 8 Une relation d'ordre est une relation binaire qui doit être réflexive, antisymétrique et transitive. 9 Cette question est fausse, il n'est donc pas utile d'essayer de la traiter. 10 Commencer par montrer qu'au moment où un sommet vi est visité pour la première fois, s'il existe un chemin de vi à vj n'empruntant que des sommets distincts pas encore vus, alors tj 6 ti . En déduire que si C est une composante fortement connexe du graphe G et tC = ti , alors le sommet vi est le premier sommet visité parmi ceux de la composante C. Conclure que tC < tC0 si C est subordonnée à C0 , avec tC = ti et tC0 = tj , en considérant deux cas, selon que vi est vu avant vj pendant le parcours, ou vice versa. On pourra considérer le cas où il existe un arc allant directement de la composante C0 à la composant C. 11 Expliquer pourquoi la première liste L retournée dans la liste de listes contient tous les sommets de la composante fortement connexe C d'instant tC maximal, puis que ce sont les seuls sommets de L en utilisant le résultat de la question 10. 12 La clause x2 ¬x2 doit être éliminée, suivant la procédure donnée. 14 Commencer par expliquer pourquoi la formule `i `j est une tautologie dès lors que les sommets vi et vj , associés aux littéraux `i et `j , sont tels qu'il existe un chemin de vi à vj dans G. 16 Pour respecter la complexité linéaire demandée par l'énoncé, on ne peut pas vérifier chaque composante en testant la présence du sommet v2i pour chaque sommet v2i+1 présent dans la composante. À la place, on pourra remplir un tableau associant à chaque sommet un numéro, unique pour chaque composante. 18 Utiliser la fonction non de la question 17 pour proposer une fonction évaluant un littéral, puis la fonction ou pour évaluer une clause, et enfin la fonction et pour évaluer une formule en FNC. 19 Un parcours d'arbre peut s'implémenter aisément de façon récursive. 20 Pour appliquer la distributivité de la disjonction sur la conjonction, tout fonctionne comme on le ferait habituellement avec un produit de sommes de variables. De même que pour des variables réelles x0 , x1 , x2 , x3 , x4 , (x0 + x1 + x2 ) × (x3 + x4 ) = x0 × x3 + x0 × x4 + · · · + x2 × x4 les formules de variables booléennes x0 , x1 , x2 , x3 (x0 x1 x2 ) (x2 x3 ) et (x0 x3 ) (x0 x4 ) · · · (x2 x4 ) sont équivalentes. 21 Pour montrer que f 0 et f sont équisatisfiables, on pourra procéder par récurrence en montrant que toute valuation satisfaisant f 0 satisfait aussi f , et que toute valuation satisfaisant f peut être prolongée en une valuation satisfaisant f 0 . 23 Utiliser une fonction récursive pour parcourir la formule f tout en maintenant le prochain numéro de variable à donner dans le cas d'une disjonction f = . Faire la conjonction de deux formules en FNC revient à concaténer les listes correspondantes. Préliminaires 1 L'énoncé ne demande pas de justification, mais nous en donnons une tout de même dans ce corrigé, pour aider à la compréhension. a) La formule x1 (x0 ¬x0 ) ¬x1 est insatisfiable puisque, pour être satisfaite, la variable x1 doit être à la fois Vrai et Faux. b) La formule (x0 ¬x1 ) (¬x0 x2 ) (x1 ¬x2 ) est satisfiable, par exemple via la valuation telle que (x0 ) = (x1 ) = (x2 ) = Vrai. c) La formule x0 ¬(x0 ¬(x1 ¬(x1 ¬x2 ))) est satisfiable, par exemple avec la même valuation que précédemment. d) La formule (x0 x1 ) (¬x0 x1 ) (x0 ¬x1 ) (¬x0 ¬x1 ) est insatisfiable puisque, pour être satisfaites, les deux premières disjonctions impliquent que la variable x1 doit être Vrai, alors que les deux dernières impliquent que x1 doit être Faux. 2 Commençons par calculer récursivement le plus grand indice de variable utilisé dans une clause, en utilisant la fonction max : 'a -> 'a -> 'a de la bibliothèque standard d'OCaml. Puisque l'énoncé stipule que les variables sont indexées par des entiers positifs ou nuls, une clause vide est associée à l'indice -1, pour la différencier de la clause x0 associée à l'indice 0. let rec var_max_clause c = match c with | [] -> -1 | (V x) :: c -> max x (var_max_clause c) | (NV x) :: c -> max x (var_max_clause c);; Utilisons ensuite cette fonction pour calculer récursivement le plus grand indice de variable utilisé dans une formule, en associant à nouveau l'indice -1 à la formule vide. let rec var_max f = match f with | [] -> -1 | c :: f -> max (var_max_clause c) (var_max f);; Il est aussi possible d'écrire ces deux fonctions à l'aide de la fonction List.fold_left, rappelée sous le nom de it_list dans l'énoncé. On extrait pour simplifier une fonction variable associant à un littéral l'indice de sa variable. let variable = function | V x -> x | NV x -> x;; let var_max_clause c = List.fold_left (fun n l -> max n (variable l)) (-1) c;; let var_max f = List.fold_left (fun n c -> max n (var_max_clause c)) (-1) f;;