let g1 = [| [2]; [5; 9]; [0; 6; 7]; []; [6; 8]; [1]; [2; 4; 7; 8]; [2; 6]; [4; 6]; [1] |] ;;

let g2 = [| []; [0]; []; []; [3; 8]; [1; 8]; [3]; [4]; [0] |];;

let g3 = [| [1]; [5; 6]; [8]; [0; 4]; [3; 9]; [1; 6; 10; 11]; [5]; [8]; [2]; []; [5];
            [6; 7; 12]; [13]; [12] |];;

(* Parcours en largeur *)

(* Exercice 1 *)

let parcours_largeur g s =
  let a_traiter = Queue.create () in
  let n = Array.length g in
  let deja_traites = Array.make n false in
  let pred = Array.make n (-1) in
  let dist = Array.make n (-1) in
  deja_traites.(s) <- true ;
  Queue.push s a_traiter ;
  pred.(s) <- s ;
  dist.(s) <- 0 ;
  while not (Queue.is_empty a_traiter) do
    let s = Queue.pop a_traiter in
    let rec aux l_voisins = match l_voisins with
      | [] -> ()
      | t::q when deja_traites.(t) -> aux q
      | t::q -> Queue.push t a_traiter ;
        deja_traites.(t) <- true ;
        dist.(t) <- dist.(s) + 1 ;
        pred.(t) <- s ;
        aux q
    in aux g.(s)
  done ;
  dist, pred
;;

parcours_largeur g1 0 ;;

parcours_largeur g2 7 ;;

parcours_largeur g2 0 ;;

(* Exercice 2 *)

let pcc g s x =
  let _, pred = parcours_largeur g s in
  let rec remonte l t = match pred.(t) with
    | -1 -> failwith "x non accessible !"
    | _ when t = s -> s::l
    | t' -> remonte (t::l) t'
  in remonte [] x
;;

pcc g1 0 4 ;;

pcc g2 0 1 ;;

pcc g3 0 13 ;;

(* Parcours en profondeur *)

(* Exercice 3 *)

let creer_liste n =
  let rec aux k = match k<n with
    | false -> []
    | true -> k::aux (k+1)
  in aux 0
;;

creer_liste 10 ;;

(* Exercice 4 *)

type couleur = Blanc | Gris | Noir ;;

let parcours_prof_gen g liste_som =
  let n = Array.length g in
  let color = Array.make n Blanc in
  let enum_glob = ref [] in
  let enum = ref [] in
  let enums = ref [] in
  let gris_encore = ref false in
  let rec pp u =
    color.(u) <- Gris ;
    let rec aux q = match q with
      | [] -> color.(u) <- Noir ;
              enum := u::!enum ;
              enum_glob := u::!enum_glob
      | v::p when color.(v) = Gris -> gris_encore := true ; aux p
      | v::p when color.(v) = Blanc -> pp v ; aux p
      | v::p -> aux p
    in aux g.(u)
  in
  let rec pp_principal q = match q with
    | [] -> ( !gris_encore, !enums , !enum_glob)
    | u::p when color.(u) = Blanc -> enum := [] ;
                                     pp u ;
                                     enums := !enum::!enums ;
                                     pp_principal p
    | u::p -> pp_principal p
  in pp_principal liste_som
;;

parcours_prof_gen g1 (creer_liste 10) ;;

parcours_prof_gen g2 (creer_liste 9) ;;

parcours_prof_gen g3 (creer_liste 14) ;;

(* Exercice 5 *)

let tri_topologique g =
  let n = Array.length g in
  let (b, _, p) = parcours_prof_gen g (creer_liste n) in
  if not b then p
  else failwith "Il y a un cycle"
;;

tri_topologique g2 ;;

tri_topologique g3 ;;

(* Exercice 6 *)

let composantes_connexes g =
  let n = Array.length g in
  let (_, l, _) = parcours_prof_gen g (creer_liste n) in
  l
;;

composantes_connexes g1 ;;

(* Exercice 7 *)

let graphe_transpose g =
  let n = Array.length g in
  let tg = Array.make n [] in
  let rec aux l i = match l with
    | [] -> ()
    | j::q -> tg.(j) <- i::tg.(j) ; aux q i
  in
  for i=0 to n-1 do
    aux g.(i) i
  done ;
  tg
;;

graphe_transpose g1 ;;

