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 profondeur *)

(* Exercice 1 *)

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

let _ = creer_liste 10

(* Exercice 2 *)

type couleur = Blanc | Gris | Noir

let parcours_prof_gen g liste_som =
  let n = Array.length g in
  (* Initialisation des variables *)
  let color = Array.make n Blanc in
  let l_postfixe = ref [] in
  let comp = ref [] in
  let l_comp = ref [] in
  let cycle = ref false in
  (* parcours en profondeur élémentaire *)
  let rec pp u = match color.(u) with
    | Noir -> ()
    | Gris -> cycle := true
    |Blanc -> color.(u) <- Gris ;
              List.iter pp g.(u) ;
              color.(u) <- Noir ;
              comp := u::!comp ;
              l_postfixe := u::!l_postfixe
  in
  (* traitement dans l'ordre de liste_som *)
  let rec pp_principal l = match l with
    | u::q when color.(u) = Blanc -> comp := [] ;
                                     pp u ;
                                     l_comp := !comp::!l_comp ;
                                     pp_principal q
    | u::q -> pp_principal q
    | [] -> ( !cycle, !l_comp , !l_postfixe)
  in pp_principal liste_som

let _ = parcours_prof_gen g1 (creer_liste 10)

let _ = parcours_prof_gen g2 (creer_liste 9)

let _ = parcours_prof_gen g3 (creer_liste 14)

(* Exercice 3 *)

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

let _ = tri_topologique g2

let _ = tri_topologique g3

(* Exercice 4 *)

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

let _ = composantes_connexes g1

(* Exercice 5 *)

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

let graphe_transpose g =
  let n = Array.length g in
  let tg = Array.make n [] in
  for i = 0 to n-1 do
    List.iter (fun j -> tg.(j) <- i::tg.(j)) g.(i)
  done ;
  tg

let _ = graphe_transpose g1

let _ = graphe_transpose g2

let _ = graphe_transpose g3

(* Exercice 6 *)

let kosaraju g =
  let n = Array.length g in
  let (_,_,l_postfixe) = parcours_prof_gen g (creer_liste n) in
  let tg = graphe_transpose g in
  let (_,l_comp,_) = parcours_prof_gen tg l_postfixe in
  l_comp

let _ = kosaraju g1

let _ = kosaraju g2

let _ = 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 7 *)

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

let _ = construit_graphe 3 fsat3

let _ = construit_graphe 3 fnsat3

(* Exercice 8 *)

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

let _ = est_satisfiable 3 fsat3

let _ = est_satisfiable 3 fnsat3

let _ = est_satisfiable 5 fsat5

let _ = est_satisfiable 5 fnsat5


(* Exercice 9 *)

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

let _ = certificat 3 fsat3

let _ = certificat 3 fnsat3

let _ = certificat 5 fsat5

let _ = certificat 5 fnsat5