sat.ml

type formula = [
  | `Atom of string
  | `Not of formula
  | `Or of formula list
  | `And of formula list
]

type redformula = [
  | `Atom of string
  | `NotAtom of string
  | `Or of redformula list
  | `And of redformula list
]

let sat_solver formula failure success =
  let rec reduce : formula -> redformula =
    let map_reduce fs = List.map (fun f -> reduce (`Not f)) fs in
    function
    | `Atom a -> `Atom a
    | `Not (`Atom a) -> `NotAtom a
    | `Not (`Or fs) -> `And (map_reduce fs)
    | `Not (`And fs) -> `Or (map_reduce fs)
    | `Not (`Not f) -> reduce f
    | `Or fs -> `Or (List.map reduce fs)
    | `And fs -> `And (List.map reduce fs)
  in
  let find_c key alist succ_cont fail_cont =
    try succ_cont (List.assoc key alist)
    with Not_found -> fail_cont ()
  in
  let var_of_lit = function | `Atom x | `NotAtom x -> `Atom x in
  let is_satisfying_value = function | `Atom x -> true | `NotAtom x -> false in
  let does_lit_satisfy lit alist =
    find_c (var_of_lit lit) alist (fun b -> b=(is_satisfying_value lit))
                                  (fun () -> false)
  in
  let bind k v alist = (k,v)::alist in
  let rec sat_gen form target cur f s =
    let sat_lit lit cur f s =
      if does_lit_satisfy lit cur then s cur f
      else if List.mem_assoc (var_of_lit lit) cur then f ()
      else (s (bind (var_of_lit lit) (is_satisfying_value lit) cur) f)
    in
    let rec sat_and forms target cur f s =
      match forms with
      | [] -> s cur f
      | fst::rst -> sat_gen fst target cur f
                      (fun cur' resume -> sat_and rst target cur' resume s)
    in
    let rec sat_or forms target cur f s =
      match forms with
      | [] -> f ()
      | fst::rst -> sat_gen fst target cur (fun () -> sat_or rst target cur f s)
                                           (fun cur' resume -> s cur' resume)
    in
    match form with
      | `Atom x -> sat_lit (`Atom x) cur f s
      | `NotAtom x -> sat_lit (`NotAtom x) cur f s
      | `And fs -> sat_and fs target cur f s
      | `Or fs -> sat_or fs target cur f s
  in sat_gen (reduce formula) true [] failure success

let string_of_solution soln =
  let string_of_binding (f, v) =
    "(" ^ (match f with `Atom x -> x) ^ " " ^ (string_of_bool v) ^ ")"
  in
  "(" ^ (String.concat " " (List.map string_of_binding soln)) ^ ")"

let attempt form =
  let fail () = failwith "no solution" in
  let succ cur resume = cur in
  print_endline (string_of_solution (sat_solver form fail succ))

let () =
  attempt (`Not (`Or ([`Atom "x"; `Atom "y"])));;