Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions

DOI10.1007/978-3-662-46681-0_27MaRDI QIDQ5194955zbMATH OpenOpenAlexFDO

Authors Roberto Sebastiani, Patrick Trentin

Publication date 17 September 2019

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1410.5568

zbMATH Keywords

cost functionunit clausetruth assignmentbound model checkincremental version

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: In the last decade we have witnessed an impressive progress in the expressiveness and efficiency of Satisfiability Modulo Theories (SMT) solving techniques. This has brought previously-intractable problems at the reach of state-of-the-art SMT solvers, in particular in the domain of SW and HW verification. Many SMT-encodable problems of interest, however, require also the capability of finding models that are optimal wrt. some cost functions. In previous work, namely "Optimization Modulo Theory with Linear Rational Cost Functions -- OMT(LAR U T )", we have leveraged SMT solving to handle the minimization of cost functions on linear arithmetic over the rationals, by means of a combination of SMT and LP minimization techniques. In this paper we push the envelope of our OMT approach along three directions: first, we extend it to work also with linear arithmetic on the mixed integer/rational domain, by means of a combination of SMT, LP and ILP minimization techniques; second, we develop a multi-objective version of OMT, so that to handle many cost functions simultaneously; third, we develop an incremental version of OMT, so that to exploit the incrementality of some OMT-encodable problems. An empirical evaluation performed on OMT-encoded verification problems demonstrates the usefulness and efficiency of these extensions.

Recommendations

• Optimization modulo theories with linear rational costs
• Optimization modulo non-linear arithmetic via incremental linearization
• On the usefulness of linear modular arithmetic in constraint programming
• scientific article; zbMATH DE number 1303552
• A practical approach to satisfiability modulo linear integer arithmetic
• From \textsc{MiniZinc} to optimization modulo theories, and back
• Exact arithmetic at low cost. -- A case study in linear programming
• On the complexity of linear programming under finite precision arithmetic

Cited in

(13)

• Optimization modulo non-linear arithmetic via incremental linearization
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Delegatable functional signatures
• Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
• Optimization modulo theories with linear rational costs
• Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
• Global optimization of objective functions represented by ReLU networks
• Optimization modulo the theory of floating-point numbers
• Generalized optimization modulo theories
• Exploiting partial-assignment enumeration in optimization modulo theories
• Optimization modulo the theories of signed bit-vectors and floating-point numbers
• Structured learning modulo theories
• Satisfiability modulo the theory of costs: foundations and applications

This page was built for publication: Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5194955)