Optimization modulo the theories of signed bit-vectors and floating-point numbers
From MaRDI portal
Publication:2051569
DOI10.1007/s10817-021-09600-4OpenAlexW3185622705MaRDI QIDQ2051569
Patrick Trentin, Roberto Sebastiani
Publication date: 24 November 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-021-09600-4
optimization modulo theoriesOMT satisfiability modulo theoriesSMT floating-point arithmetic attractor dynamic attractor
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Deciding floating-point logic with abstract conflict driven clause learning
- Propagation based local search for bit-precise reasoning
- Exploring approximations for floating-point arithmetic using UppSAT
- \textsc{OptiMathSAT}: a tool for optimization modulo theories
- Optimization modulo the theory of floating-point numbers
- An approximation framework for solvers and decision procedures
- Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
- Optimization Modulo Theories with Linear Rational Costs
- Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
- Approximations for Model Construction
- Satisfiability Modulo the Theory of Costs: Foundations and Applications
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
- A Modular Approach to MaxSAT Modulo Theories
- Symbolic optimization with SMT solvers
- A Decision Procedure for Bit-Vectors and Arrays
- On SAT Modulo Theories and Optimization Problems
This page was built for publication: Optimization modulo the theories of signed bit-vectors and floating-point numbers