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 constant-time algorithm for computing successive normal floating-point factors of normal floating-point numbers in radix 2. This leads to a constant-time procedure for solving the given equation.

翻译：解决浮动点方程式 $x otimes y = z$, 美元、 美元和 z美元属于浮动点间隔, 是自动推理中的一项共同任务, 通常并不知晓有效的算法。 我们显示, 可以通过计算固定数量的浮动点因子来解决这个问题, 并给出一个固定时间算法, 用于计算 raidx 2 中正常浮动点数的连续正常浮动点因子 。 这会导致解决特定方程的固定时间程序 。