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方法变体与扩展的框架。