On SAT Modulo Theories and Optimization Problems
On SAT Modulo Theories and Optimization Problems
复制标题
SAT 模理论与最优化问题
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Albert Oliveras
中科院分区：
文献类型：
--
作者：
R. Nieuwenhuis;Albert Oliveras
SAT模理论(SMT)的求解器现在可以处理大型工业问题(例如，正式的硬件和软件验证)，而不是整数、数组或等式等理论。在这里，我们展示了SMT方法还可以有效地解决乍一看不具有典型SMT风格的问题。特别地，我们在这里处理SAT和SMT问题，其中模型M被寻求使得给定的成本函数f(M)最小化。
为此，我们引入了SMT的一个变种，其中理论T变得越来越强，并用抽象的DPLL模理论框架证明了它的正确性。我们讨论了这种SMT变体的两个不同的应用实例：加权MAX-SAT和加权MAX-SMT。我们展示了如何以相对较少的努力，获得一个具有竞争力的系统，在差分逻辑理论中的加权Max-SMT的情况下，甚至可以处理众所周知的硬无线电频率分配问题，而不需要任何定制的启发式算法。这些结果似乎表明MAX-SAT/SMT技术已经可以用于实际应用。
Solvers for SAT Modulo Theories (SMT) can nowadays handle large industrial (e.g., formal hardware and software verification) problems over theories such as the integers, arrays, or equality. Here we show that SMT approaches can also efficiently solve problems that, at first sight, do not have a typical SMT flavor. In particular, here we deal with SAT and SMT problems where models M are sought such that a given cost function f(M) is minimized.
For this purpose, we introduce a variant of SMT where the theory T becomes progressively stronger, and prove it correct using the Abstract DPLL Modulo Theories framework. We discuss two different examples of applications of this SMT variant: weighted Max-SAT and weighted Max-SMT. We show how, with relatively little effort, one can obtain a competitive system that, in the case of weighted Max-SMT in the theory of Difference Logic, can even handle well-known hard radio frequency assignment problems without any tailored heuristics. These results seem to indicate that Max-SAT/SMT techniques can already be used for realistic applications.