使用 Z3 证明函数是满射的

Question

我正在尝试了解如何使用 Z3 有效地证明一个有点简单的函数 f : u32 -> u32 是双射的：

def f(n):
    for i in range(10):
        n *= 3
        n &= 0xFFFFFFFF # Let's treat this like a 4 byte unsigned number
        n ^= 0xDEADBEEF
    return n

我已经知道它是双射的，因为它是通过双射函数的组合获得的，所以这更像是一个计算问题。

现在，知道域和余域是有限的并且大小相同，我首先想到通过让 Z3 找到它是单射的反例来做到这一点：

N = BitVec('N', 32)
M = BitVec('M', 32)
solve(N != M, f(N) == f(M))

然而，这会花费相当长的时间（> 10 分钟，但会在之后关闭），这是合理的，因为搜索 space 几乎是 64 位的，并且函数可能非常复杂，无法推理因为它混合了很多乘法和二进制运算，所以我想知道是否可以通过满射来证明它，也许结果更快。

这是否真的更快，或者是否有有效解决这个问题的方法可能是另一个问题，但我一直在思考如何通过满射来证明它，那就是让 Z3 找到一个 M这样 f(N) != M forall N。

这与证明单射性有什么不同吗？

如何在 Z3 的 python 绑定中声明它？

是否可以完全从满射语句中删除存在限定词？

是否有更有效的方法来证明一个函数是双射的？因为对于这样的东西，暴力搜索可能更有效，因为 32 位向量所需的内存应该不会很多，但这种方法肯定不适用于 64 位 input/outputs.

Answer 1

你可以这样写满射性：

N = BitVec('N', 32)
M = BitVec('M', 32)
s = Solver()
s.add(ForAll([N], f(N) != M))

r = s.check()
if r == sat:
    print(s.model())
else:
    print(r)

不幸的是，将量词添加到位向量通常会使逻辑无法确定，z3 在我的机器上大约 10 秒后就放弃了：

unknown

一般来说，添加量词只会使 z3（或与此相关的任何其他 SMT 求解器）的问题变得非常困难。您的原始编码为：

solve(N!=M, f(N) == f(M))

可能是解决此问题的最佳方式。事实上，如果您将范围从 10 更改为更小的值（我试过最多 3），z3 会相对快速地回答 unsat。但很明显，求解器时间会随着函数中迭代次数的增加呈指数增长 f。

SMT 求解器可能不是证明这样的属性的最佳工具。你当然可以表达这样的约束，但充其量你会得到 unknown 作为答案，最坏的情况是它会永远循环。一个合适的定理证明器（如 Isabelle、HOL、Coq、ACL2 等）将提供一个更好的（以自动化程度较低为代价）平台来进行这些证明。

使用 Z3 证明函数是满射的

Prove a function is surjective using Z3

z3

z3py