Generalized Optimization Modulo Theories
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要