Satisfiability Modulo the Theory of Costs: Foundations and Applications

Abstract. We extend the setting of Satisfiability Modulo Theories (SMT) by introducing a theory of costs C, 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 of C and any other theory T . This framework has two important applications. First, we tackle the problem of Optimization 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...

• Type: Journal
• Year: 2010
• Where: TACAS
• Authors: Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico
• Keywords: Algorithms, Cost Functions, Multiple Cost Functions, SMT Solvers, TACAS 2010