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 Citations (Scopus)

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

Other

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

Fingerprint

Artificial intelligence
Costs
Automatic test pattern generation
Planning
Model checking
Coloring
Field programmable gate arrays (FPGA)
Electronic design automation

All Science Journal Classification (ASJC) codes

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

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] https://doi.org/10.1109/ICCAD.2006.320089
Fu, Zhaohui ; Malik, Sharad. / Solving the minimum-cost satisfiability problem using sat based branch-and-bound search. Proceedings of the 2006 International Conference on Computer-Aided Design, ICCAD. 2006. pp. 852-859
@inproceedings{997c0e04b0074dcfb72307b6a705c170,
title = "Solving the minimum-cost satisfiability problem using sat based branch-and-bound search",
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.",
author = "Zhaohui Fu and Sharad Malik",
year = "2006",
month = "12",
day = "1",
doi = "https://doi.org/10.1109/ICCAD.2006.320089",
language = "English (US)",
isbn = "1595933891",
pages = "852--859",
booktitle = "Proceedings of the 2006 International Conference on Computer-Aided Design, ICCAD",

}

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., 4110137, pp. 852-859, 2006 International Conference on Computer-Aided Design, ICCAD, San Jose, CA, United States, 11/5/06. https://doi.org/10.1109/ICCAD.2006.320089

Solving the minimum-cost satisfiability problem using sat based branch-and-bound search. / Fu, Zhaohui; Malik, Sharad.

Proceedings of the 2006 International Conference on Computer-Aided Design, ICCAD. 2006. p. 852-859 4110137.

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

TY - GEN

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

AU - Fu, Zhaohui

AU - Malik, Sharad

PY - 2006/12/1

Y1 - 2006/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=46149116824&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=46149116824&partnerID=8YFLogxK

U2 - https://doi.org/10.1109/ICCAD.2006.320089

DO - https://doi.org/10.1109/ICCAD.2006.320089

M3 - Conference contribution

SN - 1595933891

SN - 9781595933898

SP - 852

EP - 859

BT - Proceedings of the 2006 International Conference on Computer-Aided Design, ICCAD

ER -

Fu Z, Malik S. 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. 2006. p. 852-859. 4110137 https://doi.org/10.1109/ICCAD.2006.320089