Many SMT problems of interest, however, require the capability of finding models that are optimal wrt. some objective functions. These problems are grouped under the umbrella term of Optimization Modulo Theories (OMT).

This tutorial aims at providing an overview of the main problems, techniques, functionalities and applications of OMT, focusing on both expressivity and efficiency. Specific topics include, e.g., supporting objective functions expressed in distinct theories of interest; handling OMT incrementally; dealing with multiple objectives; dealing with important OMT sub-cases like Max-SMT. We briefly describe some interesting applications. Finally, we indicate some open problems and research directions.

The tutorial assumes only a basic knowledge of logic and AI topics. Some background on SAT and/or SMT may be of help, but it is not strictly necessary.

Many SMT-encoded problems of interest, however, require the capability of finding models that are optimal wrt. some objective functions. For instance, in SMT-based planning one may want to find a plan which minimizes the total timespan; in SMT-based goal-modeled requirement engineering, one may want to find the realization of a goal model which best fulfils the stakeholders’ requests; in SMT-based model checking, one may want to find executions optimizing the value of some parameter while full-filling/violating some property –e.g., to find the minimum openingtime interval for a rail-crossing causing a safety violation.

These problems are grouped under the umbrella term of Optimization Modulo Theories (OMT), and involve a variety of sub-problems, depending on the theory expressing the objectives (e.g., LRA, LIA, PB, BV or FP), the way distinct objectives are combined, and other issues. In the last ten years, OMT problems have been deeply investigated, many efficient OMT techniques have been developed, and some tools have been implemented and effectively used to solve OMT-encoded problems coming from a variety of application domains.

The goal of this tutorial is to introduce and overview these problems, techniques, tools and applications for the AI community.

- Motivations and Goals of OMT
- From SMT to OMT
- Motivating applications of OMT;
- OMT vs. other optimization problems & techniques

- OMT Basics: OMT with linear-rational (LRA) objectives
- Offline vs. inline schemata (hints)
- Linear vs. binary search
- Termination and efficiency issues
- Incrementality

- Handling different kinds of objectives
- Linear-integer (LIA) objectives
- Pseudo-Boolean (PB) objectives
- Partial Weighted MaxSMT
- Bit-vector (BV) and Floating-point (FP) objectives

- Dealing with multiple objectives
- Max/min, min/max, linear composition
- Lexicographic optimization
- Boxed optimization
- Pareto optimization (hints)

- Some example OMT applications (hints)
- Formal verification
- Requirement engineering
- Hybrid machine learning
- Encodings for quantum annealing

- Open research problems and future research directions.

His current main interest is Optimization Modulo Theories (OMT), Satisfiability Modulo Theories (SMT) and their applications to Formal Verification and AI problems. His research involves also Formal Verification, Quantum Annealing, SAT, Decision Procedures for modal and description logics, Planning, Theorem Proving.

He has published more than 90 archival papers, many of which on AI or AI-related journals (e.g., Artificial Intelligence, JAIR, Information and Computation, ACM Transaction on Computational Logics, Journal of Automated Reasoning, Journal on Satisfiability, Boolean Modeling and Computation) and conferences (e.g., IJCAI, AAAI, IJCAR, CADE, SAT, KR, FroCoS). (See http://disi.unitn.it/rseba/publist.html.)

He has been co-chair of IJCAR, SAT, FroCoS, SMT/PDPAR conferences. He is senior IJCAI PC member. He is/has been in the PC of AI or AI-related conferences and workshops like IJCAI, AAAI, SAT, IJCAR, CADE, FROCOS, KR, CAV, AIMSA, SMT, PDPAR, Calculemus!. He is associate editor of Journal on Satisfiability, Boolean Modeling and Computation, JSAT. He is editing/has edited special issues on Journal on Symbolic Computation, Journal of Automated Reasoning, Journal on Satisfiability, Boolean Modeling and Computation. He is/has been in the Steering Committee of IJCAR, SAT, FroCoS, SMT conferences.

He is a leading figure in the SMT community and in the OMT sub-branch. He has coauthored 15 archival papers on OMT and its applications and 40 archival papers or book chapters on SMT techniques and applications. He has been co-leading the development of MathSAT, a state-of-the-art SMT solver, and leads the development of OptiMathSAT, a state-of-the-art SMT solver built on top of MathSAT.

For more details, see:

Back to Roberto Sebastiani's home page.