Optimization Modulo Theories (OMT) has emerged as an important extension of the highly successful Satisfiability Modulo Theories (SMT) paradigm. The OMT problem requires solving an SMT problem with the restriction that the solution must be optimal with respect to a given objective function. We introduce a generalization of the OMT problem where, in particular, objective functions can range over partially ordered sets. We provide a formalization of and an abstract calculus for the generalized OMT problem and prove their key correctness properties. Generalized OMT extends previous work on OMT in several ways. First, in contrast to many current OMT solvers, our calculus is theory-agnostic, enabling the optimization of queries over any theories or combinations thereof. Second, our formalization unifies both single- and multi-objective optimization problems, allowing us to study them both in a single framework and facilitating the use of objective functions that are not supported by existing OMT approaches. Finally, our calculus is sufficiently general to fully capture a wide variety of current OMT approaches (each of which can be realized as a specific strategy for rule application in the calculus) and to support the exploration of new search strategies. Much like the original abstract DPLL(T) calculus for SMT, our Generalized OMT calculus is designed to establish a theoretical foundation for understanding and research and to serve as a framework for studying variations of and extensions to existing OMT methodologies.

翻译：优化模理论（OMT）已成为高度成功的可满足性模理论（SMT）范式的重要扩展。OMT问题要求在求解SMT问题时，解必须相对于给定目标函数是最优的。本文引入了OMT问题的一个广义化形式，其中目标函数可取值于偏序集。我们为广义OMT问题提供了形式化定义和抽象演算，并证明了其关键正确性性质。广义OMT在多个方面扩展了先前OMT相关工作：首先，与当前许多OMT求解器不同，我们的演算是理论无关的，从而能够对任意理论或其组合进行查询优化；其次，我们的形式化统一了单目标和多目标优化问题，使得能够在同一框架内研究两者，并便于使用现有OMT方法不支持的目标函数；最后，我们的演算具有足够的一般性，能够完整刻画当前多种OMT方法（每种方法均可作为演算中规则应用的具体策略实现），并支持探索新的搜索策略。类似于SMT的原始抽象DPLL(T)演算，我们的广义OMT演算旨在为理解与研究奠定理论基础，并作为研究现有OMT方法变体与扩展的框架。