Commit 52eeaf78 authored by pa's avatar pa

Made the basis of the algorithm

parent 07294cdb
......@@ -2,9 +2,9 @@ module type CHOICE = sig
val choice : Ast.Cnf.t -> Ast.var
end
module DefaultChoice =
module DefaultChoice : CHOICE =
struct
let choice : Ast.Cnf.t -> Ast.var = fun cnf -> failwith "todo: choice"
let choice : Ast.Cnf.t -> Ast.var = fun cnf -> Ast.Clause.choose (Ast.Cnf.choose cnf)
end
module type SOLVER = sig
......@@ -13,5 +13,23 @@ end
module DPLL(C:CHOICE) : SOLVER =
struct
let solve : Ast.t -> Ast.model option = fun p -> failwith "todo: solve"
module VarPool = Set.Make(struct type t = Ast.var let compare = compare end)
exception Incoherent
let units (p : Ast.Cnf.t) : VarPool.t =
Ast.Cnf.fold (fun clause acc -> List.fold_left (fun acc2 var -> VarPool.add var acc2)
acc (Ast.Clause.elements clause))
(Ast.Cnf.filter (fun clause -> Ast.Clause.cardinal clause = 1) p) VarPool.empty
let unit_propagation (p : Ast.Cnf.t) (vp : VarPool.t) : Ast.Cnf.t option =
let next (clause : Ast.Clause.t) (vp : VarPool.t) : Ast.Clause.t =
Ast.Clause.fold (fun var acc -> if VarPool.mem (-var) vp then raise Incoherent;
if VarPool.mem var vp then acc else Ast.Clause.add var acc) clause Ast.Clause.empty in
try
Some (Ast.Cnf.fold (fun clause acc -> let cl2 = next clause vp in
if (Ast.Clause.is_empty cl2) then acc else Ast.Cnf.add cl2 acc) p Ast.Cnf.empty)
with Incoherent -> None
let coherent (p : VarPool.t) : bool = VarPool.is_empty (VarPool.inter (VarPool.map ((-) 0) p) p)
let solve (p : Ast.t) : Ast.model option = failwith "f"
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment