Boolean

A1

Write a data-type boolean that defines the boolean formulae:

type boolean = 
  | True 
  | False
  | Var of int
  | Not of boolean
  | And of (boolean*boolean)
  | Or of (boolean*boolean)
  | Impl of (boolean*boolean)
  | Equiv of (boolean*boolean)

With this type, (x∧y)⇒x is written Impl(And(Var 0, Var 1),Var 0).

A2

Write a function string_of_boolean that transforms a boolean formula into a string.

let rec string_of_boolean f = 
  let comp v f1 f2 = (string_of_boolean f1)^v^(string_of_boolean f2) in
  let par f1 = "("^f1^")" in match f with 
    True -> "True"
  | False-> "False"
  | Var i -> "x"^(string_of_int i)
  | Not f1 -> "~"^(par (string_of_boolean f1))
  | And (f1,f2) -> par (comp "/\\" f1 f2)
  | Or (f1,f2) -> par (comp "\\/" f1 f2)
  | Impl (f1,f2) -> par (comp "->" f1 f2)
  | Equiv (f1,f2) -> par (comp "<->" f1 f2)

string_of_boolean (Impl(And(Var 0, Var 1),Var 0)) vale "((x0/\\x1)->x0)".

A3

Write a function eval that takes a formula and an evaluation of its variables and returns the value of the formula for the given evaluation.
The evaluation is implemented as a list. The value of the variable n is the n-th element of the list:

let rec eval and f = match f with
  True -> true
| False -> false
| Var i -> List.nth and i
| Not f1 -> not (eval and f1)
| And (f1,f2) -> (eval and f1) && (eval and f2)
| Or (f1,f2) ->  (eval and f1) || (eval and f2)
| Impl (f1,f2) -> (eval and f2) || (not (eval and f1))
| Equiv (f1,f2) -> (eval and f1)=(eval and f2)

For example,

eval [true;false;true] 
         (Impl (Or (And (Var 0,Var 1), Var 2), 
                Impl (Var 2,And (Var 0, Var 1))))

is evaluated to false.

A4

Write a function table that takes a formula and prints out its truth table.

To produce the table, first we need to know the number of variables:

let rec maxI f = match f with
     True -> 0
   | False -> 0
   | Var i -> i
   | Not f1 -> (maxI f1)
   | And (f1,f2) -> max (maxI f1) (maxI f2)
   | Or (f1,f2) -> max (maxI f1) (maxI f2)
   | Impl (f1,f2) -> max (maxI f1) (maxI f2)
   | Equiv (f1,f2) -> max (maxI f1) (maxI f2)

Now

let table f = 
  let n = maxI f in
  (* Compute the number of digits of  k *)
  let rec digit k = if k < 10 then 1 else 1+digit (k/10) in
  (* Length of a box *)
  let size = max 5 ((digit n)+1)  in
  (* A bool as a string *)
  let string_of_bool b = if b then " true" else "false" in
  (* Indentation for boolean values *)
  let indent = (String.make (size-5) ' ')^"|" in
  (* Generation of the table *)
  let rec gen and k = match k with
    0 ->
      begin
        List.iter (fun x -> print_string (string_of_bool x); print_string indent) e;
        print_string (string_of_bool (eval and f)); print_newline();
      end
  | _ -> gen (false::e) (k-1);gen (true::e) (k-1) in
  (* Separator *)
  let sep = String.make ((n+2)*(size+1)) '-' in
  (* Sep *)
  print_string sep; print_newline();
  (* First line *)
  for i=0 to n do
    print_string (String.make (max 0 (size-((digit i)+1))) ' ');
    print_string "x"; print_int i; print_string "|";
  done;
  print_string (string_of_boolean f); print_newline();
  (* Sep *)
  print_string sep; print_newline();
  (* Table *)
  gen [] (n+1);
  (* Sep *)
  print_string sep; print_newline()

With table (And (Var 0, Var 1)) we have:

------------------
   x0|   x1|(x0/\x1)
------------------
false|false|false
 true|false|false
false| true|false
 true| true| true
------------------

A5

Write a function sat that verifies if a formula is satisfiable.

let sat f = 
  let n = maxI f in
  let rec satn and k = match k with
    0 -> eval and f
  | _ -> if (satn (false::e) (k-1)) then true else satn (true::e) (k-1) 
  in
  satn [] (n+1)

A6

Write a function taut that verifies if a formula is a tautology.

let taut f = 
  let n = maxI f in
  let rec tautn and k = match k with
    0 -> eval and f
  | _ -> if (tautn (false::e) (k-1)) then (tautn (true::e) (k-1)) else false 
  in
  tautn [] (n+1)

*A7

Give an evaluation of variables that makes the formula x⇒ (y ⇒ x) true.

Every evaluation is ok, the formula is a tautology.

*A8

Give an evaluation of variables that makes the formula x⇒ (y ⇒ x) false.

There is no such evaluation, the formula is a tautology.

*A9

Give an evaluation of variables that makes the formula ¬y⇒ (x ∧ y) true.

The formula is equivalent to y, so y=true makes it true.

*A10

Give an evaluation of variables that makes the formula ¬y⇒ (x ∧ y) false.

The formula is equivalent to y, so y=false makes it false.

*A11

Give an evaluation of variables that makes the formula ((x⇒ y) ⇒ x) ⇒ x true.

Every evaluation is ok, the formula is a tautology.

*A12

Give an evaluation of variables that makes the formula ((x⇒ y) ⇒ x) ⇒ x false.

There is no such evaluation, the formula is a tautology.

*A13

Give the truth table for the formula (x∨ ¬y) ⇒ (x ∧ y).

 


  x y x∨¬y x∧y (x∨ ¬y) ⇒ (x ∧ y)


  false false true true true


  false true true false false


  true false false false true


  true true true false false

Problem of the N queens

B1

Write a function exactly_one that takes an initial variable i, an increment j and a number n and returns the boolean formula that expresses that exactly one of the variables x(i), x(i+j),...,x(i+(n-1)*j) is true.

let exactly_one i j n = 
  let rec  f k n1 = 
    if (n1=1) then (Not (Var k))
    else And (Not (Var k), f (k+j) (n1-1))
  in 
  let rec  g k n2 = 
    if (n2=1) then (Var k)
    else And (Impl (Var k, f (k+j) (n2-1)),
              Impl (Not (Var k), g (k+j) (n2-1)))
  in  g i n

B2

Write a function at_most_one that takes an initial variable i, an increment j and a number n and returns the boolean formula that expresses that at most one of the variables x(i), x(i+j),...,x(i+(n-1)*j) is true.

let at_most_one i j n = 
  let rec  f k n1 = 
    if (n1=1) then (Not (Var k))
    else And (Not (Var k), f (k+j) (n1-1))
  in 
  let rec  g k n2 = 
    if (n2=2) then  Impl (Var k, f (k+j) (n2-1))
    else And (Impl (Var k, f (k+j) (n2-1)),Impl (Not (Var k), g (k+j) (n2-1)))
  in  if (n=1) then True else g i n

B3

Write a function chessboard that takes the dimension n and returns the formula that corresponds to the problem of the n queens.

let gen_rows n = 
  let rec f k n1 = 
    if (n1=1) then exactly_one k 1 n
    else And(exactly_one k 1 n, f (k+n) (n1-1))
  in f 0 n

let gen_cols n = 
  let rec f k n1 =
    if (n1=1) then exactly_one k n n
    else And(exactly_one k n n, f (k+1) (n1-1))
  in f 0 n

let gen_diags n =
  let rec  f k n1 = 
      if (n1=1) then  at_most_one k (n-1) n
      else  And (And (And (at_most_one k (n+1) n1,
                          at_most_one k (n-1) (n-n1+1)),
                     And (at_most_one (n*n-k-1) (-(n+1)) n1,
                          at_most_one (n*n-k-1) (-(n-1)) (n-n1+1))),
                f (k+1) (n1-1))
  in 
    if (n=1) then True
    else And (at_most_one 0 (n+1) n, f 1 (n-1))

let chessboard n =
  if (n<2) then True
  else And (And (gen_rows n, gen_cols n), gen_diags n)

Davis-Putnam Algorithm

C1

Write a function expand that changes the implications and the equivalences with the equivalent formulae.

let rec expand f = match f with
  Var _ | True | False   -> f
| And(a,b) -> And(expand a, expand b)
| Or(a,b) -> Or(expand a, expand b)
| Not a -> Not (expand a)
| Impl(a,b) -> Or(Not (expand a),expand b)
| Equiv(a,b) -> And (Or(expand a,Not (expand b)),Or(Not (expand a),expand b))

C2

Write a function check_cnf that verifies if a formula of type boolean is in CNF.

let check_cnf f = 
  let rec only_neg f = match f with
    True | False | Var _ -> true
  | Not a -> only_neg a
  | _ -> false in
  let rec only_or f = match f with
    Or(a,b) -> (only_or a) && (only_or b)
  | _ -> only_neg f in
  let rec only_and f = match f with
    And(a,b) -> (only_and a) && (only_and b)
  | _ -> only_or f in
  only_and f

C3

Write a function push_neg that, given a boolean formula that contains ∧,∨,¬ only, pushes down the negations.

let rec push_neg f = match f with
  Or (a,b) -> Or (push_neg a, push_neg b)
| And (a,b) -> And (push_neg a, push_neg b)
| Not a -> rpush_neg a
| _ -> f
and
rpush_neg f = match f with
  Or (a,b) -> And (rpush_neg a, rpush_neg b)
| And (a,b) -> Or (rpush_neg a, rpush_neg b)
| Not a -> push_neg a
| True -> False
| False -> True
| _ -> Not f

C4

Write a function push_or that, given a boolean formula that contains ∧,∨,¬ only, pushes the disjunctions after the conjunctions.

