Aller au contenu

Algorithme de Kosaraju et 2-SAT

Ce TP accompagne le chapitre Algorithmique avancée des graphes. Il est disponible sous forme de notebook Jupyter.

Kosaraju

On va considérer un type graphe où les sommets ne sont pas forcément des entiers et où on stocke une table de hachage pour faire la correspondance entre la valeur d'un sommet et son indice.

type 'a graphe = {
    sommets : 'a array;
    sommets_indices : ('a, int) Hashtbl.t;
    ladj : int list array
}

Question 1. Écrire une fonction qui étant donné un tableau t va construire la table des associations t.(i) -> i qui permettra ainsi de remonter du tableau à l'indice.

Note C'est le moment de retourner apprendre par cœur la documentation du module Hashtbl.

Corrigé 
let table_indices (t:'a array) : ('a, int) Hashtbl.t =
    let h = Hashtbl.create (Array.length t) in
    for i = 0 to Array.length t - 1 do
        Hashtbl.add h t.(i) i
    done;
    h

Question 2. Écrire une fonction indice qui prend un graphe et un sommet et renvoie son indice en utilisant la table sommets_indices.

Corrigé 
let indice g a = Hashtbl.find g.sommets_indices a

Question 3. En déduire une fonction cree_graphe qui va prendre un tableau sommets et créer un graphe sans arêtes dont ce sont les sommets.

Corrigé 
let cree_graphe sommets =
    {
        sommets = sommets;
        sommets_indices = table_indices sommets;
        ladj = Array.make (Array.length sommets) []
    }

Question 4. Écrire une fonction ajoute_arete telle que ajoute_arete g a b ajoute l'arête a -> b où les sommets sont donnés par leur valeur et non pas par leur indice.

Corrigé 
let ajoute_arete g a b =
    let ia = indice g a in
    let ib = indice g b in
    if not (List.mem ib g.ladj.(ia))
    then g.ladj.(ia) <- ib :: g.ladj.(ia)

Les deux cellules suivantes permettent de définir le graphe vu dans le cours en exemple :

let ex_cours = cree_graphe [|'a';'b';'c';'d';'e';'f';'g';'h';'i';'j';'k';'l';'m';'n';'o';'p'|]

List.iter (fun (a,b) -> ajoute_arete ex_cours a b)
    [('a','b'); ('b','f'); ('g','a');('f','g');
     ('c','h'); ('g','c'); ('d','c');('h','d');
     ('e','f'); ('f','l'); ('e','i'); ('g','k');
     ('h','l'); ('i','n'); ('j','m'); ('j','k');
     ('k','l'); ('k','h'); ('l','o'); ('l','p');
     ('m','i'); ('n','j'); ('n','o'); ('o','k')]

Question 5. Écrire une fonction graphe_miroir qui renvoie le graphe miroir du graphe donné, c'est-à-dire qui renverse toutes les arêtes.

Corrigé 
let graphe_miroir g =
    let gr = {
        sommets = g.sommets;
        sommets_indices = g.sommets_indices;
        ladj = Array.make (Array.length g.sommets) []
    } in
    for i = 0 to Array.length g.sommets - 1 do
        List.iter (fun j -> gr.ladj.(j) <- i :: gr.ladj.(j)) g.ladj.(i)
    done;
    gr

Question 6. Écrire une fonction dfs qui va parcourir en profondeur un graphe et appliquer une fonction de post-traitement. Pas besoin de noter les temps de sortie puisqu'ils correspondent au moment où on effectue ce traitement.

Corrigé 
let rec dfs g trait visites x =
    if not visites.(x)
    then begin
        visites.(x) <- true;
        List.iter (fun y ->
            if not visites.(y)
            then dfs g trait visites y
        ) g.ladj.(x);
        trait x
    end

Question 7. En déduire une fonction kosaraju qui renvoie un tableau indiquant le numéro de la composante fortement connexe de chaque sommet.

Attention, cette fonction va être un peu compliquée, on indique les grandes lignes ici :

  • on initialise un tableau de visites ;
  • on va construire une liste ordre des indices de sommets rencontrés lors d'un premier DFS de tout le graphe grâce à un post-traitement (avec une référence) ;
  • on calcule \(G^R\) et on initialise un tableau de visites ;
  • on fait des DFS dans \(G^R\) mais en prenant les sommets depuis la liste ordre. En post-traitement, on va remplir un tableau comp où comp.(x) sera le numéro de la composante fortement connexe de x.

On commence par numéroter les composantes à 1.

Corrigé 
let kosaraju g =
    let n = Array.length g.sommets in
    let ordre = ref [] in
    let visites = Array.make n false in
    for i = 0 to n-1 do
        if not visites.(i)
        then dfs g (fun x -> ordre := x :: !ordre) visites i
    done;
    let gr = graphe_miroir g in
    let visites = Array.make n false in
    let ncomp = ref 0 in
    let comp = Array.make n 0 in
    List.iter (fun ia ->
        if not visites.(ia)
        then begin
            incr ncomp;
            dfs gr (fun x -> comp.(x) <- !ncomp) visites ia
        end
        ) !ordre;
    comp

