Solving the floating-point equation $x \otimes y = 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.

翻译：解决浮动点方程式 $x otimes y = z$, 美元、 美元和 z美元属于浮动点间隔, 是自动推理中一项共同任务, 通常不为任何有效的算法所了解。 我们显示, 可以通过计算固定的浮点系数来解决这个问题, 并给出快速算法, 用于计算 raidx 2 中正常浮动点数的连续正常浮动点系数 。 这导致解决特定方程式的有效程序, 与浮点乘法同步运行 。