Optimization Modulo Theories with Linear Rational Costs

DOI10.1145/2699915zbMath1354.68233arXiv1410.6039OpenAlexW2090777457MaRDI QIDQ2946768

Roberto Sebastiani, Silvia Tomasi

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

optimizationautomated reasoningsatisfiability modulo theories

Mathematics Subject Classification ID

Related Items (12)

Optimization modulo non-linear arithmetic via incremental linearization ⋮ Solving linear optimization over arithmetic constraint formula ⋮ OMTPlan: A Tool for Optimal Planning Modulo Theories ⋮ Semiring programming: a semantic framework for generalized sum product problems ⋮ Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results ⋮ Learning modulo theories for constructive preference elicitation ⋮ Structured learning modulo theories ⋮ An interleaved depth-first search method for the linear optimization problem with disjunctive constraints ⋮ Delegatable Functional Signatures ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Optimization modulo the theory of floating-point numbers

Uses Software

• MiniSat
• SCIP
• CPLEX
• Yices
• z3
• GAMS
• LogMIP
• Chaff
• MathSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A hierarchy of relaxations for linear generalized disjunctive programming
• A structure-preserving clause form translation
• Disjunctive programming: Properties of the convex hull of feasible points
• Efficient theory combination via Boolean search
• Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
• Efficient generation of craig interpolants in satisfiability modulo theories
• Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
• Solving SAT and SAT Modulo Theories
• Satisfiability Modulo the Theory of Costs: Foundations and Applications
• Mixed Integer Programming Computation
• Disjunctive Programming and a Hierarchy of Relaxations for Discrete Optimization Problems
• Simplification by Cooperating Decision Procedures
• Theory and Applications of Satisfiability Testing
• The MathSAT5 SMT Solver
• A Modular Approach to MaxSAT Modulo Theories
• Constraint Integer Programming: A New Approach to Integrate CP and MIP
• Precise reasoning for programs using containers
• New Variants of Lift-and-Project Cut Generation from the LP Tableau: Open Source Implementation and Testing
• On SAT Modulo Theories and Optimization Problems

This page was built for publication: Optimization Modulo Theories with Linear Rational Costs