(** 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 = [] (* A FAIRE *) ;;
affiche_formule f1;;
let f2 = [] (* A FAIRE *) ;;
affiche_formule f2;;
(* Q3 *)
(* evalue une formule *)
let rec evalue f v =
failwith "A FAIRE";;
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 =
failwith "A FAIRE";;
(* Q5 *)
(* construit une valuation aletoire *)
let rec valuation_alea lv =
failwith "A FAIRE";;
(* 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 =
failwith "A FAIRE"
;;
(* tests *)
let test f k =
Printf.printf "satLV k=%d sur : " k; affiche_formule f;
match satLV f k with
| _ -> failwith "A implémenter "
;;
(* Q9 *)
(* compte le nombre de clauses satisfaites *)
let rec nb_clauses_ok f v =
failwith "A FAIRE";;
(* Q10 *)
let maxSatBacktrack f =
let maxi = ref 0 in (* nombre maximal de formules satisfaites *)
let vmaxi = ref [] in (* valuation correspondante *)
(* let rec parcours ... =
in
parcours ...; *)
(!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 *)
let rec eval_p f v =
failwith "A FAIRE";;
(* Q13 *)
let maxSatBnB f =
failwith "A FAIRE";
;;