(* DPLL algorithm for SAT checking; after SAT-Micro (Conchon et al.) *)

module type LITERAL = sig
  type t
  val compare: t -> t -> int            (* multimile necesita ordonare *)
  val neg: t -> t                       (* negatia *)
end

module Sat(L: LITERAL) = struct
  module S = Set.Make(L)                (* multime de literali *)
  exception Sat of S.t
  exception Unsat

  let rec simplify ones =               (* arg: lit. adev. + lista de clauze *)
    let filter_clause ones =            (* arg: lit. adev. + clauza *)
      List.filter (fun lit ->           (* ones: multimea lit. adevarate *)
        if S.mem lit ones then raise Exit;      (* clauza e satisfacuta *)
        not (S.mem (L.neg lit) ones))   (* filtreaza lit. false *)
    in List.fold_left (fun (ones, cls) cl ->    (* ones, cls acumuleaza rez. *)
      try match filter_clause ones cl with      (* filtreaza cu ones *)
        [] -> raise Unsat                       (* clauza vida *)
      | [lit] -> simplify (S.add lit ones) cls  (* simplifica cu lit adevarat *)
      | cl -> (ones, cl :: cls)                 (* adauga clauza filtrata *)
      with Exit -> (ones, cls))         (* clauza satisf. -> nimic nou *)
    (ones, [])        (* incepe fold cu multimea data + nicio clauza *)

  let sat cls =
    let rec sat1 ones cls = 
      match simplify ones cls with      (* intai simplifica *)
        (ones, []) -> raise (Sat ones)  (* nicio clauza -> gata *)
      | (ones, cls) -> let l1 = List.hd (List.hd cls) and rcl = List.tl cls in (
        try sat1 (S.add l1 ones) rcl    (* incearca cu l1 adevarat *)
        with Unsat -> sat1 (S.add (L.neg l1) ones) cls) (* incearca fals *)
    in try sat1 S.empty cls             (* initial fara lit. atribuite *)
      with Sat ones -> S.elements ones  (* fa lista din multime *)
end

module StrLit = struct
  type t = P of string | N of string
  let compare = compare
  let neg = function P s -> N s | N s -> P s
end
module SatS = Sat(StrLit)
open StrLit;;

SatS.sat [[P "a"; P "b"; N "c"]; [N "a"; P "c"]; [P "a"; N "b"]];;

This document was generated using caml2html