(** TP  SAT FNC - MAXSAT **)

(* Type formule en FNC *)

type litt = Pos of int | Neg of int

type clause = litt list

type formule = clause list

(* Type valuation *)

type valuation = (int * bool) list

(* Affichage *)

let affiche_litt l = match l with
| Pos i -> Printf.printf "x%d" i
| Neg i -> Printf.printf "!x%d" i

let rec affiche_clause cl = match cl with
 | [] -> ()
 | [litt] -> affiche_litt litt
 | litt :: ccl -> affiche_litt litt; Printf.printf " v "; affiche_clause ccl
;;

let rec affiche_formule f = match f with 
  | [] -> Printf.printf "\n"
  | [cl] ->  Printf.printf "["; affiche_clause cl; Printf.printf "]\n"
  | cl :: ff -> Printf.printf "["; affiche_clause cl; Printf.printf "] ^ "; affiche_formule ff
;;

let affiche_valuation v =
  Printf.printf "Valuation ";
  List.iter (fun (i,b) -> if b then Printf.printf "x%d:T " i else Printf.printf "x%d:F " i) v;
  Printf.printf " \n";;
  
(* Q1 Q2 *)
let f1 = [[Pos 0; Neg 2]; [Pos 1; Pos 2]; [Neg 0; Neg 1; Pos 2]];;

affiche_formule f1;;

let f2 = [[Pos 0; Pos 1]; [Neg 0; Pos 1]; [Pos 0; Neg 1]; [Neg 0; Neg 1]];;

affiche_formule f2;;

(* Q3 *)
(* evalue un litteral *)
let rec evalueL x v = match v with
  | [] -> failwith "valeur inconnue"
  | (i,b) :: vv -> 
    if x = Pos i then b 
    else if x = Neg i then not b
    else evalueL x vv;;

(* evalue une clause *)
let rec evalueC c v = match c with
  | [] -> false
  | lit :: cc -> if evalueL lit v then true else evalueC cc v;;

(* evalue une formule *)
let rec evalue f v = match f with
  | [] -> true
  | c :: ff -> evalueC c v && evalue ff v;;

assert (evalue f1 [(0,true);(1,true);(2,true)]);;
assert (not (evalue f1 [(0,true);(1,true);(2,false)]));;
assert (not (evalue f2 [(0,false);(1,true)]));;