Comme on ajoute chaque sommet en tête de ordre au moment où il devient traité, ordre contient les sommets par temps de sortie décroissant.

Pour tester :

assert (kosaraju ex_cours = [|3; 3; 4; 4; 1; 3; 3; 4; 2; 2; 4; 4; 2; 2; 4; 5|]);
"OK"

Question 8. Cette représentation des composantes va nous être utile mais elle n'est pas très maniable. Écrire une fonction listes_comp telle que listes_comp sommets comp renvoie le tableau des composantes données sous forme de listes de sommets.

Corrigé 
let listes_comp sommets comp =
    let n = Array.fold_left max 0 comp in
    let comp_l = Array.make n [] in
    for i = 0 to Array.length comp - 1 do
        let n = comp.(i) in
        comp_l.(n-1) <- sommets.(i) :: comp_l.(n-1)
    done;
    comp_l

Pour tester :

assert (listes_comp ex_cours.sommets (kosaraju ex_cours) =
    [|['e']; ['n'; 'm'; 'j'; 'i'];
      ['g'; 'f'; 'b'; 'a'];  ['o'; 'l'; 'k'; 'h'; 'd'; 'c']; ['p']|]);
"OK"

Remarque

Pour tester kosaraju plus largement, on peut comparer son résultat sur des petits graphes aléatoires avec une méthode naïve : on calcule pour chaque sommet \(x\) l'ensemble des sommets accessibles par un parcours, et on vérifie que comp.(x) = comp.(y) si et seulement si \(y\) est accessible depuis \(x\) et \(x\) depuis \(y\). On peut aussi vérifier que pour toute arête \(x \rightarrow y\), comp.(x) <= comp.(y) : c'est la propriété de numérotation utilisée pour 2-SAT ci-dessous.

2-SAT

On va résoudre 2-SAT en utilisant l'algorithme de Kosaraju. Tout d'abord, on rappelle que les formules de 2-SAT sont des conjonctions de clauses comportant chacune deux littéraux (voir le chapitre Calcul propositionnel).

Exemple : \(f = (a \vee \neg b) \wedge (\neg a \vee b) \wedge (\neg a \vee \neg b) \wedge (a \vee \neg c)\)

On reprend un type proche de ce qui a été fait l'an dernier, sauf que les clauses sont des couples de littéraux.

type lit = Pos of char | Neg of char
type clause = lit * lit
type formule = clause list

La formule donnée au-dessus s'écrit alors :

let f = [ (Pos 'a', Neg 'b'); (Neg 'a', Pos 'b'); (Neg 'a', Neg 'b'); (Pos 'a', Neg 'c') ]

Question 9. Écrire une fonction label : lit -> char qui renvoie l'étiquette d'un littéral et une fonction neg : lit -> lit qui renvoie le littéral opposé d'un littéral donné.

Corrigé 
let label = function Pos a | Neg a -> a

let neg = function Pos a -> Neg a | Neg a -> Pos a

Question 10. Écrire une fonction variables qui renvoie les étiquettes de tous les littéraux sans répétitions. On pourra utiliser List.sort_uniq Stdlib.compare.

Corrigé 
let variables f =
    let rec var_aux f =
        match f with
        | [] -> []
        | c::f' -> var_clause c @ var_aux f'
    and var_clause (l1,l2) = [label l1; label l2]
    in List.sort_uniq Stdlib.compare (var_aux f)

Question 11. On peut écrire \(a \vee b\) sous la forme implicative \((\neg a \rightarrow b) \wedge(\neg b \rightarrow a)\).

