Module Emc

module Emc: sig .. end

Given a matrix of Booleans values (say 0 and 1), the exact matrix problem (EMC) is to find a subset of rows such that each column contains exactly one 1. This module provides a common interface to solve this problem using two different techniques: Dancing Links (module D, see also Dlx) and Zero-Suppressed Binary Decision Diagrams (module Z, see also Zdd).

The EMC problem is slightly generalized as follows: the primary first columns must be covered exactly once, and the remaining columns (called secondary columns) must be covered at most one.

type solution = int list 

module type S = sig .. end

module D: S 

module Z: S  with type t = Zdd.t

val print_boolean_matrix : Format.formatter -> bool array array -> unit

val print_boolean_array : Format.formatter -> bool array -> unit

val print_matrix_size : Format.formatter -> 'a array array -> unit

module Sat: sig .. end