Book chapter
Generalized Optimization Modulo Theories
Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I, pp.458-479
Lecture Notes in Artificial Intelligence, v. 14739, Springer Nature
2024
DOI: 10.1007/978-3-031-63498-7_27
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 singleand 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.
Details
- Title: Subtitle
- Generalized Optimization Modulo Theories
- Creators
- Nestan Tsiskaridze - Stanford UniversityClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Contributors
- C Benzmuller (Editor)MJH Heule (Editor)R A Schmidt (Editor)
- Resource Type
- Book chapter
- Publication Details
- Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I, pp.458-479
- Publisher
- Springer Nature; Cham
- Series
- Lecture Notes in Artificial Intelligence; v. 14739
- DOI
- 10.1007/978-3-031-63498-7_27
- ISSN
- 2945-9133
- eISSN
- 1611-3349
- Number of pages
- 22
- Grant note
- 2006407 / National Science Foundation; National Science Foundation (NSF) Stanford Agile Hardware Center
- Language
- English
- Date published
- 2024
- Academic Unit
- Computer Science
- Record Identifier
- 9984704760002771
Metrics
1 Record Views