NDLI: Solving the Minimum-Cost Satisfiability Problem Using SAT Based Branch-and-Bound Search

Content Provider	IEEE Xplore Digital Library
Author	Zhaohui Fu Malik, S.
Copyright Year	2006
Description	Author affiliation: Dept. of Electr. Eng., Princeton Univ., NJ (Zhaohui Fu; Malik, S.)
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 (Coudert, 1996), and more recently by SAT based algorithms, e.g. bsolo (Manquinho and Marques-Silva, 2002). 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 (Moskewicz et al., 2001), MiniSat (Een and Sorensson, 2006) 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
Starting Page	852
Ending Page	859
File Size	11449075
Page Count	8
File Format	PDF
ISBN	1595933891
ISSN	10923152
DOI	10.1109/ICCAD.2006.320089
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2006-11-05
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Association for Computing Machinery, Inc. (ACM)
Subject Keyword	Business continuity Counting circuits Electronic design automation and methodology Automatic test pattern generation Test pattern generators Design optimization Permission Artificial intelligence Costs Field programmable gate arrays Branch-and-Bound Boolean Satisfiability MinCostSAT
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Computer Science Applications Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

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

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

Solving the Minimum-Cost Satisfiability Problem Using SAT Based Branch-and-Bound Search

Incremental Solving Techniques for SAT-based ATPG

SATIRE: A new incremental satisfiability engine

FPGA PLB Architecture Evaluation and Area Optimization Techniques Using Boolean Satisfiability

Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs

Boolean satisfiability in electronic design automation

A fast pseudo-Boolean constraint solver

Solving the Minimum-Cost Satisfiability Problem Using SAT Based Branch-and-Bound Search

Similar Documents

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

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

Solving the Minimum-Cost Satisfiability Problem Using SAT Based Branch-and-Bound Search

Incremental Solving Techniques for SAT-based ATPG

SATIRE: A new incremental satisfiability engine

FPGA PLB Architecture Evaluation and Area Optimization Techniques Using Boolean Satisfiability

Exploiting Symmetries to Speed Up SAT-Based Boolean Matching for Logic Synthesis of FPGAs

Boolean satisfiability in electronic design automation

A fast pseudo-Boolean constraint solver

Solving the Minimum-Cost Satisfiability Problem Using SAT Based Branch-and-Bound Search