On Solving Boolean Optimization with Satisfiability-Based Algorithms

This paper proposes new algorithms for the Binate Covering P roblem (BCP), a well-known restriction of Boolean Optimization. Binate Covering finds application in many are as of Computer Science and Engineering. In Artificial Intel- ligence, BCP can be used for computing minimum-size prime im plicants of Boolean functions, of interest in Automated Reasoning and Non-Monotonic Reasoning. Binate Covering is also an essential modeling tool in Electronic Design Au- tomation (EDA). The objectives of the paper are to briefly rev iew algorithmic solutions for BCP, and to describe how to apply search pruning techniques from the Boolean Satisfiabi lity (SAT) domain to BCP. Furthermore, we generalize these pruning techniques, in particular the ability to backtracknon-chronologically, to exploit the actual formulation ofthe bi- nate covering problem. Experimental results, obtained on r epresentative instances indicate that the proposed techni ques provide significant performance gains for different classe s of instances.