我试图了解如何使用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位，并且由于将很多乘法与二进制混合在一起，该函数的推理可能非常复杂算术运算，所以我想知道是否有可能通过超越来证明它，也许会更快。
究竟是更快还是是否有一种有效解决此问题的方法可能是另一个问题，但是我一直在思考如何通过超越来证明这一点，那就是让Z3找到M这样一个f(N) != M forall N。
这与证明内射性有什么不同吗？
我如何在Z3的python绑定中声明它？
是否有可能将所有存在的限定词从该否定性陈述中删除？
有没有更有效的方法来证明一个函数是双射的？因为对于像这样的东西，蛮力搜索可能会更有效，因为对于32位向量来说所需的内存应该不会很大，但是这种方法肯定不适用于64位输入/输出。
您将按如下所示写出整体性：
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等）将提供更好的平台（以自动化程度较低为代价）来进行这些证明。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句