Optimization modulo the theories of signed bit-vectors and floating-point numbers
type: Item
instance of: scholarly article
title: Optimization modulo the theories of signed bit-vectors and floating-point numbers
author: Patrick Trentin
author: Roberto Sebastiani
published in: Journal of Automated Reasoning
publication date: 2021-11-24T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7433028
zbMATH Keywords: optimization modulo theories
zbMATH Keywords: OMT satisfiability modulo theories
zbMATH Keywords: SMT floating-point arithmetic attractor dynamic attractor
describes a project that uses: SYMBA
describes a project that uses: UppSAT
describes a project that uses: OptiMathSAT
describes a project that uses: Boolector
describes a project that uses: vZ
describes a project that uses: STP
MaRDI profile type: Publication
full work available at URL: s10817-021-09600-4
OpenAlex ID: W3185622705
cites work: Encoding RTL constructs for \textsc{MathSAT}: a preliminary report
cites work: Deciding floating-point logic with abstract conflict driven clause learning
cites work: Q3181652
cites work: Satisfiability Modulo the Theory of Costs: Foundations and Applications
cites work: A Modular Approach to MaxSAT Modulo Theories
cites work: A Decision Procedure for Bit-Vectors and Arrays
cites work: Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
cites work: Symbolic optimization with SMT solvers
cites work: Propagation based local search for bit-precise reasoning
cites work: On SAT Modulo Theories and Optimization Problems
cites work: Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
cites work: Optimization Modulo Theories with Linear Rational Costs
cites work: \textsc{OptiMathSAT}: a tool for optimization modulo theories
cites work: Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
cites work: Optimization modulo the theory of floating-point numbers
cites work: Exploring approximations for floating-point arithmetic using UppSAT
cites work: Approximations for Model Construction
cites work: An approximation framework for solvers and decision procedures
DOI: 10.1007/S10817-021-09600-4
description: scientific article; zbMATH DE number 7433028