module type LITERAL = sig       (* tip modul = interfata *)
  type t
  val compare: t -> t -> int          (* necesar pt. multimi *)
  val ispos: t -> bool
  val neg: t -> t
  val print_lit: t -> unit
end

open Printf
module Sat(L: LITERAL) = struct        (* modul parametrizat *)
  module S = Set.Make(L)

  exception Unsat

  let filter_clause ones =
    List.filter (
        fun e -> if S.mem e ones then raise Exit  (* clauza e adevarata *)
                 else not (S.mem (L.neg e) ones)  (* cele care nu sunt false *)
      )
                
  let rec simplify ones lst =
    (*    let init = List.length lst in *)        
    List.fold_left (
        fun (ones, clist) cl -> 
        try (match filter_clause ones cl with
             | [] -> raise Unsat        (* clauza vida -> nerealizabila *)
             | [lit] -> (* L.print_lit lit; print_endline " is true"; *)
                        simplify (S.add lit ones) clist (* reia cu lit=true *)
             | newcl -> (ones, newcl :: clist))
        with Exit -> (ones, clist) (* clauza adevarata -> nu modifica *)
      ) (ones, []) lst
  (*    in printf "simplified %d to %d clauses\n" init (List.length nc);
      List.iter (fun l -> L.print_lit l; print_char ' ')
                 (List.filter L.ispos (S.elements no));
    print_newline(); (no, nc) *)

  let sat cls =
    let rec sat1 ones clist =
    match simplify ones clist with
    | (nones, []) -> nones         (* nu mai sunt clauze: gata *)
    | (nones, (lit::cls)::clist) ->        (* incearca lit cu ambele valori *)
       (* print_string "trying "; L.print_lit lit; print_endline " false"; *)
       S.union nones (
                 try sat1 (S.singleton (L.neg lit)) (cls::clist)
                 with Unsat -> 
                   (* print_string "retry "; L.print_lit lit; print_endline " false"; *)
                   sat1 (S.singleton lit) clist
               )
    in S.elements (sat1 S.empty cls)        (* initial, fara atribuiri *)
end

module IntLit = struct
  type t = int
  let compare = compare
  let ispos = (<) 0
  let neg n = -n
  let print_lit = print_int
end

module SatI = Sat(IntLit)

open Scanf
       
let readeol () = scanf "%[^\n]" ignore; scanf "%c" ignore
                        
let readclause () =
  let rec rdcls lst = 
    scanf " %d" (fun h -> if h = 0 then (readeol(); lst) else rdcls (h :: lst))
  in rdcls []

let rec readhdr () =
  scanf "%c" (function
               | 'c' -> readeol(); readhdr()
               | 'p' -> scanf " %s" (fun s -> if s = "cnf" then readeol()
                                              else failwith "unknown problem type")
               | _ -> failwith "bad DIMACS input")

let readcnf() =
  let rec readcnf1 lst =
    try scanf "c" (); readeol(); readcnf1 lst
    with Scan_failure _ -> readcnf1 (readclause() :: lst)
       | End_of_file -> lst
  in readhdr (); readcnf1 []

let cnf = readcnf()

let _ = List.iter (printf "%d ") (SatI.sat cnf)

This document was generated using caml2html