z3pysolver.check（）当我增加位向量的长度时从“饱和”变为“未知”

Question

我想用Z3中的位向量分解数字n。我使用Bitvectores是因为我想限制p和q中的单个位。这个简单的例子确实起作用，求解器返回“ sat”。

from z3 import *

Bits = 32

n = 12
p_vec = BitVec('p', Bits)
q_vec = BitVec('q', Bits)
n_vec = BitVecVal(n,Bits)

s = Solver()
s.add(p_vec * q_vec == n_vec)
s.add(p_vec > 1, q_vec > 1)
s.add(BVMulNoOverflow(p_vec,q_vec,False))

print (s.check())

但是现在我想用4096位分解另一个数字n。因此，我在示例中将Bits = 4096更改为相同的数字。求解器现在给我“未知”而不是“星期六”。似乎求解器在某个时候停止了。我是否需要更改一些求解器设置，还是有其他方法可以做到这一点？

Answer 1

当我用Bits = 4096运行程序时，它会not说unknown。它只是不能很快完成（我等了几分钟），我也不希望这样。

位向量求解器已完成。也就是说，如果您等待足够长的时间，它会最终返回sat或unsat，前提是您不会耗尽内存（和耐心）。但是，对于这个问题，您要等待的数量实际上是无限的，并且很可能在此之前很久就耗尽了计算机的内存。因此，我不确定您如何获得该unknown。也许您正在使用某些超时选项，或者您未在此处显示其他内容。

您可以尝试添加以下形式的约束：p_vec < n和q_vec < p_vec以破坏对称性。由于n是一个常数，因此在某些情况下确实可以提供帮助。但这通常是徒劳的，对于在密码学实践中使用的任何合理位长，求解器实际上将永远循环。

基于明显的原因，分解是一个困难的问题，SMT求解器绝对是不是正确的工具。参见此处进行更早的讨论：Bitvector function Z3