Satisfiability Modulo the Theory of Costs: Foundations and Applications
Satisfiability Modulo the Theory of Costs: Foundations and Applications
复制标题
DOI：
10.1007/978-3-642-12002-2_8
复制
发表时间：
2010-03
期刊：
影响因子：
--
通讯作者：
A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani;Cristian Stenico
中科院分区：
文献类型：
--
作者：
A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani;Cristian Stenico
我们通过引入成本理论来扩展可满足性模理论（SMT）的设置，其中可以对资源消耗和多个成本函数进行建模和推理，例如，电池时间和空间我们定义了一个决策过程，它具有与惰性SMT模式集成所需的所有功能：递增性，回溯性，冲突集的构建和演绎。这自然会导致SMT求解器的不相交工会和任何其他理论。首先，我们解决了优化模理论的问题：而不是检查一个满意的分配的存在，在SMT中，我们需要一个满意的分配，最小化给定的成本函数。我们建立在SMT的决策问题与成本，即，在容许范围内寻找一个代价满足的指派问题，并提出了两种优化算法。其次，我们使用多个代价函数来处理伪布尔约束。在该框架内，有效的伪布尔约束处理的成本solver，而其他约束减少到纯布尔reasoning.We实现了所提出的方法内的MathSAT SMT solver，我们实验评估了一个大的基准集，也从工业应用。结果清楚地表明了该方法的潜力。
We extend the setting of Satisfiability Modulo Theories (SMT) by introducing a theory of costs, where it is possible to model and reason about resource consumption and multiple cost functions, e.g., battery, time, and space. We define a decision procedure that has all the features required for the integration withint the lazy SMT schema: incrementality, backtrackability, construction of conflict sets, and deduction. This naturally results in an SMT solver for the disjoint union ofand any other theory.This framework has two important applications. First, we tackle the problem ofOptimization Modulo Theories: rather than checking the existence of a satisfying assignment, as in SMT, we require a satisfying assignment that minimizes a given cost function. We build on the decision problem for SMT with costs, i.e., finding a satisfying assigniment with cost within an admissibility range, and propose two algorithms for optimization. Second, we use multiple cost functions to deal withPseudoBoolean constraints. Within theframework, the effectively PseudoBoolean constraints are dealt with by the cost solver, while the other constraints are reduced to pure boolean reasoning.We implemented the proposed approach within the MathSAT SMT solver, and we experimentally evaluated it on a large set of benchmarks, also from industrial applications. The results clearly demonstrate the potential of the approach.