Optimization Modulo Theory

Introduction

Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by adding optimization capabilities. While SMT focuses on finding satisfying assignments to formulas in first-order logic with respect to background theories, OMT additionally allows for finding optimal solutions according to objective functions.

OMT in Arlib

Currently, we rely on the pyomt library for solving OMT problems. (TBD: need to add it as a requirement)

Basic Usage

References

• Sebastiani, R., & Trentin, P. (2015). “Optimization Modulo Theories with Linear Rational Costs”. ACM Transactions on Computational Logic.

• Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., & Chechik, M. (2014). “Symbolic Optimization with SMT Solvers”. POPL.

• Bjørner, N., Phan, A. D., & Fleckenstein, L. (2015). “νZ - An Optimizing SMT Solver”. TACAS.