Code : Formules logiques

Syntaxe des formules logiques¶

In [16]:

type 'a formula = 
    | T | F (* true, false *)
    | Var of 'a (* variable *)
    | Not of 'a formula
    | And of 'a formula * 'a formula
    | Or of 'a formula * 'a formula

type 'a formula = | T | F (* true, false *) | Var of 'a (* variable *) | Not of 'a formula | And of 'a formula * 'a formula | Or of 'a formula * 'a formula

Out[16]:

type 'a formula =
    T
  | F
  | Var of 'a
  | Not of 'a formula
  | And of 'a formula * 'a formula
  | Or of 'a formula * 'a formula

Substitution¶

In [17]:

let rec sub f1 x f2 = (* f1[x <- f2] *)
    match f1 with
    | T | F -> f1
    | Var y -> if y = x then f2 else f1
    | Not f3 -> Not (sub f3 x f2)
    | And(f3, f4) -> And(sub f3 x f2, sub f4 x f2)
    | Or(f3, f4) -> Or(sub f3 x f2, sub f4 x f2)

let rec sub f1 x f2 = (* f1[x <- f2] *) match f1 with | T | F -> f1 | Var y -> if y = x then f2 else f1 | Not f3 -> Not (sub f3 x f2) | And(f3, f4) -> And(sub f3 x f2, sub f4 x f2) | Or(f3, f4) -> Or(sub f3 x f2, sub f4 x f2)

Out[17]:

val sub : 'a formula -> 'a -> 'a formula -> 'a formula = <fun>

Quantificateur¶

In [18]:

let forall x f = And(sub f x T, sub f x F)
let exists x f = Or(sub f x T, sub f x F)

let forall x f = And(sub f x T, sub f x F) let exists x f = Or(sub f x T, sub f x F)

Out[18]:

val forall : 'a -> 'a formula -> 'a formula = <fun>

Out[18]:

val exists : 'a -> 'a formula -> 'a formula = <fun>

On pourrait aussi ajouter des quantificateurs à la définition des formules (remarque : on pourrait aussi ajouter l'implication) :

In [19]:

(* type 'a formula_ext = 
    | T | F (* true, false *)
    | Var of 'a (* variable *)
    | Not of 'a formula
    | And of 'a formula * 'a formula
    | Or of 'a formula * 'a formula
    | Forall of 'a * 'a formula
    | Exists of 'a * 'a formula *)

(* type 'a formula_ext = | T | F (* true, false *) | Var of 'a (* variable *) | Not of 'a formula | And of 'a formula * 'a formula | Or of 'a formula * 'a formula | Forall of 'a * 'a formula | Exists of 'a * 'a formula *)

Sémantique¶

In [21]:

let rec eval v = function
    | T -> true
    | F -> false
    | Var x -> v x
    | Not p -> not (eval v p)
    | And(p, q) -> eval v p && eval v q
    | Or(p, q) -> eval v p || eval v q

let rec eval v = function | T -> true | F -> false | Var x -> v x | Not p -> not (eval v p) | And(p, q) -> eval v p && eval v q | Or(p, q) -> eval v p || eval v q

Out[21]:

val eval : ('a -> bool) -> 'a formula -> bool = <fun>

Résolution de SAT par force brute¶

On code les valuations dans les entiers (en passant par la représentation en base 2) pour pouvoir plus facilement énumérer toutes les valuations :

In [40]:

exception Sat of (int -> bool);;

let sat f n = (* n : nombre de variables. On suppose que les variables sont des entiers entre 0 et n - 1 *)
    try for i = 0 to Int.shift_left 1 n - 1 do
        let v = fun k -> Int.logand i (Int.shift_left 1 k) != 0 in
        if eval v f then raise (Sat v)
    done;
    None
    with Sat v -> Some v

exception Sat of (int -> bool);; let sat f n = (* n : nombre de variables. On suppose que les variables sont des entiers entre 0 et n - 1 *) try for i = 0 to Int.shift_left 1 n - 1 do let v = fun k -> Int.logand i (Int.shift_left 1 k) != 0 in if eval v f then raise (Sat v) done; None with Sat v -> Some v

Out[40]:

exception Sat of (int -> bool)

Out[40]:

val sat : int formula -> int -> (int -> bool) option = <fun>

In [41]:

sat (And(Var 1, And(Or(Var 0, Not (Var 0)), Not (Var 1)))) 2;;
match sat (And(Or(Var 0, Not(Var 1)), And(Or(Not(Var 0), Var 2), Or(Var 1, Not(Var 2))))) 2 with
    | Some v -> Format.printf "%b %b@." (v 0) (v 1)
    | None -> failwith "error"

sat (And(Var 1, And(Or(Var 0, Not (Var 0)), Not (Var 1)))) 2;; match sat (And(Or(Var 0, Not(Var 1)), And(Or(Not(Var 0), Var 2), Or(Var 1, Not(Var 2))))) 2 with | Some v -> Format.printf "%b %b@." (v 0) (v 1) | None -> failwith "error"

Out[41]:

- : (int -> bool) option = None

false false

Out[41]:

- : unit = ()

Algorithme de Quine¶

In [14]:

type litteral = V of int | NV of int;;
type cnf = litteral list list;;

type litteral = V of int | NV of int;; type cnf = litteral list list;;

Out[14]:

type litteral = V of int | NV of int

Out[14]:

type cnf = litteral list list

In [15]:

let var x b = if b then V x else NV x;;

let rec subst f x b = match f with
  | [] -> Some []
  | c::q -> let c = List.filter ((<>) (var x (not b))) c in
    match subst q x b with
      | None -> None
      | Some s -> 
        if c = [] then None
        else if List.mem (var x b) c then Some s
        else Some (c::s);;

let get_var = function
  | ((V x)::_)::_ | ((NV x)::_)::_ -> x
  | _ -> failwith "get_var"

let var x b = if b then V x else NV x;; let rec subst f x b = match f with | [] -> Some [] | c::q -> let c = List.filter ((<>) (var x (not b))) c in match subst q x b with | None -> None | Some s -> if c = [] then None else if List.mem (var x b) c then Some s else Some (c::s);; let get_var = function | ((V x)::_)::_ | ((NV x)::_)::_ -> x | _ -> failwith "get_var"

Out[15]:

val var : int -> bool -> litteral = <fun>

Out[15]:

val subst : litteral list list -> int -> bool -> litteral list list option =
  <fun>

Out[15]:

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

In [16]:

let rec quine f =
  if f = [] then true
  else 
    let x = get_var f in
    List.exists (fun v -> match subst f x v with
      | Some s -> quine s
      | None -> false) [false; true];

let rec quine f = if f = [] then true else let x = get_var f in List.exists (fun v -> match subst f x v with | Some s -> quine s | None -> false) [false; true];

Out[16]:

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

In [21]:

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

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

Out[21]:

- : bool = true

Out[21]:

- : bool = true

Out[21]:

- : bool = true