let bool_of_int i = i = 1
let int_of_bool b = if b then 1 else 0
let negated literal = literal < 0

let valeur_literal literal values = if negated literal then 
                not (bool_of_int values.(literal)) 
        else
                bool_of_int values.(literal)

let valeur_clause clause values =
        let final_value = ref false in begin
        for i = 1 to clause.(0) do
                final_value := !final_value || (valeur_literal clause.(i) values)
        done;
        int_of_bool (!final_value)
        end

let valeur_clause_degueu c val_ = 
        (*
                une boucle while de longueur p au maximum,
                donc O(p)
        *)
        let p = c.(0) and i = ref 1 and res = ref 0 in
        while (!i <= p) && (!res = 0) do
                res := if c.(!i) > 0 then
                        val_.(c.(!i))
                else
                        1 - val_.(-c.(!i))
                ;
        incr i
        done;
        !res;;

let satisfait_formule f val_ =
        let p = f.(0).(0) and i = ref 1 and res = ref true in
        while (!i <= p) && (!res) do
                res := bool_of_int (valeur_clause f.(!i) val_);
                incr i
        done;
        !res;;

let rec resoudre_rec f v k = if k = f.(0).(1) + 1 then
        satisfait_formule f v
else begin 
        v.(k+1) <- 0;
        if resoudre_rec f v (k+1) then true else begin
                v.(k+1) <- 1;
                resoudre_rec f v (k+1)
        end;
end;;

(* let troue = true and falsse = false; *)

let resoudre f = 
        let val_ = Array.make (f.(0).(1) + 1) 0 in 
        val_.(0) <- if resoudre_rec f val_ 0 then 1 else 0; 
        val_

(*
        Soit n = F.(0).(1).
        On a au plus 2 appels récursifs pour chaque appel récursif.
        Il y a au plus n^2 appels récursifs.

        De plus, satifsait formule est linéaire. Donc la complexité est en

                O(n + n^2) = O(n^2)
*)