Optimization modulo non-linear arithmetic via incremental linearization
type: Item
instance of: scholarly article
title: Optimization modulo non-linear arithmetic via incremental linearization
DOI: 10.1007/978-3-030-86205-3_12
author: Filippo Bigarella
author: Alberto Griggio
author: Ahmed Irfan
author: Martin Jonáš
author: Roberto Sebastiani
author: Patrick Trentin
author: Alessandro Cimatti
author: Marco Roveri
publication date: 2022-03-24T00:00:00Z
Mathematics Subject Classification ID: 68Txx
zbMATH DE Number: 7497924
describes a project that uses: CVC
describes a project that uses: MathSAT5
describes a project that uses: SMT-LIB
describes a project that uses: z3
describes a project that uses: OptiMathSAT
describes a project that uses: dReal
describes a project that uses: vZ
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: 978-3-030-86205-3 12
OpenAlex ID: W3198878388
cites work: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
cites work: Algorithm 852
cites work: Q5503674
cites work: Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
cites work: SAT modulo linear arithmetic for solving polynomial constraints
cites work: A CDCL-style calculus for solving non-linear constraints
cites work: Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
cites work: The MathSAT5 SMT Solver
cites work: From \textsc{MiniZinc} to optimization modulo theories, and back
cites work: Frontiers of combining systems. 11th international symposium, FroCoS 2017, Brasília, Brazil, September 27--29, 2017. Proceedings
cites work: Subtropical satisfiability
cites work: SAT Solving for Termination Analysis with Polynomial Interpretations
cites work: dReal: An SMT Solver for Nonlinear Theories over the Reals
cites work: Solving Nonlinear Integer Arithmetic with MCSAT
cites work: Delta-decision procedures for exists-forall problems over the reals
cites work: Fully incremental cylindrical algebraic decomposition
cites work: A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
cites work: Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
cites work: Q3992465
cites work: On SAT Modulo Theories and Optimization Problems
cites work: Designing theory solvers with extensions
cites work: Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
cites work: Optimization Modulo Theories with Linear Rational Costs
cites work: Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
cites work: \textsc{OptiMathSAT}: a tool for optimization modulo theories
cites work: Q4804919
cites work: Optimization modulo the theory of floating-point numbers
cites work: Quantifier elimination for real algebra -- the quadratic case and beyond
cites work: Satisfiability of Non-linear (Ir)rational Arithmetic
description: scientific article; zbMATH DE number 7497924