Article

Solving the minimum-cost satisfiability problem using SAT based branch-and-bound search

Authors:

Sharad MalikAuthors Info & Claims

ICCAD '06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design

Pages 852 - 859

https://doi.org/10.1145/1233501.1233681

Published: 05 November 2006 Publication History

Abstract

Boolean Satisfiability (SAT) has seen many successful applications in various fields, such as Electronic Design Automation (EDA) and Artificial Intelligence (AI). However, in some cases it may be required/preferable to use variations of the general SAT problem. In this paper we consider one important variation, the Minimum-Cost Satisfiability Problem (MinCostSAT). MinCostSAT is a SAT problem which minimizes the cost of the satisfying assignment. MinCostSAT has various applications, e.g. Automatic Test Pattern Generation (ATPG), FPGA Routing, AI Planning, etc. This problem has been tackled before - first by covering algorithms, e.g. scherzo [3], and more recently by SAT based algorithms, e.g. bsolo [16]. However the SAT algorithms they are based on are not the current generation of highly efficient solvers. The solvers in this generation, e.g. Chaff [20], MiniSat [5] etc., incorporate several new advances, e.g. two literal watching based Boolean Constraint Propagation, that have delivered order of magnitude speedups. We first point out the challenges in using this class of solvers for the MinCostSAT problem and then present techniques to overcome these challenges. The resulting solver MinCostChaff shows order of magnitude improvement over several current best known branch-and-bound solvers for a large class of problems, ranging from Minimum Test Pattern Generation, Bounded Model Checking in EDA to Graph Coloring and Planning in AI.

References

[1]

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

[2]

O. Coudert. Two-level logic minimization: An overview. Integration the VLSI journal, 17(2):97--140, 1994.

Digital Library

[3]

