距离的数量级比较

数量级推理——通过对量大小的粗略比较进行推理——通常被称为“信封背面计算”，这意味着这种计算虽然近似但很快速。本文展示了一类有趣的约束集，其中数量级推理被证明是快速的。具体而言，我们提出了一种多项式时间算法，能够求解形如“点a和点b之间的距离远小于点c和点d之间的距离”的约束集。我们证明，只要标度差异大于约束集中的变量数，无论将“远小于”解释为指代标度的无限差异还是指代标度的有限差异，该算法均适用。我们还证明了此类约束上的一阶理论是可判定的。