Optimization modulo non-linear arithmetic via incremental linearization

DOI10.1007/978-3-030-86205-3_12OpenAlexW3198878388MaRDI QIDQ831943

Ahmed Irfan, Alberto Griggio, Patrick Trentin, Roberto Sebastiani, Filippo Bigarella, Martin Jonáš, Marco Roveri, Alessandro Cimatti

Publication date: 24 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-86205-3_12

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Related Items (1)

OMTPlan: A Tool for Optimal Planning Modulo Theories

Uses Software

• SMT-LIB
• z3
• dReal
• CVC
• MathSAT5
• vZ
• GitHub
• OptiMathSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• SAT modulo linear arithmetic for solving polynomial constraints
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Designing theory solvers with extensions
• Subtropical satisfiability
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• From \textsc{MiniZinc} to optimization modulo theories, and back
• A CDCL-style calculus for solving non-linear constraints
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Optimization modulo the theory of floating-point numbers
• Fully incremental cylindrical algebraic decomposition
• Frontiers of combining systems. 11th international symposium, FroCoS 2017, Brasília, Brazil, September 27--29, 2017. Proceedings
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
• Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
• Optimization Modulo Theories with Linear Rational Costs
• Solving Nonlinear Integer Arithmetic with MCSAT
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Algorithm 852
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
• The MathSAT5 SMT Solver
• On SAT Modulo Theories and Optimization Problems
• Delta-decision procedures for exists-forall problems over the reals

This page was built for publication: Optimization modulo non-linear arithmetic via incremental linearization