Optimization modulo theories with linear rational costs
From MaRDI portal
Abstract: In the contexts of automated reasoning (AR) and formal verification (FV), 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, little work has been done to extend SMT to deal with optimization problems; in particular, we are not aware of any previous 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 the work described in this paper we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of linear rational cost functions, combining SMT with standard minimization techniques. We have implemented the procedures within the MathSAT SMT solver. Due to the absence of competitors in the AR, FV and SMT domains, we have 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 in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
- 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
Cites work
- scientific article; zbMATH DE number 1140674 (Why is no real title available?)
- scientific article; zbMATH DE number 2086596 (Why is no real title available?)
- scientific article; zbMATH DE number 2102695 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- A hierarchy of relaxations for linear generalized disjunctive programming
- A modular approach to MaxSAT modulo theories
- A practical approach to satisfiability modulo linear integer arithmetic
- A structure-preserving clause form translation
- Computing small unsatisfiable cores in satisfiability modulo theories
- Constraint Integer Programming: A New Approach to Integrate CP and MIP
- Disjunctive Programming and a Hierarchy of Relaxations for Discrete Optimization Problems
- Disjunctive programming: Properties of the convex hull of feasible points
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Efficient theory combination via Boolean search
- Lazy satisfiability modulo theories
- Mixed integer programming computation
- New Variants of Lift-and-Project Cut Generation from the LP Tableau: Open Source Implementation and Testing
- On SAT Modulo Theories and Optimization Problems
- Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
- Precise reasoning for programs using containers
- Satisfiability modulo the theory of costs: foundations and applications
- Simplification by Cooperating Decision Procedures
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- The MathSAT5 SMT solver
- Theory and Applications of Satisfiability Testing
- Verifying industrial hybrid systems with \textsc{MathSAT}
Cited in
(23)- 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
- SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
- Semiring programming: a semantic framework for generalized sum product problems
- Learning modulo theories for constructive preference elicitation
- An interleaved depth-first search method for the linear optimization problem with disjunctive constraints
- 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
- Solving linear optimization over arithmetic constraint formula
- Entailment vs. verification for partial-assignment satisfiability and enumeration
- Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results
- On SAT Modulo Theories and Optimization Problems
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
- Structured learning modulo theories
- Symbolic optimization with SMT solvers
- Solving generalized optimization problems subject to SMT constraints
- OMTPlan: A Tool for Optimal Planning Modulo Theories
- Constraint learning: an appetizer
- Satisfiability modulo the theory of costs: foundations and applications
This page was built for publication: Optimization modulo theories with linear rational costs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946768)
