Generalized Optimization Modulo Theories

Nestan Tsiskaridze; Clark Barrett; Cesare Tinelli

doi:10.48550/arxiv.2404.16122

Back

Generalized Optimization Modulo Theories

Preprint

Open access

Generalized Optimization Modulo Theories

Nestan Tsiskaridze, Clark Barrett and Cesare Tinelli

ArXiv.org

Cornell University

04/24/2024

DOI: 10.48550/arxiv.2404.16122

Files and links (1)

url

https://doi.org/10.48550/arxiv.2404.16122View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

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.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Generalized Optimization Modulo Theories
Creators: Nestan Tsiskaridze
Clark Barrett
Cesare Tinelli
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2404.16122
ISSN: 2331-8422
Publisher: Cornell University; Ithaca, New York
Language: English
Date posted: 04/24/2024
Academic Unit: Computer Science
Record Identifier: 9984618195102771

Metrics

87 Record Views