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

Zhaohui Fu, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

23 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 2006 International Conference on Computer-Aided Design, ICCAD
Pages852-859
Number of pages8
DOIs
StatePublished - Dec 1 2006
Event2006 International Conference on Computer-Aided Design, ICCAD - San Jose, CA, United States
Duration: Nov 5 2006Nov 9 2006

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Other

Other2006 International Conference on Computer-Aided Design, ICCAD
CountryUnited States
CitySan Jose, CA
Period11/5/0611/9/06

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Keywords

  • Boolean satisfiability
  • Branch-and-bound
  • MinCostSAT

Fingerprint Dive into the research topics of 'Solving the minimum-cost satisfiability problem using sat based branch-and-bound search'. Together they form a unique fingerprint.

  • Cite this

    Fu, Z., & Malik, S. (2006). Solving the minimum-cost satisfiability problem using sat based branch-and-bound search. In Proceedings of the 2006 International Conference on Computer-Aided Design, ICCAD (pp. 852-859). [4110137] (IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD). https://doi.org/10.1109/ICCAD.2006.320089