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 =
  failwith "A coder"
;;

let _ = creer_liste 10

(* Exercice 2 *)

type couleur = Blanc | Gris | Noir

let parcours_prof_gen g liste_som =
  failwith "A coder"
;;

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 =
  failwith "A coder"
;;

let _ = tri_topologique g2 ;;

let _ = tri_topologique g3 ;;

(* Exercice 4 *)

let composantes_connexes g =
  failwith "A coder"
;;

let _ = composantes_connexes g1 ;;

(* Exercice 5 *)

let graphe_transpose g =
  failwith "A coder"
;;

let _ = graphe_transpose g1 ;;

let _ = graphe_transpose g2 ;;

let _ = graphe_transpose g3 ;;

(* Exercice 6 *)

let kosaraju g =
  failwith "A coder"
;;

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 =
  failwith "A coder"
;;

let _ = construit_graphe 3 fsat3 ;;

let _ = construit_graphe 3 fnsat3 ;;

(* Exercice 8 *)

let est_satisfiable n f =
  failwith "A coder"
;;

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 =
  failwith "A coder"
;;

let _ = certificat 3 fsat3 ;;

let _ = certificat 3 fnsat3 ;;

let _ = certificat 5 fsat5 ;;

let _ = certificat 5 fnsat5 ;;