C.: Satisfiability modulo the theory of costs: Foundations and applications. In: Tools and Algorithms for the Construction and Analysis of Systems

Abstract. We extend the setting of Satisfiability Modulo Theories (SMT) by in-troducing 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 integra-tion 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 satisfy-ing 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 pro-pose two algorithms for optimization. Second, we use multiple cost functions to deal with PseudoBoolean constraints. Within the SMT(C) framework, the effec-tively PseudoBoolean constraints are dealt with by the cost solver, while the othe