graphe_transpose g2 ;;

graphe_transpose g3 ;;

(* Exercice 8 *)

let kosaraju g =
  let n = Array.length g in
  let (_,_,p) = parcours_prof_gen g (creer_liste n) in
  let tg = graphe_transpose g in
  let (_,l,_) = parcours_prof_gen tg p in
  l
;;

kosaraju g1 ;;

kosaraju g2 ;;

kosaraju g3 ;;

(* Application a 2-SAT *)

type litteral = X of int | Xb of int ;;

type clause2 = litteral * litteral ;;

type formule2sat = clause2 list ;;

(* une formule a 3 variables satisfiable *)
let fsat3 = [(Xb 0, X 1); (X 1, X 2); (Xb 1, Xb 2); (X 0, X 2); (X 0, Xb 2)] ;;

(* une formule a 3 variables non satisfiable *)
let fnsat3 = [(X 0, X 1); (Xb 0, X 2); (X 0, Xb 1); (Xb 1, X 2); (Xb 0, Xb 2)] ;;

(* une formule a 5 variables satisfiable *)
let fsat5 = [(X 2, X 4); (X 1, Xb 2); (X 0, Xb 3); (X 2, X 3); (Xb 3, X 4); (Xb 1, Xb 2); (X 1, X 4); (Xb 0, Xb 2); (Xb 0, X 3); (X 1, X 2); (X 1, X 3); (Xb 2, X 4); (X 0, Xb 4); (X 1, Xb 3); (Xb 1, X 3)] ;;

(* une formule a 5 variables non satisfiable *)
let fnsat5 = [(Xb 2, X 4); (X 1, Xb 2); (Xb 3, Xb 4); (Xb 0, Xb 3); (Xb 0, X 1); (Xb 1, Xb 4); (Xb 0, Xb 1); (Xb 1, X 3); (Xb 1, X 4); (Xb 2, Xb 3); (X 1, X 4); (X 3, Xb 4); (X 0, X 1); (Xb 0, Xb 4); (Xb 2, Xb 4)] ;;

(* Exercice 9 *)

let construit_graphe n f =
  let g = Array.make (2*n) [] in
  let ajout_arc i j = g.(i) <- j::g.(i) in
  let arcs c = match c with
    | X i, X j -> ajout_arc (n+i) j ; ajout_arc (n+j) i
    | X i, Xb j -> ajout_arc (n+i) (n+j) ; ajout_arc j i
    | Xb i, X j -> ajout_arc i j ; ajout_arc (n+j) (n+i)
    | Xb i, Xb j -> ajout_arc i (n+j) ; ajout_arc j (n+i)
  in
  let rec parcours l = match l with
    | [] -> ()
    | c::q -> arcs c ; parcours q
  in
  parcours f ;
  g
;;

construit_graphe 3 fsat3 ;;

construit_graphe 3 fnsat3 ;;

(* Exercice 10 *)

let est_satisfiable n f =
  let g = construit_graphe n f in
  let c = kosaraju g in
  let rec check l = match l with
    | [] -> true
    | t::q when t<n && List.mem (t+n) q -> false
    | t::q when t>=n && List.mem (t-n) q -> false
    | _::q -> check q
  in
  let rec aux lc = match lc with
    | [] -> true
    | l::qc -> check l && aux qc
  in aux c
;;

est_satisfiable 3 fsat3 ;;

est_satisfiable 3 fnsat3 ;;

est_satisfiable 5 fsat5 ;;

est_satisfiable 5 fnsat5 ;;


(* Exercice 11 *)

let certificat n f = match est_satisfiable n f with
  | false -> failwith "non satisfiable"
  |true ->
    let g = construit_graphe n f in
    let c = kosaraju g in
    let v = Array.make n (-1) in
    let rec aux l = match l with 
      | [] -> ()
      | i::q when i<n && v.(i) = -1 -> v.(i) <- 1 ; aux q
      | i::q when i>=n && v.(i-n) = -1 -> v.(i-n) <- 0 ; aux q
      | _::q -> aux q
    in
    let rec aux' lc = match lc with
      | [] -> ()
      | l::qc -> aux l ; aux' qc
    in
    aux' c ;
    v
;;

certificat 3 fsat3 ;;

certificat 3 fnsat3 ;;

certificat 5 fsat5 ;;

certificat 5 fnsat5 ;;