En faisant cela, on peut alors construire un graphe sur les littéraux où \(l \rightarrow l'\) quand cette implication apparaît dans la formule.

Écrire une fonction implication_graphe qui étant donnée f renvoie ce graphe.

Corrigé 
let implication_graphe f =
    let v = variables f in
    let s = List.concat (List.map (fun x -> [Pos x; Neg x]) v) in
    let sommets = Array.of_list s in
    let g = cree_graphe sommets in
    List.iter (fun (a,b) ->
        ajoute_arete g (neg a) b;
        ajoute_arete g (neg b) a
    ) f;
    g

Les sommets sont rangés par variable : le sommet d'indice \(2i\) est Pos x et celui d'indice \(2i+1\) est Neg x pour la \(i\)-ème variable x.

On cherche alors une valuation des variables telle qu'il n'y ait pas d'arête \(\top \rightarrow \perp\) d'un littéral vrai vers un littéral faux. En effet, toutes les autres affectations vérifient la clause correspondante. Ainsi, tous les littéraux d'une composante fortement connexe doivent nécessairement avoir la même valeur de vérité. Si \(C \rightarrow C'\) pour deux composantes, on ne peut pas affecter la valeur vraie à \(C\) et fausse à \(C'\). On remarque que le graphe est symétrique par contraposition, donc il existe une composante niée \(\neg C\) pour chaque composante \(C\).

L'idée pour résoudre 2-SAT est donc de calculer les composantes fortement connexes et de parcourir leur graphe acyclique en partant des puits, en affectant la valeur vraie à la première composante rencontrée entre \(C\) et \(\neg C\).

Pour résoudre 2-SAT, on va appliquer Kosaraju sur le graphe d'implication de la formule.

kosaraju (implication_graphe f)

Sur ce graphe, on remarque que si deux littéraux opposés sont dans la même composante fortement connexe, alors la formule est insatisfiable. Si ce n'est pas le cas, on peut démontrer que la valuation suivante fonctionne :

\[ \forall a \in V, v(a) = \begin{cases} \top & \text{si } comp(a) > comp(\neg a) \\ \perp & \text{sinon }\end{cases} \]

Cette affirmation repose sur deux propriétés :

  • les composantes sont numérotées dans l'ordre croissant d'un tri topologique de leur graphe, qui est acyclique : pour toute arête \(x \rightarrow y\), \(comp(x) \le comp(y)\) ;
  • le graphe d'implication possède une symétrie par contraposition : si \(a_1 \rightarrow a_2 \dots \rightarrow a_n\) alors \(\neg a_n \rightarrow \neg a_{n-1} \dots \rightarrow \neg a_1\).

Théorème

Une formule de 2-SAT est satisfiable si et seulement si aucune variable \(a\) n'est dans la même composante fortement connexe que \(\neg a\) dans son graphe d'implication. Dans ce cas, la valuation \(v\) ci-dessus est un modèle.

Preuve

Si \(v\) est un modèle, chaque arête \(l \rightarrow l'\) provient d'une clause \(\neg l \vee l'\) satisfaite par \(v\) : si \(l\) est vrai, \(l'\) aussi. Par récurrence, deux littéraux reliés par un chemin \(l \leadsto l'\) vérifient : si \(l\) est vrai, \(l'\) l'est. Si \(a\) et \(\neg a\) étaient dans la même composante, on aurait \(a \leadsto \neg a\) et \(\neg a \leadsto a\), donc \(a\) vrai entraîne \(\neg a\) vrai et réciproquement : impossible.

Réciproquement, supposons que \(comp(a) \neq comp(\neg a)\) pour toute variable \(a\). Montrons d'abord que la valuation \(v\) rend vrai le littéral \(l\) (positif ou négatif) si et seulement si \(comp(l) > comp(\neg l)\). C'est la définition si \(l = a\) ; si \(l = \neg a\), \(l\) est vrai si et seulement si \(comp(a) < comp(\neg a)\), c'est-à-dire \(comp(l) > comp(\neg l)\) puisque les deux numéros sont distincts.

Soit une clause \(l \vee l'\) et supposons par l'absurde que \(v\) rende \(l\) et \(l'\) faux : \(comp(l) < comp(\neg l)\) et \(comp(l') < comp(\neg l')\). Les arêtes \(\neg l \rightarrow l'\) et \(\neg l' \rightarrow l\) du graphe donnent, par la première propriété, \(comp(\neg l) \le comp(l')\) et \(comp(\neg l') \le comp(l)\). On obtient \(comp(l) < comp(\neg l) \le comp(l') < comp(\neg l') \le comp(l)\), ce qui est absurde. Toutes les clauses sont donc satisfaites.

La première propriété découle de l'étude de Kosaraju dans le cours : la deuxième passe découvre les composantes par temps de sortie décroissant, et une arête \(x \rightarrow y\) entre deux composantes distinctes impose \(t_s(\overline{y}) < t_s(\overline{x})\), donc \(comp(x) < comp(y)\).

On remarque que la preuve n'utilise pas directement la symétrie : celle-ci garantit simplement que \(\neg C\) est une composante, ce qui donne l'interprétation précédente en termes de composantes.

Question 12. En déduire une fonction resout_2sat qui étant donné une formule renvoie None si elle est insatisfiable, et Some l où l est une liste de couples (variable,valeur) représentant une valuation solution.

Corrigé 
let resout_2sat f =
    let g = implication_graphe f in
    let comp = kosaraju g in
    let n = Array.length g.sommets / 2 in
    let valuation = ref [] in
    let insoluble = ref false in
    for i = 0 to n-1 do
        (* g.sommets.(2*i) est Pos a et g.sommets.(2*i+1) est Neg a *)
        let a = label g.sommets.(2*i) in
        if comp.(2*i) = comp.(2*i+1)
        then insoluble := true
        else valuation := (a, comp.(2*i) > comp.(2*i+1)) :: !valuation
    done;
    if !insoluble
    then None
    else Some (List.rev !valuation)

Sur l'exemple, resout_2sat f renvoie Some [('a', false); ('b', false); ('c', false)], qui est bien un modèle de \(f\).

Remarque

On peut tester resout_2sat contre une méthode naïve qui essaie toutes les valuations des variables : sur des milliers de formules aléatoires à au plus 6 variables, quand resout_2sat renvoie Some v, on vérifie que v satisfait la formule, et quand elle renvoie None, on vérifie qu'aucune valuation ne la satisfait.