OPTIMATHSAT: A Tool for Optimization Modulo Theories

作     者：Sebastiani, Roberto Trentin, Patrick 

作者机构：Univ Trento DISI Via Sommar 9 I-39123 Trento Italy 

出 版 物：《JOURNAL OF AUTOMATED REASONING》 (自动推理杂志)

年 卷 期：2020年第64卷第3期

页      面：423-460页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：OPTIMATHSAT Optimization Modulo Theories OMT MAXSMT Sorting networks Multi-objective optimization 

摘      要：Optimization Modulo Theories (OMT) is an extension of SMT which allows for finding models that optimize given objectives. OptiMathSAT is an OMT solver which allows for solving a list of optimization problems on SMT formulas with linear objective functions-on the Boolean, the rational and the integer domains, and on their combination thereof-including (partial weighted) MaxSMT . Multiple and heterogeneous objective functions can be combined together and handled either independently, or lexicographically, or in linear or min-max /max-min combinations. OptiMathSAT provides an incremental interface, it supports both an extended version of the SMT-LIBv2 language and a subset of the FlatZinc language, and can be interfaced via an API. In this paper we describe OptiMathSAT and its usage in full detail.