使用 z3 的模块化算法

问题描述

我试图证明如下陈述：

(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 标志的方向？

解决方法

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

有关详细信息，请参阅此答案： How does Z3 handle non-linear integer arithmetic?

你能做什么

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

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

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

在实践中，我建议改为证明您财产的特定实例。也就是说，运行一堆案例，每次修复 n：

(assert (= n 10))

然后

(assert (= n 27))

等等。显然，这不能证明所有 n，但在实际系统中，如果您仔细选择 n 的值，您可以剔除很多非定理这样。

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

integer integer integer modulo smt z3