Generalized Optimization Modulo Theories

TL;DR

This paper introduces a theory-agnostic, generalized framework for Optimization Modulo Theories that unifies single- and multi-objective optimization, enabling broader applicability and new research directions.

Contribution

It formalizes a theory-agnostic calculus for generalized OMT, unifying various optimization approaches and supporting complex, multi-objective problems within a single framework.

Findings

Formalization of a theory-agnostic OMT calculus

Unification of single- and multi-objective optimization

Framework supports diverse existing and new strategies

Abstract

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.