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

摘要

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.