O. Coudert. On solving covering problems. In Proceedings of the 33rd Design Automation Conference (DAC'96), pages 197--202, 1996.

Digital Library

[4]

O. Coudert and J. C. Madre. New ideas for solving covering problems. In Proceedings of the 32nd Design Automation Conference (DAC'95), pages 641--646, 1995.

Digital Library

[5]

N. Eén and N. Sörensson. The MiniSat page, http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/, 2006.

[6]

P. Flores, H. Neto, and J. Marques-Silva. An exact solution to the minimum size test pattern problem. IEEE Transactions on Design Automation of Electronic Systems, 6(4):629--644, 2001.

Digital Library

[7]

Z. Fu and S. Malik. On solving the Partial MAX-SAT problem. In International Conference on Theory and Applications of Satisfiability Testing (SAT'06), LNCS 4121, pages 252--265, 2006.

Digital Library

[8]

R. Gomory. Outline of an algorithm for integer solution to linear programs. Bulletin of the American Mathematical Society, 64:275--278, 1958.

[9]

H. H. Hoos and T. Stützle. SATLIB: An online resource for research on SAT, http://www.satlib.org.SAT 2000, pages 283--292, 2000.

[10]

ILOG. Cplex homepage, http://www.ilog.com/products/cplex/, 2006.

[11]

D. S. Johnson. Approximation algorithms for combinatorial problems. Journal of Computer and System Sciences, 9:256--278, 1974.

Digital Library

[12]

S. Khanna, M. Sudan, L. Trevisan, and D. Williamson. The approximability of constraint satisfaction problems. SIAM Journal of Computing, 30(6): 1863--1920, 2000.

Digital Library

[13]

X. Y. Li. Optimization Algorithms for the Minimum-Cost Satisfiability Problem. PhD thesis, Department of Computer Science, North Carolina State University, Raleigh, North Carolina, 2004. 162 pages.

Digital Library

[14]

S. Liao and S. Devadas. Solving covering problems using LPR-based lower bounds. In Proceedings of the 34th Design Automation Conference (DAC'97), pages 117--120, 1997.

Digital Library

[15]

V. Manquinho, P. Flores, J. Marques-Silva, and A. Oliverira. Prime implicant computation using satisfiability algorithms. In Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI'99), pages 117--120, 1999.

[16]

V. Manquinho and J. Marques-Silva. Search pruning techniques in SAT-based branch-and-bound algorithms for the binate covering problem. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 21:505--516, 2002.

Digital Library

[17]

V. Manquinho and O. Roussel. Pseudo-Boolean evaluation 2005 http://www.cril.univ-artois.fr/PB05/, August 2005.

[18]

J. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48:506--521, 1999.

Digital Library

[19]

S. Miyazaki, K. Iwama, and Y. Kambayashi. Database queries as combinatorial optimization problems. In Proceedings of the International Symposium on Cooperative Database Systems for Advanced Applications, pages 448--454, 1996.

[20]

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC'01), 2001.

Digital Library

[21]

S. Yang. Logic synthesis and optimization benchmarks user guide. Technical Report 1991-IWLS-UG-Saeyang, MCNC, Research Triangle Park, NC, 1991.

Cited By

Zhai EChen APiskac RBalakrishnan MTian BSong BZhang HBhagwan RPorter G(2020)Check before you changeProceedings of the 17th Usenix Conference on Networked Systems Design and Implementation10.5555/3388242.3388285(575-590)Online publication date: 25-Feb-2020
https://dl.acm.org/doi/10.5555/3388242.3388285
Jabbour SKaci SSais LSalhi Y(2016)Itemset Mining with Penalties2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI)10.1109/ICTAI.2016.0148(962-966)Online publication date: Nov-2016
https://doi.org/10.1109/ICTAI.2016.0148
Lu QHuang RChen YXu YZhang WChen G(2014)A SAT-based approach to cost-sensitive temporally expressive planningACM Transactions on Intelligent Systems and Technology10.1145/2542182.25422005:1(1-35)Online publication date: 3-Jan-2014
https://dl.acm.org/doi/10.1145/2542182.2542200
Show More Cited By

Index Terms

Solving the minimum-cost satisfiability problem using SAT based branch-and-bound search
1. Hardware
  1. Integrated circuits
    1. Logic circuits

Recommendations

Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts
DAC '09: Proceedings of the 46th Annual Design Automation Conference

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and ...
Iterative SAT Solving for Minimum Satisfiability
ICTAI '12: Proceedings of the 2012 IEEE 24th International Conference on Tools with Artificial Intelligence - Volume 01

Minimum Satisfiability (MinSAT) denotes one of the optimization versions of the Boolean Satisfiability (SAT) problem. In some settings MinSAT is preferred to using Maximum Satis-fiability (MaxSAT). Several encodings and dedicated branch and bound ...
Accelerating Boolean Satisfiability (SAT) solving by common subclause elimination

Boolean Satisfiability (SAT) is an important problem in many domains. Modern SAT solvers have been widely used in important industrial applications including automated planning and verification. To solve more problems in real applications, new ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '06: Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design

November 2006

147 pages

ISBN:1595933891

DOI:10.1145/1233501

General Chair:
Soha Hassoun
Tufts Univ., Medford, MA

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CAS: Circuits & Systems
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 November 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICCAD06

Sponsor:

SIGDA
IEEE-CAS
IEEE-CS

ICCAD06: The International Conference on Computer-Aided Design 2006

November 5 - 9, 2006

California, San Jose

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
416
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhai EChen APiskac RBalakrishnan MTian BSong BZhang HBhagwan RPorter G(2020)Check before you changeProceedings of the 17th Usenix Conference on Networked Systems Design and Implementation10.5555/3388242.3388285(575-590)Online publication date: 25-Feb-2020
https://dl.acm.org/doi/10.5555/3388242.3388285
Jabbour SKaci SSais LSalhi Y(2016)Itemset Mining with Penalties2016 IEEE 28th International Conference on Tools with Artificial Intelligence (ICTAI)10.1109/ICTAI.2016.0148(962-966)Online publication date: Nov-2016
https://doi.org/10.1109/ICTAI.2016.0148
Lu QHuang RChen YXu YZhang WChen G(2014)A SAT-based approach to cost-sensitive temporally expressive planningACM Transactions on Intelligent Systems and Technology10.1145/2542182.25422005:1(1-35)Online publication date: 3-Jan-2014
https://dl.acm.org/doi/10.1145/2542182.2542200
Abío IStuckey P(2014)Encoding Linear Constraints into SATPrinciples and Practice of Constraint Programming10.1007/978-3-319-10428-7_9(75-91)Online publication date: 2014
https://doi.org/10.1007/978-3-319-10428-7_9
Abío INieuwenhuis ROliveras ARodríguez-Carbonell E(2013)A Parametric Approach for Smaller and Better Encodings of Cardinality ConstraintsPrinciples and Practice of Constraint Programming10.1007/978-3-642-40627-0_9(80-96)Online publication date: 2013
https://doi.org/10.1007/978-3-642-40627-0_9
Huang HZhang SOu XPrakash ASakallah KZakon RMcDermott JLocasto M(2011)Distilling critical attack graph surface iteratively through minimum-cost SAT solvingProceedings of the 27th Annual Computer Security Applications Conference10.1145/2076732.2076738(31-40)Online publication date: 5-Dec-2011
https://dl.acm.org/doi/10.1145/2076732.2076738
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 JJanota MLynce I(2010)On Computing Backbones of Propositional TheoriesProceedings of the 2010 conference on ECAI 2010: 19th European Conference on Artificial Intelligence10.5555/1860967.1860972(15-20)Online publication date: 4-Aug-2010
https://dl.acm.org/doi/10.5555/1860967.1860972
Homer JOu X(2009)Sat-solving approaches to context-aware enterprise network security managementIEEE Journal on Selected Areas in Communications10.1109/JSAC.2009.09040727:3(315-322)Online publication date: 1-Apr-2009
https://dl.acm.org/doi/10.1109/JSAC.2009.090407
Tayade RAbraham J(2009)Critical Path Selection for Delay Test Considering Coupling NoiseProceedings of the 2009 European Test Symposium10.1109/ETS.2009.37(163-168)Online publication date: 25-May-2009
https://dl.acm.org/doi/10.1109/ETS.2009.37
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten