Optimization modulo non-linear arithmetic via incremental linearization

DOI10.1007/978-3-030-86205-3_12MaRDI QIDQ831943zbMATH OpenOpenAlexFDO

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

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)

Cites work

• scientific article; zbMATH DE number 42574 (Why is no real title available?)
• scientific article; zbMATH DE number 1903374 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A CDCL-style calculus for solving non-linear constraints
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• Algorithm 852
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Delta-decision procedures for exists-forall problems over the reals
• Designing theory solvers with extensions
• From \textsc{MiniZinc} to optimization modulo theories, and back
• Frontiers of combining systems. 11th international symposium, FroCoS 2017, Brasília, Brazil, September 27--29, 2017. Proceedings
• Fully incremental cylindrical algebraic decomposition
• Incomplete SMT techniques for solving non-linear formulas over the integers
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• On SAT Modulo Theories and Optimization Problems
• Optimization in SMT with \(\mathcal{LA}(\mathbb Q)\) cost functions
• Optimization modulo the theory of floating-point numbers
• Optimization modulo theories with linear rational costs
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
• Quantifier elimination for real algebra -- the quadratic case and beyond
• SAT Solving for Termination Analysis with Polynomial Interpretations
• SAT modulo linear arithmetic for solving polynomial constraints
• Satisfiability of non-linear (ir)rational arithmetic
• Solving nonlinear integer arithmetic with MCSAT
• Subtropical satisfiability
• The MathSAT5 SMT solver
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• dReal: an SMT solver for nonlinear theories over the reals

Cited in

(4)

• scientific article; zbMATH DE number 4191003 (Why is no real title available?)
• Optimization modulo the theory of floating-point numbers
• Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
• OMTPlan: A Tool for Optimal Planning Modulo Theories

Describes a project that uses

Uses Software

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

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

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