使用 z3 的模运算

Question

我正在尝试证明以下陈述：

(assert (=
    (mod i n)
    (mod j n)))

(assert (> n 0))
    
(assert (not (=
    (mod (+ i 1) n)
    (mod (+ j 1) n))))

(check-sat)
(get-model)

其他是：

• (((i % n) + j) % n) == ((i + j) % n)
• ((i - n + 1) % n) == ((i + 1) % n)
• ((((a - 1) % n) + 1) % n) == (a % n)

但是 z3 在证明这些陈述时似乎并没有终止。它们是否超出了 z3/smt 求解器的能力？

如果这是唯一的方法，我不介意做更明确的证明步骤，但这些规则看起来太简单了，我不知道从哪里开始。即使在使用归纳法时，我也很快遇到了我认为是正确的情况（如最初的示例），但似乎无法用 z3 证明。

我正在使用 z3 4.8.6，物有所值。任何人都可以解释一下为什么这很难，或者可能指出我的方向是使这可行的论文/z3标志？

Answer 1

长答案短，是的。这些属性对于 SMT 求解器来说太难处理了。它们本质上涉及非线性整数算术，没有决策程序。求解器有一堆内置的启发式方法，可能会也可能不会回答您的查询；但更常见的情况是它不会像你观察到的那样进入无限循环。

详情请参阅此答案： How does Z3 handle non-linear integer arithmetic?

你能做什么

如果您想坚持使用纯按钮解决方案，那么您真的无能为力。在某些情况下，以下行会有所帮助：

(check-sat-using (and-then qfnra-nlsat smt))

这使用实数理论来解决您的查询（NRA：非线性实数算术 - 恰好是可判定的），然后查看解决方案是否实际上是整数。显然，这并不总是有效。特别是像mod这样的操作，使用这种策略将很难处理。

在实践中，我建议改为证明您的属性的特定实例。也就是跑一堆case，每次都修复n：

(assert (= n 10))

然后

(assert (= n 27))

等等。显然，这并不能证明 all n，但在实际系统中，如果您仔细选择 n 的值，您可以通过这种方式剔除很多非定理。

如果您真的想为所有n 证明这一点，那么请改用定理证明器。显然这不会是按钮，但这是最先进的。这里有很多选择：Isabelle、HOL、HOL-Light、ACL2、Coq、Lean、.. 等等。请注意，这些定理证明者中的大多数都内置了利用 SMT 求解器在后台执行许多子目标的策略。因此，您可以两全其美，当然证明本身需要在此类系统中进行手动分解。