article

Satisfiability-Based Algorithms for Boolean Optimization

Authors:

Vasco M. Manquinho,

João P. Marques-SilvaAuthors Info & Claims

Annals of Mathematics and Artificial Intelligence, Volume 40, Issue 3-4

Pages 353 - 372

https://doi.org/10.1023/B:AMAI.0000012872.46214.11

Published: 01 March 2004 Publication History

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 objectives 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 pruning 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.

References

[1]

{1} P. Barth, A Davis-Putnam enumeration algorithm for linear pseudo-Boolean optimization, Technical Report MPI-I-95-2-003 (Max Plank Institute for Computer Science, 1995).

[2]

{2} R. Bayardo Jr. and R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proceedings of the National Conference on Artificial Intelligence (1997).

Digital Library

[3]

{3} M.S. Bazaraa, J.J. Jarvis and H.D. Sherali, Linear Programming and Network Flows, 2nd ed. (John Wiley & Sons, 1989).

Digital Library

[4]

{4} O. Coudert, Two-level logic minimization, an overview, Integration, The VLSI Journal 17(2) (October 1993) 677-691.

Digital Library

[5]

{5} O. Coudert, On solving covering problems, in: Proceedings of the ACM/IEEE Design Automation Conference (June 1996).

Digital Library

[6]

{6} O. Coudert and J.C. Madre, New ideas for solving covering problems, in: Proceedings of the ACM/IEEE Design Automation Conference (June 1995).

Digital Library

[7]

{7} M. Davis and H. Putnam, A computing procedure for quantification theory, Journal of the Association for Computing Machinery 7 (1960) 201-215.

Digital Library

[8]

{8} D. De Micheli, Synthesis and Optimization of Digital Circuits (McGraw-Hill, 1994).

Digital Library

[9]

{9} P.F. Flores, H.C. Neto and J.P. Marques Silva, An exact solution to the minimum-size test pattern problem, in: Proceedings of the IEEE International Conference on Computer Design (October 1998) pp. 510-515.

Digital Library

[10]

{10} J. Gimpel, A reduction technique for prime implicant tables, IEEE Transactions on Electronic Computers EC-14 (August 1965) 535-541.

[11]

{11} E. Goldberg, L. Carloni, T. Villa, R.K. Brayton and A.L. Sangiovanni-Vincentelli, Negative thinking by incremental problem solving: application to unate covering, in: Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (1997).

Digital Library

[12]

{12} G. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms (Kluwer Academic Publishers, 1996).

Digital Library

[13]

{13} S. Liao and S. Devadas, Solving covering problems using LPR-based lower bounds, in: Proceedings of the ACM/IEEE Design Automation Conference (1997).

Digital Library

[14]

{14} V.M. Manquinho, P.F. Flores, J.P. Marques Silva and A.L. Oliveira, Prime implicant computation using satisfiability algorithms, in: Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (November 1997) pp. 232-239.

Digital Library

[15]

{15} J.P. Marques Silva and K.A. Sakallah, GRASP: A new search algorithm for satisfiability, in: Proceedings of the ACM/IEEE International Conference on Computer-Aided Design (November 1996) pp. 220-227.

Digital Library

[16]

{16} M.R.C.M. Berkelaar, UNIX manual page of lp-solve, in: Eindhoven University of Technology, Design Automation Section, ftp://ftp.es.ele.tue.nl/pub/lp_solve (1992).

[17]

{17} G.L. Nemhauser and L. Wolsey, Integer and Combinatorial Optimization (John Wiley & Sons, 1988).

Digital Library

[18]

{18} C. Pizzuti, Computing prime implicants by integer programming, in: Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (November 1996) pp. 332-336.

Digital Library

[19]

{19} S.J. Russell and P. Norvig, Artificial Intelligence: A Modern Approach (Prentice-Hall, 1994).

Digital Library

[20]

{20} T. Villa, T. Kam, R.K. Brayton and A.L. Sangiovanni-Vincentelli, Explicit and implicit algorithms for binate covering problems, IEEE Transactions on Computer Aided Design 16(7) (July 1997) 677-691.

Digital Library

[21]

{21} S. Yang, Logic Synthesis and Optimization Benchmarks User Guide (Microelectronics Center of North Carolina, January 1991).

