X-ENS 2016 (Problème SAT) : Corrigé

Préliminaires¶

In [1]:

type litteral =
|V of int (* variable *)
|NV of int;; (* negation de variable *)
type clause = litteral list;;
type fnc = clause list;;

type litteral = |V of int (* variable *) |NV of int;; (* negation de variable *) type clause = litteral list;; type fnc = clause list;;

Out[1]:

type litteral = V of int | NV of int

Out[1]:

type clause = litteral list

Out[1]:

type fnc = clause list

In [2]:

let rec max_clause = function
    | [] -> min_int
    | (V x)::q' | (NV x)::q' -> max x (max_clause q');;

let rec var_max f = match f with
    | [] -> min_int
    | c::q -> max (max_clause c) (var_max q)

let rec max_clause = function | [] -> min_int | (V x)::q' | (NV x)::q' -> max x (max_clause q');; let rec var_max f = match f with | [] -> min_int | c::q -> max (max_clause c) (var_max q)

Out[2]:

val max_clause : litteral list -> int = <fun>

Out[2]:

val var_max : litteral list list -> int = <fun>

In [3]:

type trileen = Vrai|Faux|Indetermine;;

type trileen = Vrai|Faux|Indetermine;;

Out[3]:

type trileen = Vrai | Faux | Indetermine

Partie I. Résolution de 1-SAT¶

In [4]:

let un_sat f =
    let t = Array.make (1 + var_max f) Indetermine in
    let rec aux = function
        | [] -> true
        | [V x]::q -> if t.(x) = Faux then false else (t.(x) <- Vrai; aux q)
        | [NV x]::q -> if t.(x) = Vrai then false else (t.(x) <- Faux; aux q)
        | _ -> failwith "not 1SAT" in
    aux f

let un_sat f = let t = Array.make (1 + var_max f) Indetermine in let rec aux = function | [] -> true | [V x]::q -> if t.(x) = Faux then false else (t.(x) <- Vrai; aux q) | [NV x]::q -> if t.(x) = Vrai then false else (t.(x) <- Faux; aux q) | _ -> failwith "not 1SAT" in aux f

Out[4]:

val un_sat : litteral list list -> bool = <fun>

In [5]:

let f = [[V 0]; [NV 1]; [NV 1]] in
un_sat f

let f = [[V 0]; [NV 1]; [NV 1]] in un_sat f

Out[5]:

- : bool = true

Partie II. Résolution de 2-SAT¶

In [6]:

let dfs_tri g =
    let deja_vu = Array.make (Array.length g) false in
    let resultat = ref [] in
    let rec dfs_rec i =
        if not deja_vu.(i) then (
            deja_vu.(i) <- true;
        List.iter dfs_rec g.(i); (* voir page 2 pour la d´efinition de do list *)
        resultat := i :: !resultat;
        ) in
    for i = 0 to Array.length g - 1 do dfs_rec i done;
    !resultat;;

let dfs_tri g = let deja_vu = Array.make (Array.length g) false in let resultat = ref [] in let rec dfs_rec i = if not deja_vu.(i) then ( deja_vu.(i) <- true; List.iter dfs_rec g.(i); (* voir page 2 pour la d´efinition de do list *) resultat := i :: !resultat; ) in for i = 0 to Array.length g - 1 do dfs_rec i done; !resultat;;

Out[6]:

val dfs_tri : int list array -> int list = <fun>

In [7]:

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

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

Out[7]:

val renverser : int list array -> int list array = <fun>

In [8]:

(* 6 *)
let dfs_cfc g l = 
    let deja_vu = Array.make (Array.length g) false in
    let dfs g v =
        let resultat = ref [] in
        let rec dfs_rec i =
            if not deja_vu.(i) then (
                deja_vu.(i) <- true;
            List.iter dfs_rec g.(i); (* voir page 2 pour la d´efinition de do list *)
            resultat := i :: !resultat;
            ) in
        dfs_rec v;
        !resultat in
    List.map (dfs g) l
    |> List.filter ((<>) [])

(* 6 *) let dfs_cfc g l = let deja_vu = Array.make (Array.length g) false in let dfs g v = let resultat = ref [] in let rec dfs_rec i = if not deja_vu.(i) then ( deja_vu.(i) <- true; List.iter dfs_rec g.(i); (* voir page 2 pour la d´efinition de do list *) resultat := i :: !resultat; ) in dfs_rec v; !resultat in List.map (dfs g) l |> List.filter ((<>) [])

Out[8]:

val dfs_cfc : int list array -> int list -> int list list = <fun>

In [9]:

let g = [|[]; [4; 3]; [3]; [2; 0]; [0; 1]; [2; 7]; [5; 1; 2]; [6]|]

let g = [|[]; [4; 3]; [3]; [2; 0]; [0; 1]; [2; 7]; [5; 1; 2]; [6]|]

Out[9]:

val g : int list array =
  [|[]; [4; 3]; [3]; [2; 0]; [0; 1]; [2; 7]; [5; 1; 2]; [6]|]

In [10]:

let cfc g =
    let l = dfs_tri g in
    let g' = renverser g in
    dfs_cfc g' l

let cfc g = let l = dfs_tri g in let g' = renverser g in dfs_cfc g' l

Out[10]:

val cfc : int list array -> int list list = <fun>

In [11]:

cfc g

cfc g

Out[11]:

- : int list list = [[5; 6; 7]; [1; 4]; [3; 2]; [0]]

In [17]:

(* Q 12 *)
let f = [[V 1; V 2]; [V 0]; [V 2; NV 2]; [NV 2; V 0]]

(* Q 12 *) let f = [[V 1; V 2]; [V 0]; [V 2; NV 2]; [NV 2; V 0]]

Out[17]:

val f : litteral list list = [[V 1; V 2]; [V 0]; [V 2; NV 2]; [NV 2; V 0]]

In [18]:

(* Q13 *)
let sat_vers_graphe f =
    let m = var_max f in
    let g = Array.make (2*(m + 1)) [] in
    let add i e = g.(i) <- e::g.(i) in
    let rec aux = function
        | [] -> g
        | [V i]::q -> add (2*i + 1) (2*i); aux q
        | [NV i]::q -> add (2*i) (2*i + 1); aux q
        | [V i; V j]::q -> add (2*i + 1) (2*j); add (2*j + 1) (2*i); aux q
        | [NV i; NV j]::q -> add (2*i) (2*j + 1); add (2*j) (2*i + 1); aux q
        | [V i; NV j]::q when i = j -> aux q
        | [V i; NV j]::q -> add (2*i + 1) (2*j + 1); add (2*j) (2*i); aux q
        | [a; b]::q -> aux ([b; a]::q)
        | _::q -> aux q in
    aux f

(* Q13 *) let sat_vers_graphe f = let m = var_max f in let g = Array.make (2*(m + 1)) [] in let add i e = g.(i) <- e::g.(i) in let rec aux = function | [] -> g | [V i]::q -> add (2*i + 1) (2*i); aux q | [NV i]::q -> add (2*i) (2*i + 1); aux q | [V i; V j]::q -> add (2*i + 1) (2*j); add (2*j + 1) (2*i); aux q | [NV i; NV j]::q -> add (2*i) (2*j + 1); add (2*j) (2*i + 1); aux q | [V i; NV j]::q when i = j -> aux q | [V i; NV j]::q -> add (2*i + 1) (2*j + 1); add (2*j) (2*i); aux q | [a; b]::q -> aux ([b; a]::q) | _::q -> aux q in aux f

Out[18]:

val sat_vers_graphe : litteral list list -> int list array = <fun>

In [19]:

sat_vers_graphe f

sat_vers_graphe f

Out[19]:

- : int list array = [|[]; [5; 0]; []; [4]; [0]; [2]|]

In [20]:

let deux_sat f =
    let t = Array.make (Array.length g /2) 0 in (* t.(i) = xi ou not xi déjà vu *) 
    let rec aux i cc = match cc with
        | [] -> true
        | c::q -> let rec aux2 = function 
            | [] -> true
            | v::q -> if t.(v / 2) = i then false
                else (t.(v/2) <- i; aux2 q) in
            (aux2 c) && aux (i + 1) q in
    f |> sat_vers_graphe |> cfc |> aux 1

let deux_sat f = let t = Array.make (Array.length g /2) 0 in (* t.(i) = xi ou not xi déjà vu *) let rec aux i cc = match cc with | [] -> true | c::q -> let rec aux2 = function | [] -> true | v::q -> if t.(v / 2) = i then false else (t.(v/2) <- i; aux2 q) in (aux2 c) && aux (i + 1) q in f |> sat_vers_graphe |> cfc |> aux 1

Out[20]:

val deux_sat : litteral list list -> bool = <fun>

In [21]:

let f2 = [[V 1; V 2]; [V 0]; [V 2; NV 2]; [NV 2; V 0]; [NV 0]]

let f2 = [[V 1; V 2]; [V 0]; [V 2; NV 2]; [NV 2; V 0]; [NV 0]]

Out[21]:

val f2 : litteral list list =
  [[V 1; V 2]; [V 0]; [V 2; NV 2]; [NV 2; V 0]; [NV 0]]

In [22]:

deux_sat f2

deux_sat f2

Out[22]:

- : bool = false

Partie III. Résolution de k-SAT pour k arbitraire¶

In [23]:

type trileen =
|Vrai
|Faux
|Indetermine;;

type trileen = |Vrai |Faux |Indetermine;;

Out[23]:

type trileen = Vrai | Faux | Indetermine

In [24]:

let et f g = match f, g with
    | Vrai, Vrai -> Vrai
    | Faux, _ | _, Faux -> Faux
    | _ -> Indetermine;;
let non = function
    | Vrai -> Faux
    | Faux -> Vrai
    | Indetermine -> Indetermine;;
let ou f g = match f, g with
    | Vrai, _ | _, Vrai -> Vrai
    | Faux, Faux -> Faux
    | _ -> Indetermine

let et f g = match f, g with | Vrai, Vrai -> Vrai | Faux, _ | _, Faux -> Faux | _ -> Indetermine;; let non = function | Vrai -> Faux | Faux -> Vrai | Indetermine -> Indetermine;; let ou f g = match f, g with | Vrai, _ | _, Vrai -> Vrai | Faux, Faux -> Faux | _ -> Indetermine

Out[24]:

val et : trileen -> trileen -> trileen = <fun>

Out[24]:

val non : trileen -> trileen = <fun>

Out[24]:

val ou : trileen -> trileen -> trileen = <fun>

In [25]:

let rec eval_clause v = function
    | [] -> Faux
    | (V x)::q -> ou v.(x) (eval_clause v q)
    | (NV x)::q -> ou (non v.(x)) (eval_clause v q);;
    
let rec eval f v = match f with
    | [] -> Vrai
    | c::q -> et (eval_clause v c) (eval q v)

let rec eval_clause v = function | [] -> Faux | (V x)::q -> ou v.(x) (eval_clause v q) | (NV x)::q -> ou (non v.(x)) (eval_clause v q);; let rec eval f v = match f with | [] -> Vrai | c::q -> et (eval_clause v c) (eval q v)

Out[25]:

val eval_clause : trileen array -> litteral list -> trileen = <fun>

Out[25]:

val eval : litteral list list -> trileen array -> trileen = <fun>

In [30]:

let k_sat f =
  let t = Array.make (1 + var_max f) Indetermine in
  let rec aux i =
    if i > List.length f then true
    else match eval f t with
      | Vrai -> true
      | Faux -> false
      | Indetermine -> (t.(i) <- Vrai; aux (i + 1)) || (t.(i) <- Faux; aux (i + 1)) in
  aux 0

let k_sat f = let t = Array.make (1 + var_max f) Indetermine in let rec aux i = if i > List.length f then true else match eval f t with | Vrai -> true | Faux -> false | Indetermine -> (t.(i) <- Vrai; aux (i + 1)) || (t.(i) <- Faux; aux (i + 1)) in aux 0

Out[30]:

val k_sat : litteral list list -> bool = <fun>

In [33]:

not (k_sat [[V 0]; [NV 1]; [V 1]]);;
k_sat [[V 0; NV 1; V 0]; [NV 0]; [V 1; V 2]];;

not (k_sat [[V 0]; [NV 1]; [V 1]]);; k_sat [[V 0; NV 1; V 0]; [NV 0]; [V 1; V 2]];;

Out[33]:

- : bool = true

Out[33]:

- : bool = true