Affordable Access

Satisfiability-Based Algorithms for Boolean Optimization

Publication Date
  • Computer Science


main.dvi Satisfiability-BasedAlgorithms for Boolean Optimization Vasco M. Manquinho ([email protected]) Dept. of Informatics, Technical University of Lisbon IST/INESC Lisbon, Portugal Joa˜o P. Marques-Silva ([email protected]) Dept. of Informatics, Technical University of Lisbon IST/INESC/Cadence European Labs. Lisbon, Portugal Abstract. This paper proposes new algorithms for the Binate Covering Problem (BCP), a well-known restriction of Boolean Optimization. Binate Covering finds application in many areas of Computer Science and Engineering. In Artificial Intelligence, BCP can be used for computing minimum-size prime implicants of Boolean functions, of interest in Automated Reasoning and Non-Monotonic Reasoning. Moreover, Binate Covering is an essential modeling tool in Electronic Design Automation. The ob- jectives of the paper are to briefly review branch-and-bound algorithms for BCP, to describe how to apply backtrack search pruning techniques from the Boolean Satisfiability (SAT) domain to BCP, and to illustrate how to strengthen those prun- ing techniques by exploiting the actual formulation of BCP. Experimental results, obtained on representative instances indicate that the proposed techniques provide significant performance gains for a large number of problem instances. Keywords: Binate Covering Problem, Propositional Satisfiability, Branch-and-Bound, Backtrack Search, Non-Chronological Backtracking 1. Introduction The generic Boolean Optimization problem as well as several of its restrictions are well-known computationally hard problems, widely used as modeling tools in Computer Science and Engineering. These prob- lems have been the subject of extensive research work in the past (see for example [1]). In this paper we address the Binate Covering Problem (BCP), one of the restrictions of Boolean Optimization. BCP can be formulated as the problem of finding a satisfying assignment for a given Conjunctive Normal Form (CNF) formula subject to minimizing a given cost function. As

There are no comments yet on this publication. Be the first to share your thoughts.