Optimization in SMT with LA( Q) cost functions

DOI10.1007/978-3-642-31365-3_38MaRDI QIDQ2908520zbMATH OpenOpenAlexFDO

Authors Roberto Sebastiani, Silvia Tomasi

Publication date 5 September 2012

Published in Automated Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Abstract: In the contexts of automated reasoning and formal verification, important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade efficient SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, bit-vectors). Surprisingly, very few work has been done to extend SMT to deal with optimization problems; in particular, we are not aware of any work on SMT solvers able to produce solutions which minimize cost functions over arithmetical variables. This is unfortunate, since some problems of interest require this functionality. In this paper we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of LA(Q) cost functions, combining SMT with standard minimization techniques. We have implemented the proposed approach within the MathSAT SMT solver. Due to the lack of competitors in AR and SMT domains, we experimentally evaluated our implementation against state-of-the-art tools for the domain of linear generalized disjunctive programming (LGDP), which is closest in spirit to our domain, on sets of problems which have been previously proposed as benchmarks for the latter tools. The results show that our tool is very competitive with, and often outperforms, these tools on these problems, clearly demonstrating the potential of the approach.

Recommendations

• Optimization modulo theories with linear rational costs
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
• Satisfiability modulo the theory of costs: foundations and applications
• On SAT Modulo Theories and Optimization Problems
• Symbolic optimization with SMT solvers

Cited in

(22)

• Solving linear optimization over arithmetic constraint formula
• An interleaved depth-first search method for the linear optimization problem with disjunctive constraints
• Optimization modulo the theories of signed bit-vectors and floating-point numbers
• Local search with a SAT oracle for combinatorial optimization
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Iterative and core-guided maxsat solving: a survey and assessment
• Delegatable functional signatures
• A survey of satisfiability modulo theory
• Solving generalized optimization problems subject to SMT constraints
• Optimization modulo theories with linear rational costs
• Search-space partitioning for parallelizing SMT solvers
• Satisfiability modulo the theory of costs: foundations and applications
• scientific article; zbMATH DE number 7444022 (Why is no real title available?)
• Structured learning modulo theories
• Learning discrete decomposable graphical models via constraint optimization
• Symbolic optimization with SMT solvers
• Exploiting partial-assignment enumeration in optimization modulo theories
• Unifying framework for optimizations in non-Boolean formalisms
• Generalized optimization modulo theories
• Optimization modulo non-linear arithmetic via incremental linearization
• Algebraic program analysis
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty

This page was built for publication: Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions

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