(* Q4 *)
(* renvoie la liste des variables présentes dans une formule (sans doublons) *)
let variables f =
  let rec dedoublonne l = match l with (* dedoublonne une liste *)
  | [] -> []
  | x :: ll -> let l2 = dedoublonne ll in if List.mem x l2 then l2 else x :: l2
  in
  let rec v_clause cl = match cl with (* liste des variables d'une clause *)
  | [] -> []
  | Pos x :: ccl | Neg x :: ccl -> x :: (v_clause ccl)
  in
  let rec v_formule f = match f with (* liste des variables d'une formule *)
  | [] -> []
  | c :: ff -> (v_clause c) @ (v_formule ff)
  in
  dedoublonne (v_formule f);;
 
(* Q5 *)
(* construit une valuation aletoire *)
let rec valuation_alea lv = 
  List.map (fun x -> if Random.int 2 = 0 then (x,false) else (x,true)) lv;;

(* Q6 *)
let small_formula = [[Pos 0;Pos 7;Pos 6];[Neg 7;Neg 9];[Neg 1;Pos 2;Neg 4];[Pos 7;Neg 8];[Pos 8;Neg 4;Neg 1];[Pos 3;Neg 9;Pos 5];[Pos 9;Pos 5];[Neg 3;Neg 9;Neg 2];
                      [Neg 5;Pos 2;Neg 7];[Neg 7;Pos 8;Pos 5];[Neg 3;Pos 4;Neg 8];[Neg 5;Pos 0;Neg 2];[Neg 0;Neg 7;Pos 1];[Neg 6;Pos 3;Pos 7];[Neg 1;Neg 0;Pos 3]];;

let satLV f k  =
  let lv = variables f in (* liste des variables de la fnc *)
  let v = ref None in (* resultat *)
  for i = 0 to k-1 do
    let va = valuation_alea lv in (* on choisit une valuation aleatoire *)
    if evalue f va then v := Some va
  done;
  (* peu efficace, on pourrait utiliser une boucle while ou une exception *)
  !v
;;

(* tests *)
let test f k =
  Printf.printf "satLV k=%d sur : " k; affiche_formule f;
  match satLV f k with
| None -> Printf.printf " : pas trouvé\n"
| Some v -> Printf.printf " : trouvé ! "; affiche_valuation v
;;

test f1 1;;
test f1 2;;
test f1 3;;
test f2 3;;
test f2 10;; (* f2 n'est pas satisfiable *)
test small_formula 2;;
test small_formula 5;;
test small_formula 10;;


(* Q9 *)
(* compte le nombre de clauses satisfaites *)
let rec nb_clauses_ok f v = match f with
  | [] -> 0
  | c :: ff -> (if evalueC c v then 1 else 0) + nb_clauses_ok ff v;;
  
  
(* Q10 *)
let maxSatBacktrack f =
  let maxi = ref 0 in (* nombre maximal de formules satisfaites *)
  let vmaxi = ref [] in (* valuation correspondante *)

  let rec parcours v lv =
    (* v : valuation partielle
       lv : liste de variables sans valeur *)
    match lv with 
    | [] -> (* fin de la branche d'exploration *)
      let ns = nb_clauses_ok f v in
      if ns > !maxi then begin 
        maxi := ns; vmaxi := v; (* Printf.printf "c'est mieux : %d\n" !maxi *)
      end
    | i :: llv -> begin
      (* tester xi = true *)
      parcours ((i,true) :: v) llv;
      (* tester xi = false *)
      parcours ((i,false) :: v) llv;
    end
  in
  parcours [] (variables f); 

  (!maxi, !vmaxi)
;;

let medium_formula = [[Pos 0;Pos 7;Pos 6];[Neg 7;Neg 9];[Neg 1;Pos 2;Neg 4];[Pos 7;Neg 8];[Pos 8;Neg 4;Neg 1];[Pos 3;Neg 9;Pos 5];[Pos 9;Pos 5];[Neg 3;Neg 9;Neg 2];
                      [Neg 5;Pos 2;Neg 7];[Neg 7;Pos 8;Pos 5];[Neg 3;Pos 4;Neg 8];[Neg 5;Pos 0;Neg 2];[Neg 0;Neg 7;Pos 1];[Neg 6;Pos 3;Pos 7];[Neg 1;Neg 0;Pos 3];
                      [Neg 4;Pos 2];[Neg 7;Neg 5];[Neg 1;Pos 4];[Neg 0;Pos 1];[Neg 3;Pos 1]];; (* 20 clauses *)

let big_formula = [[Neg 6;Pos 3;];[Neg 12;Pos 9;];[Neg 14;Neg 4;];[Pos 11;Neg 7;];[Neg 2;Pos 3;];[Pos 13;Neg 1;];[Neg 3;Neg 11;];[Neg 3;Pos 12;];
  [Neg 8;Pos 5;];[Pos 2;Neg 5;];[Pos 8;Neg 2;];[Neg 2;Pos 12;];[Neg 6;Pos 5;];[Neg 14;Neg 8;];[Neg 7;Pos 0;];[Pos 12;Neg 1;];[Pos 11;];[Pos 0;Neg 7;];
  [Neg 5;Pos 7;];[Pos 11;Pos 13;];[Neg 14;Pos 10;];[Neg 1;Neg 2;];[Neg 13;Neg 12;];[Neg 3;Neg 10;];[Neg 2;Pos 6;];[Pos 7;Pos 9;];[Pos 0;Neg 6;];
  [Neg 1;Neg 2;];[Pos 8;Pos 7;];[Neg 4;Pos 11;];[Neg 13;Pos 7;];[Neg 11;Pos 12;];[Neg 6;Neg 2;];[Pos 4;Pos 2;];[Pos 6;Pos 3;];[Neg 6;Neg 8;];
  [Neg 6;Neg 12;];[Pos 3;Neg 7;];[Neg 0;Pos 11;];[Neg 4;];[Pos 13;Pos 12;];[Pos 10;Pos 0;];[Neg 9;Pos 6;];[Pos 3;Pos 6;];[Pos 4;Pos 11;];
  [Neg 11;Pos 5;];[Neg 9;];[Pos 7;Neg 1;];[Neg 4;Neg 2;]];; (* 49 clauses *)

let very_big_formula = [[Neg 11; Neg 18; Neg 1]; [Neg 29; Neg 11; Pos 13]; (* 94 clauses *)
  [Pos 16; Pos 2; Neg 24]; [Pos 13; Neg 18];
  [Neg 6; Pos 17; Neg 23]; [Neg 0; Pos 10];
  [Neg 28; Pos 26; Pos 15]; [Pos 0; Neg 21; Pos 23];
  [Neg 1; Neg 23; Pos 11]; [Pos 2; Pos 19]; [Neg 2; Pos 25; Neg 19];
  [Pos 14; Neg 7; Pos 17]; [Pos 26; Neg 6]; [Neg 25; Pos 29; Pos 22];
  [Pos 8; Pos 5; Pos 4]; [Pos 6; Neg 11; Neg 10]; [Neg 9; Pos 22; Pos 24];
  [Neg 19; Neg 6; Neg 25]; [Neg 14; Neg 29; Neg 21];
  [Pos 25; Neg 28]; [Neg 12; Pos 17]; [Neg 14; Neg 23; Neg 19];
  [Pos 22; Neg 5; Pos 6]; [Neg 7; Pos 11; Neg 16]; [Pos 8; Neg 13; Pos 21];
  [Neg 26; Neg 21; Neg 11]; [Pos 24; Neg 6; Pos 0]; [Neg 17; Pos 1; Neg 28];
  [Neg 11; Pos 22; Pos 3]; [Neg 5; Pos 19]; [Neg 7; Pos 2; Neg 16];
  [Neg 6; Pos 17; Pos 16]; [Pos 24; Neg 5; Neg 14];
  [Neg 13; Neg 25; Neg 15]; [Neg 1; Neg 12; Pos 15]; [Neg 8; Pos 9];
  [Neg 21; Pos 14; Neg 6]; [Pos 21; Pos 16; Pos 2]; [Neg 9; Neg 28; Pos 23];
  [Neg 29; Pos 9; Pos 16]; [Neg 2; Neg 14]; [Neg 22; Neg 16; Neg 4];
  [Neg 19; Neg 17; Neg 24]; [Neg 4; Neg 1; Pos 25];[Pos 18; Neg 13];
  [Pos 16; Pos 23]; [Pos 26]; [Pos 23; Neg 17];
  [Pos 18; Neg 26]; [Pos 14; Neg 11]; [Pos 24; Neg 26]; [Pos 25; Neg 22];
  [Neg 0; Neg 26]; [Pos 27; Pos 0]; [Pos 25; Pos 23]; [Neg 16; Neg 19];
  [Pos 19; Pos 5]; [Neg 22; Neg 5]; [Pos 1; Pos 22]; [Neg 11; Neg 22];
  [Pos 19; Pos 10]; [Pos 25; Neg 29]; [Pos 4]; [Neg 10; Neg 19];
  [Neg 0; Neg 25]; [Pos 3; Neg 2]; [Pos 26; Pos 0]; [Neg 20; Neg 9];
  [Pos 1; Pos 17]; [Neg 12; Pos 24]; [Neg 28; Neg 4]; [Pos 4; Pos 25];
  [Neg 19; Neg 18]; [Pos 21; Neg 20]; [Neg 21; Neg 3]; [Pos 28; Pos 16];
  [Neg 8; Neg 7]; [Neg 13; Neg 9]; [Neg 26; Pos 29]; [Neg 15; Pos 25];
  [Neg 17; Neg 1]; [Pos 9; Neg 10]; [Neg 2; Pos 3]; [Neg 27; Pos 1];
  [Pos 0; Pos 26]; [Pos 23; Pos 26]; [Pos 3; Neg 20]; [Pos 22; Neg 8];
  [Neg 10; Neg 0]; [Neg 22; Neg 20]; [Neg 7; Neg 10]; [Neg 9; Pos 24];
  [Pos 19; Neg 22]; [Pos 24; Pos 6]];;


let n,v = maxSatBacktrack small_formula in Printf.printf "small_formula : %d clauses satisfiables au plus\n" n; affiche_valuation v ;;

let n,v = maxSatBacktrack medium_formula in Printf.printf "medium_formula : %d clauses satisfiables au plus\n" n; affiche_valuation v ;;

let n,v = maxSatBacktrack big_formula in Printf.printf "big_formula : %d clauses satisfiables au plus\n" n; affiche_valuation v;;

(* let n,v = maxSatBacktrack very_big_formula in Printf.printf "very_big_formula : %d clauses satisfiables au plus\n" n; affiche_valuation v;; *)

(* Q11 *)

(* evalue une variable booléenne : true->1 / false->-1 / ?->0 *)
let rec eval_pV x v = match v with
  | [] -> 0
  | (i,b) :: vv -> if x = i then begin 
      if b then 1 else -1 end 
      else eval_pV x vv;;

(* evalue une clause : (ns, np, nn) *)
let rec eval_pC c v = match c with
  | [] -> (0,0,1)
  | Pos i :: cc -> begin match eval_pV i v with
    | 1 -> (1,0,0)
    | 0 -> let (s,p,n) = eval_pC cc v in if s = 1 then (1,0,0) else (0,1,0)
    | -1 ->  eval_pC cc v
    | _ -> failwith "impossible" end
  | Neg i :: cc -> begin match eval_pV i v with
    | -1 -> (1,0,0)
    | 0 ->  let (s,p,n) = eval_pC cc v in if s = 1 then (1,0,0) else (0,1,0)
    | 1 ->  eval_pC cc v
    | _ -> failwith "impossible" end;;

let rec eval_p f v = 
  (* evalue une liste de clauses avec un valuation partielle. Calcule 
     ns : nombre de clauses satisfaites, 
     np : nombre de clauses peut-être satisfiables
     nn : nombre de clauses non satisfiables *)
     match f with
     | [] -> (0, 0, 0)
     | c :: ff -> let (ns, np, nn) = eval_pC c v in 
        let (ns2, np2, nn2) = eval_p ff v in 
        (ns+ ns2, np + np2, nn + nn2);;
       
(* Q13 *)
let maxSatBnB f =
  let maxi = ref 0 in (* nombre maximal de formules satisfaites *)
  let vmaxi = ref [] in (* valuation correspondante *)

  let rec parcours v lv =
    (* v : valuation partielle
       lv : liste de variables sans valeur *)
    let (ns, np, nn) = eval_p f v  in
    (* ns : nombre de clauses satisfaites, 
       np : nombre de clauses possiblement satisfaites,
       nn : nombre de clauses non satisfaites *)
    if (ns + np > !maxi) then begin
      match lv with 
      | [] -> (* fin de la branche d'exploration *)
        if ns > !maxi then begin 
          maxi := ns; vmaxi := v; (* Printf.printf "c'est mieux : %d\n" !maxi *)
        end
      | i :: llv -> begin
        (* tester xi = true *)
        parcours ((i,true) :: v) llv;
        (* tester xi = false *)
        parcours ((i,false) :: v) llv;
      end
    end
  in
  parcours [] (variables f); 
  (!maxi, !vmaxi);;


let n,v = maxSatBnB medium_formula in Printf.printf "medium_formula BnB : %d clauses satisfiables au plus\n" n; affiche_valuation v;;

let n,v = maxSatBnB big_formula in Printf.printf "big_formula BnB : %d clauses satisfiables au plus\n" n; affiche_valuation v;;

(* let n,v = maxSatBnB very_big_formula in Printf.printf "very_big_formula BnB : %d clauses satisfiables au plus\n" n; affiche_valuation v;; *)


(* Q16 *)
let maxSat_approx f =
  let lv = variables f in (* liste des variables *)
  let v = valuation_alea lv in (* valuation aleatoire *)
  nb_clauses_ok f v
;;

Printf.printf "maxSat_approx big_formula : %d\n" (maxSat_approx big_formula);;

Printf.printf "maxSat_approx very_big_formula : %d\n" (maxSat_approx very_big_formula);;