Finding normal binary floating-point factors efficiently

DOI10.1007/S10817-023-09659-1MaRDI QIDQ6156639zbMATH OpenOpenAlexFDO

Authors Mak Andrlon

Publication date 14 June 2023

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2106.05631

zbMATH Keywords

decision proceduresinterval multiplicationfloating-point equation solving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: Solving the floating-point equation $xotimesy=z$, where $x$, $y$ and $z$ belong to floating-point intervals, is a common task in automated reasoning for which no efficient algorithm is known in general. We show that it can be solved by computing a constant number of floating-point factors, and give a fast algorithm for computing successive normal floating-point factors of normal floating-point numbers in radix 2. This leads to an efficient procedure for solving the given equation, running in time of the same order as floating-point multiplication.

Recommendations

• scientific article; zbMATH DE number 3856292
• Computing absolutely normal numbers in nearly linear time
• Exploiting structure in floating-point arithmetic
• Faster deterministic integer factorization
• Asymptotically Fast Factorization of Integers
• Algorithms for efficient reproducible floating point summation
• Factoring polynomials using binary representations of finite fields
• scientific article; zbMATH DE number 40800
• Fast evaluation and root finding for polynomials with floating-point coefficients

Cites work

• scientific article; zbMATH DE number 2185690 (Why is no real title available?)
• scientific article; zbMATH DE number 1863384 (Why is no real title available?)
• A parameterized floating-point formalizaton in HOL Light
• Accurate Floating-Point Summation Part I: Faithful Rounding
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• Exploiting binary floating-point representations for constraint propagation
• Floating-point arithmetic in the Coq system
• Formal Methods for Hardware Verification
• Formal verification of the VAMP floating point unit
• Handbook of floating-point arithmetic
• Optimal inverse projection of floating-point addition

This page was built for publication: Finding normal binary floating-point factors efficiently

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