module Z: S with type t = Zdd.t
ZDD-based implementation
type
val create : ?primary:int -> bool array array -> t
Creates an EMC problem.
val create_sparse : ?primary:int -> columns:int -> int list array -> t
To be used instead of create when the matrix is large but sparse.
val find_solution : t -> Emc.solution
Returns the first solution that is found.
Raises Not_found if the problem has no solution.
val iter_solution : (Emc.solution -> unit) -> t -> unit
Emc.iter_solution f p applies f in turn to each solution.
val count_solutions : t -> int
The total number of solutions.
module type ARITH = sig .. end
Minimal arithmetic module to count solutions
module Count:
To count solutions using any arithmetic implementation