DPLL algorithm

definitions.ml

type variable = X of int | Y of int
type assign = variable * bool
type literal = bool * variable
type clause = literal list
type cnf = clause list

type formula =
| And of formula * formula 
| Or of formula * formula
| Not of formula
| Var of variable

let string_of_variable = function
  X id -> "x" ^ string_of_int id
  | Y id -> "y" ^ string_of_int id

let string_of_assign ((v, b) : assign) = string_of_variable v ^ " := " ^ string_of_bool b

let string_of_literal ((b, v) : literal) = (if b then "" else "~") ^ string_of_variable v

let string_of_clause (c : clause) = if c = [] then "false" else String.concat " \\/ " @@ List.map string_of_literal c

let string_of_cnf (c : cnf) = if c = [] then "true" else String.concat " /\\ " @@ List.map (fun cl -> "(" ^ string_of_clause cl ^ ")") c

(*
Var: 0
Not: 1, ~
And: 2, /\ 
Or: 3, \/
*)

let var_priority = 0
let not_priority = 1
let and_priority = 2
let or_priority = 3

let add_parenthesis outer_p (inner_p, s) =
  if inner_p > outer_p then "(" ^ s ^ ")" else s

let rec string_of_formula' = function
  And (f0, f1) ->
    let p0, s0 = string_of_formula' f0 in
    let p1, s1 = string_of_formula' f1 in
    (and_priority,
      add_parenthesis and_priority (p0, s0) ^ " /\\ " ^ add_parenthesis and_priority (p1, s1))
  | Or (f0, f1) ->
    let p0, s0 = string_of_formula' f0 in
    let p1, s1 = string_of_formula' f1 in
    (or_priority,
      add_parenthesis or_priority (p0, s0) ^ " \\/ " ^ add_parenthesis or_priority (p1, s1))
  | Not f ->
    let p, s = string_of_formula' f in
    (not_priority,
      "~" ^ add_parenthesis not_priority (p, s))
  | Var v ->
    (var_priority, string_of_variable v)

let string_of_formula (f : formula) =
  let _, s = string_of_formula' f in s

dpll.ml

open Definitions

let literal_of_variable (v : variable) : literal = (true, v)
let literal_not ((b, v) : literal) : literal = (not b, v)

let cnf_assign (cnf: cnf) ((v, b): assign) : cnf =
	let cnf' = List.filter (fun cl -> not (List.mem (b, v) cl)) cnf in
	let cnf'' = List.map (fun cl -> List.filter (fun l -> l <> (not b, v)) cl) cnf' in
	cnf''

let rec dpll (cnf : cnf) : assign list option =
(*    print_string ("dpll: " ^ string_of_cnf cnf ^ "\n");*)
	let is_trivially_true c = (c = []) in
	let is_trivially_false = List.mem [] in
	if is_trivially_true cnf then
		Some []
	else if is_trivially_false cnf then
		None
	else
	let is_single_literal = function
		[_] -> true
		| _ -> false in
	try
		let (b, v) = List.hd @@ List.find is_single_literal cnf in
		let cnf' = cnf_assign cnf (v, b) in
		match dpll cnf' with
			Some a -> Some ((v, b)::a)
			| None -> None
	with
		Not_found ->
			let _, v = List.hd @@ List.hd cnf in
			(match dpll (cnf_assign cnf (v, true)) with
			Some a -> Some ((v, true)::a)
			| None -> (match dpll (cnf_assign cnf (v, false)) with
			Some a -> Some ((v, false)::a)
			| None -> None))

test.ml

open Definitions
(*
let var_id : int ref = ref 0
let new_variable () = let id = !var_id in var_id := !var_id + 1; Var id

let _ =
	let l0 = literal_of_variable @@ new_variable () in
	let l1 = literal_of_variable @@ new_variable () in
	let l2 = literal_of_variable @@ new_variable () in
	let l3 = literal_of_variable @@ new_variable () in
	let cnf = [[l0; l1]; [l2; l3]; [literal_not l1]] in
	match dpll cnf with
	Some al -> List.iter (fun a -> print_string @@ string_of_assign a; print_string "\n") al
	| None -> ()
*)

let test_cases_cnf : cnf list = [
[
	[(true, X 0); (true, X 1)];
	[(true, X 2); (true, X 3)];
	[(false, X 0)]
];
[];
[[]];
[
	[(true, X 0); (true, X 1)];
	[(true, X 2)];
	[(false, X 0); (false, X 2)]
];
[[(true, X 0)]; [(false, X 0)]];
[[(true, X 0); (false, X 0)]];
]

let test_cases_formula : formula list = [
	And (Var (X 0), Var (X 1));
	Or (Var (X 0), Var (X 1));
	Not (Var (X 0));
	And (Var (X 0), Or (Var (X 1), Var (X 2)));
	And (Var (X 0), And (Var (X 1), Var (X 2)))
]

let option_map f = function
	Some x -> Some (f x)
	| None -> None

let _ =
	let string_of_sat_result = function
		Some al -> "SAT: [" ^ (String.concat "; " @@ List.map string_of_assign al) ^ "]"
		| None -> "UNSAT" in
	print_endline "==== test (cnf) ====";
	List.iter (fun cnf ->
		print_endline @@ string_of_cnf cnf;
		print_endline @@ string_of_sat_result @@ Dpll.dpll cnf
    ) test_cases_cnf;
	print_endline "==== test (formula) ====";
	List.iter (fun formula ->
		print_endline @@ string_of_formula formula;
		let cnf = Tseitin.tseitin formula in
		print_endline @@ string_of_cnf cnf;
		let result = Dpll.dpll cnf in
		print_endline @@ string_of_sat_result @@ result;
		print_endline @@ string_of_sat_result @@ option_map (List.filter (fun (v, b) -> match v with X _ -> true | Y _ -> false)) result
	) test_cases_formula

tseitin.ml

open Definitions

let var_id : int ref = ref 0
let new_var () = let id = !var_id in var_id := !var_id + 1; Y id

let rec tseitin' : formula -> variable * cnf = function
	And (f0, f1) ->
		let v0, cnf0 = tseitin' f0 in
		let v1, cnf1 = tseitin' f1 in
		let v = new_var () in
		(v, [[(false, v); (true, v0)]; [(false, v); (true, v1)]; [(true, v); (false, v0); (false, v1)]] @ cnf0 @ cnf1)
	| Or (f0, f1) ->
		let v0, cnf0 = tseitin' f0 in
		let v1, cnf1 = tseitin' f1 in
		let v = new_var () in
		(v, [[(false, v); (true, v0); (true, v1)]; [(true, v); (false, v0)]; [(true, v); (false, v1)]] @ cnf0 @ cnf1)
	| Not f ->
		let v', cnf = tseitin' f in
		let v = new_var () in
		(v, [[(false, v); (false, v')]; [(true, v); (true, v')]] @ cnf)
	| Var v -> (v, [])

let tseitin (f : formula) : cnf =
	let v, cnf = tseitin' f in
	[(true, v)]::cnf