有没有一种有效的方法可以找到Z3中两个 BitVec()
之间的汉明距离?也就是说,两个相等长度的BitVectors在它们各自的位置上相差一定的位数 . 我正在尝试使用here中的一些Z3-API .
这是我到现在为止所尝试的:
V_1, V_2 = BitVecs('V_1 V_2',bit_length) #bit_length varies from 1 to 9.
s.add(Sum([ZeroExt(int(ceil(log(bit_length)/log(2))+1), Extract(i,i,(V_1 ^ V_2))) for i in range(bit_length) ]) == 9)
现在,仅当BitVecs V_1和V_2在9位位置不同时,上述约束才应给出“SAT” . 但是,当V_1 ='0',V_2 ='1'且V_1 ='00',V_2 = '10'时,它也会给出SAT
我担心我的约束过于复杂 . 有两种简单的方法可以在两个BitVecs之间找到HD吗?
我是SAT求解和SMT求解器领域的初学者 . 我目前正在尝试Z3学习,并希望在这方面提供任何帮助 . 提前致谢!
仅供参考 - 对于上面的代码,这是我在循环中运行以检查 0 < bit_length < 10
时得到的输出 . V_1,V_2值以二进制表示,以提高可读性:
Sat, bit_length = 1,
V_1 -> 0
V_2 -> 1
Sat, bit_length = 2,
V_1 -> 00
V_2 -> 10
NotSat, bit_length = 3,
NotSat, bit_length = 4,
NotSat, bit_length = 5,
NotSat, bit_length = 6,
NotSat, bit_length = 7,
NotSat, bit_length = 8,
Sat, bit_length = 9,
V_1 -> 111011101
V_2 -> 000100010
UPDATE :在使用 simplify()
调试我的约束后,我使用了 ZeroExt(int(ceil(log(bit_length)/log(2))+ <HD_value>), )
,即上面的s.add()更改为:
s.add(Sum([ZeroExt(int(ceil(log(bit_length)/log(2))+9), Extract(i,i,(V_1 ^ V_2))) for i in range(bit_length) ]) == 9)
尽管如此,如果能找到更好的方法,我会继续探索 . 如果您知道更好的方法,请随时发布您的答案 . 谢谢!
2 回答
我觉得你做的很好 . 但是从文体的角度来看;您可能希望使用一些函数来提高可读性/可重用性:
当我运行这个时,我得到:
基于位向量加法的编码通常非常好 . 通过在每次二进制加法后检查溢出,有一个优化使用log(目标)1位 .
您还可以使用基数约束 . 要强制Z3使用与位向量约束相同的求解器,您必须按如下方式设置求解器:
使用基数编码约束来制定汉明约束,如下所示: