UTVPI 约束的增量可满足性与蕴含判定

每不等式含两个变量的单元约束（UTVPI）构成了最大类的整数约束之一，其在多项式时间内可解（除非 P=NP）。人们在约束求解、抽象解释、空间数据库和定理证明等领域对其应用抱有浓厚兴趣。本文开发了一种新的 UTVPI 约束可满足性及蕴含判定的增量算法，该算法在增量检查 $n$ 个变量上 $m$ 个 UTVPI 约束的可满足性以及检查 $p$ 个 UTVPI 约束的蕴含关系时，需要 $O(m + n \log n + p)$ 的时间和 $O(n+m+p)$ 的空间。