let push_or f =
  let rec push_rules a b = match (a,b) with
    And (a1,a2), _ -> And (push_rules a1 b, push_rules a2 b)
  | _, And (b1,b2) -> And (push_rules a b1, push_rules a b2)
  |  _ -> Or (a,b) in
  let rec push f = match f with
    And (a,b) -> And (push a, push b)
  | Or (a,b) -> push_rules (push a) (push b)
  | _ -> f in
  push f

C5

Write a function cnf that turns a boolean formula into an equivalent CNF formula.

let cnf f = push_or (push_neg (expand f))

*C6

Put in CNF the formula (x∨¬y)⇒z.

(¬x ∨ z) ∧ (y ∨ z).

C7

Write a function eval_disj that evaluates a formula (that contains only disjunctions, variables and negations of variables) with respect to the evaluation of some of its variables, and says if the formula is true or false or which are the variables of the formula that do not have value in the given evaluation.
The evaluation can be expressed as a list. The values inside this list are true, false or unknown.

(* The type of values: true, false, or unknown *)
type value = 
    TRUE 
  | FALSE
  | NONE

(* Find the value of a variable inside the list *)
let rec get_env and i = match (e,i) with
  (v::e1), 0 -> v
| (v::e1), _ -> get_env e1 (i-1)
| [], _ -> NONE

(* The type of the result of the evaluation *)
type eval = 
  Satisfied 
| Contradiction 
| Vars of boolean list

let rec eval_disj and f = match f with 
  Var i ->
    begin
     match get_env and i with
       TRUE -> Satisfied
     | FALSE -> Contradiction
     | NONE -> Vars [Var i]
    end
| Not (Var i) ->
    begin
     match get_env and i with
       TRUE ->  Contradiction
     | FALSE -> Satisfied
     | NONE ->  Vars  [Not (Var i)]
    end
| Or (f1,f2) -> 
     begin 
       match eval_disj and f1 with
         Satisfied -> Satisfied 
       | Vars l1 ->
           begin 
             match eval_disj and f2 with
               Satisfied -> Satisfied
             | Contradiction -> Vars l1
             | Vars l2 -> Vars (List.append l1 l2)
           end
       | Contradiction -> eval_disj and f2
      end
| False -> Contradiction
| _ -> Satisfied

C8

Write a function eval_conj that takes a formula in CNF and an evaluation and says if for this evaluation the formula is true, false, or if there are candidates for the unitary resolution.

let rec eval_conj and f = match f with 
  And (f1, f2) ->
    begin
     match eval_conj and f1 with
       Contradiction -> Contradiction
     | Satisfied -> eval_conj and f2 
     | Vars l1 ->
         begin
           match eval_conj and f2 with 
             Satisfied -> Vars l1
           | Contradiction -> Contradiction
           | Vars l2 -> Vars (List.append l1 l2)
         end
    end
|  _ ->
         begin
           match eval_disj and f with
             Satisfied -> Satisfied
           | Contradiction -> Contradiction
           | Vars [v1] -> Vars [v1]
           | Vars _ -> Vars []
         end

C9

Write a function davis that implements the Davis-Putnam algorithm.

(* Update the list e so that at index i there is the value v
  Use the option type to say if this update is possible *)
let rec set_env e i v = match (e,i) with
  (NONE::e1), 0 -> Some (v::e1)
| (v1::e1), 0 -> if (v1=v) then (Some e) else None
| (v1::e1), _ -> 
    begin 
      match (set_env e1 (i-1) v) with
        None -> None
      | Some e2 -> Some (v1::e2)
    end
| [], _ -> set_env [NONE] i v

(* Given a list build two lists where the first NONE of the initial list
   is changed with  TRUE and FALSE respectively *)
let rec split_env e  = match e with
  []  -> [TRUE],[FALSE]
| NONE::e1 -> TRUE::e1, FALSE::e1
| v::e1 -> let l1,l2 = split_env e1 in
            v::l1,v::l2 

(* Assign inside e to v the value TRUE *)
let set_var e v = match v with
  (Var i) -> set_env e i TRUE
| (Not (Var i)) -> set_env e i FALSE
| _ -> Some e

(* Assign to all the variables inside l the value TRUE *)
let rec set_vars e l = match l with
  [] -> Some e
| v::l1 ->
   begin 
     match set_var e v with
       None -> None
     | Some e1 -> set_vars e1 l1
   end


let rec davis f = 
  let rec  davisn e = match eval_conj e f with
    Satisfied -> true
  | Contradiction -> false
  | Vars [] -> 
      let e1,e2 = split_env e in
        if (davisn e1) then true else (davisn e2)
  | Vars l -> 
      begin
        match set_vars e l with
          None -> false
        | Some e1 -> davisn e1
      end
  in davisn []

Monica Nesi

x	y	x∨¬y	x∧y	(x∨ ¬y) ⇒ (x ∧ y)
false	false	true	true	true
false	true	true	false	false
true	false	false	false	true
true	true	true	false	false