模块差分逻辑很困难
摘要：机器算术中与我们有关的是形如 x + k ≤ y + k' 的约束系统。在整数上，对于这样的系统，可满足性问题是多项式时间的。如果我们限制注意力在一个固定模数 N 的残余上，该问题则变得 NP 完全。
作者：Nikolaj Bj{o}rner (1), Andreas Blass (2), Yuri Gurevich (1), and Madan Musuvathi (1)
论文ID：0811.0987
分类：Computational Complexity
分类简称：cs.CC
提交时间：2008-11-07