Conditions for Non-Chronological Backtracking in Boolean Optimization

This paper proposes new algorithms for the Binate Covering P rob- lem (BCP), a well-known restriction of Boolean Optimizatio n. Binate Covering finds application in many areas of Computer Scienceand Engineering. In Artificial Intelligence, BCP can be used forcomput- ing minimum-size prime implicants of Boolean functions, ofinterest in Automated Reasoning and Non-Monotonic Reasoning. Moreo ver, Binate Covering is an essential modeling tool in ElectronicDesign Automation. The objectives of the paper are to briefly reviewbranch- and-bound algorithms for BCP, to describe how to apply backt rack search pruning techniques from the Boolean Satisfiability ( SAT) do- main to BCP, and to illustrate how to strengthen those prunin g tech- niques by exploiting the actual formulation of BCP. Experim ental results, obtained on representative instances indicate th at the pro- posed techniques provide significant performance gains fordifferent classes of instances.