时间戳

首页 > 解决方案 > 使用 Z3 证明函数是满射的

z3 - 使用 Z3 证明函数是满射的

问题描述

我试图了解如何使用 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 分钟，但之后将其关闭），并且合理地如此，因为搜索空间几乎是 64 位，并且该函数可能非常复杂，因为它混合了很多乘法与二进制算术，所以我想知道是否有可能通过 surjection 来证明它，也许结果更快。

这是否实际上更快，或者是否有一种方法可以有效地解决这个问题可能是另一个问题，但是我一直在思考如何通过推测来证明它，那就是让 Z3 找到一个M这样的f(N) != M forall N.

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

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

是否有可能从满射陈述中删除存在限定词？

有没有更有效的方法来证明一个函数是双射的？因为对于这样的事情，蛮力搜索可能更有效，因为 32 位向量所需的内存不应该很多，但这种方法肯定不适用于 64 位输入/输出。

标签： z3z3py

解决方案

你可以这样写满射性：

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 等）将提供一个更好的（以自动化程度较低为代价）平台来进行这些证明。

推荐阅读