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