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
复制标题
使用基于 SAT 的分支定界搜索解决最小成本可满足性问题
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
S. Malik
中科院分区：
文献类型：
--
作者：
Z. Fu;S. Malik
布尔值满意度（SAT）在各个领域都有许多成功的应用，例如电子设计自动化（EDA）和人工智能（AI）。但是，在某些情况下，使用一般SAT问题的变体可能需要/更可取。在本文中，我们考虑了一种重要的变化，即最低成本的满足性问题（MinCostsat）。 Mincostsat是一个SAT问题，可最大程度地减少令人满意的作业的成本。 Mincostsat有各种应用，例如自动测试模式生成（ATPG），FPGA路由，AI计划等。此问题已经解决了 - 首先涵盖算法，例如Scherzo（Coudert，1996年），最近通过SAT基于SAT的算法，例如BSOLO（Manquinho和Marques-Silva，2002年）。但是，他们基于的SAT算法并不是当前一代高效的求解器。这一代的求解器，例如Chaff（Moskewicz等，2001），Minisat（Een and Sorensson，2006）等，结合了几个新的进步，例如两个基于观看的基于布尔的直接约束传播，它们提供了数量级的加速顺序。我们首先指出，将此类别的求解器用于Mincostsat问题，然后提出了克服这些挑战的技术。最终的求解器MinCostchaff显示了针对大量问题的几个最新最佳的分支和结合求解器的数量级改进，范围从最小测试模式产生，有限的模型检查到EDA中的有限模型到AI中的图形和计划
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