IJCAI-2019 Tutorial:

From Satisfiability to Optimization Modulo Theories

Prof. Roberto Sebastiani, DISI, University of Trento, Italy

SLIDES

Duration: 1/2 day (i.e., 3h, two 1:30h slots).

Abstract

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a (typically quantifier-free) first-order formula with respect to some decidable first-order theory (e.g., that of linear arithmetic over the rationals LRA or the integers LIA and their sub-theories, of Arrays AR, of Bit-Vectors BV and of floating-point numbers FP) and their combinations thereof. SMT engines are widely used as backend engines in many application domains (including, e.g., planning, model checking, requirement engineering, SW and HW verification).
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.

Target Audience

The tutorial is directed to a rather general and transversal AI audience, in particular to people interested in various domains of Automated Reasoning, Knowledge Representation, SAT, SMT, planning, constraint programming and optimization, temporal reasoning, and formal verification. I’d say that any AI scientist who is interested in SMT may very likely be interested in OMT as well.
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.

Motivations and Goals

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a (typically quantifier-free) firstorder formula with respect to some decidable first-order theory, (e.g., that of linear arithmetic over the rationals LRA or the integers LIA and their sub-theories, of Arrays AR, of Bit-Vectors BV and of floating-point numbers FP) and their combinations thereof. SMT problems require capabilities for heavy Boolean reasoning combined with capabilities for reasoning in expressive decidable F.O. theories. To address these requirements, modern SMT solver combine the power of SAT solvers with the expressivity of theory-specific decision procedures (theory solvers or T -solvers), merging techniques from SAT, Theorem Proving, Formal Verification, CSP and Operational Research. The last 15 years have witnessed a boost in the expressiveness and efficiency of SMT solvers, which are now the workhorse backend engine of a large variety of applications.

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.

Outline

This tutorial is planned to cover the following topics:

About Roberto Sebastiani

Roberto Sebastiani is currently associate professor at the Department of Information Sciences & Engineering of University of Trento, Italy. He got a M.S. in Electronic Engineering from University of Padova, Italy, (1991), and a PhD in Computer Science Engineering from University of Genova, Italy (1997).

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.