[22]

{22} H. Zhang, SATO: An efficient propositional prover, in: Proceedings of the International Conference on Automated Deduction (July 1997) pp. 272-275.

Digital Library

Cited By

Abío IDeters MNieuwenhuis RStuckey P(2011)Reducing chaos in SAT-like searchProceedings of the 14th international conference on Theory and application of satisfiability testing10.5555/2023474.2023504(273-286)Online publication date: 19-Jun-2011
https://dl.acm.org/doi/10.5555/2023474.2023504
Larrosa JNieuwenhuis ROliveras ARodríguez-Carbonell E(2011)A Framework for Certified Boolean Branch-and-Bound OptimizationJournal of Automated Reasoning10.1007/s10817-010-9176-z46:1(81-102)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1007/s10817-010-9176-z
Marques-Silva JArgelich JGraça ALynce I(2011)Boolean lexicographic optimizationAnnals of Mathematics and Artificial Intelligence10.1007/s10472-011-9233-262:3-4(317-343)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1007/s10472-011-9233-2
Show More Cited By

Index Terms

Satisfiability-Based Algorithms for Boolean Optimization
1. Mathematics of computing
  1. Mathematical analysis
    1. Numerical analysis
      1. Number-theoretic computations
2. Theory of computation
  1. Logic
  2. Randomness, geometry and discrete structures

Recommendations

A satisfiability procedure for quantified boolean formulae
The renesse issue on satisfiability

We present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSAT_CNF of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a ...
Efficient Symmetry Breaking for Boolean Satisfiability

Identifying and breaking the symmetries of conjunctive normal form (CNF) formulae has been shown to lead to significant reductions in search times. Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to an ...
Efficient data structures for backtrack search SAT solvers

The implementation of efficient Propositional Satisfiability (SAT) solvers entails the utilization of highly efficient data structures, as illustrated by most of the recent state-of-the-art SAT solvers. However, it is in general hard to compare existing ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Annals of Mathematics and Artificial Intelligence

Annals of Mathematics and Artificial Intelligence Volume 40, Issue 3-4

March 2004

238 pages

ISSN:1012-2443

Issue’s Table of Contents

Copyright © Copyright © 2004 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 March 2004

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Abío IDeters MNieuwenhuis RStuckey P(2011)Reducing chaos in SAT-like searchProceedings of the 14th international conference on Theory and application of satisfiability testing10.5555/2023474.2023504(273-286)Online publication date: 19-Jun-2011
https://dl.acm.org/doi/10.5555/2023474.2023504
Larrosa JNieuwenhuis ROliveras ARodríguez-Carbonell E(2011)A Framework for Certified Boolean Branch-and-Bound OptimizationJournal of Automated Reasoning10.1007/s10817-010-9176-z46:1(81-102)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1007/s10817-010-9176-z
Marques-Silva JArgelich JGraça ALynce I(2011)Boolean lexicographic optimizationAnnals of Mathematics and Artificial Intelligence10.1007/s10472-011-9233-262:3-4(317-343)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1007/s10472-011-9233-2
Morgado AMarques-Silva J(2010)Combinatorial Optimization Solutions for the Maximum Quartet Consistency ProblemFundamenta Informaticae10.5555/1890507.1890513102:3-4(363-389)Online publication date: 1-Aug-2010
https://dl.acm.org/doi/10.5555/1890507.1890513
Argelich JLynce IMarques-Silva J(2009)On solving Boolean multilevel optimization problemsProceedings of the 21st International Joint Conference on Artificial Intelligence10.5555/1661445.1661508(393-398)Online publication date: 11-Jul-2009
https://dl.acm.org/doi/10.5555/1661445.1661508
Heras FLarrosa JOliveras A(2008)MINIMAXSATJournal of Artificial Intelligence Research10.5555/1622655.162265631:1(1-32)Online publication date: 1-Jan-2008
https://dl.acm.org/doi/10.5555/1622655.1622656
Heras FLarrosa JOliveras A(2007)MiniMaxSATProceedings of the 10th international conference on Theory and applications of satisfiability testing10.5555/1768142.1768150(41-55)Online publication date: 28-May-2007
https://dl.acm.org/doi/10.5555/1768142.1768150

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents