A new algorithm for the binate covering problem and its application to the minimization of Boolean relations

The binate covering problem (BCP) is the problem of finding a minimum cost assignment to variables that is a solution of a Boolean equation f=1. It is a generalization of the set covering (or unate covering) problem, where f is positive unate, and is generally given as a table with rows corresponding to the set elements and the columns corresponding to the subsets. Previous methods have considered the case when f is given as a product-of-sum formula or as a binary decision diagram (BDD). A branch-and-bound algorithm for the BCP that assumes f is expressed as the conjunction of multiple BDDs is presented. The BCP solver that has been implemented can be applied to several problems, including exact minimization of Boolean relations, for which results are presented. It has been possible to solve large, difficult problems (up to 4692 variables) which could not be solved by the product of sum based method.<>