Z3：两个位向量之间的汉明距离答案

【问题标题】：Z3: Hamming Distance between two bit vectorsZ3：两个位向量之间的汉明距离
【发布时间】：2018-04-24 00:15:27
【问题描述】：

有没有一种有效的方法来找到 Z3 中两个 BitVec() 之间的汉明距离？也就是说，两个长度相等的 BitVector 在它们各自的位置上相差一定数量的位。我正在尝试使用来自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

恐怕我的约束过于复杂了。有没有一种简单的方法可以在两个 BitVec 之间找到 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

更新：使用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)

不过，如果我能找到更好的方法，我会继续探索。如果您知道更好的方法，请随时发布您的答案。谢谢！

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

基于位向量加法的编码通常非常好。通过在每次二进制加法后检查溢出来使用 log(target)+1 位的优化。

您还可以使用基数约束。要强制 Z3 使用与位向量约束相同的求解器，您必须按如下方式设置求解器：

    s = SolverFor("QF_FD")

要使用基数对约束进行编码，请按如下方式制定汉明约束：

 def hamming(V1, V2, count):
 h = V1 ^ V2
     return PbEq([(Extract(i, i, h) == 1,1) for i in range(V1.size())], count)

【讨论】：

【解决方案2】：

我认为你所做的一切都很好。但从文体的角度来看；您可能想使用一些函数来提高可读性/可重用性：

from z3 import *

def hamming(V1, V2, target):
    h = V1 ^ V2
    s = max(target.bit_length(), V1.size().bit_length())
    return Sum([ZeroExt(s, Extract(i, i, h)) for i in range(V1.size())])

def test(bitLength, target):
    s = Solver()
    V1, V2 = BitVecs('V1 V2', bitLength)
    s.add(hamming(V1, V2, target) == target)
    print "Solving for bitLength = %d:" % bitLength,
    if s.check() == sat:
       print format(s.model()[V1].as_long(), "0%db" % bitLength),
       print format(s.model()[V2].as_long(), "0%db" % bitLength)
    else:
       print "No model found!"


# testing
[test(i, 9) for i in range(1, 10)]

当我运行它时，我得到：

Solving for bitLength = 1: No model found!
Solving for bitLength = 2: No model found!
Solving for bitLength = 3: No model found!
Solving for bitLength = 4: No model found!
Solving for bitLength = 5: No model found!
Solving for bitLength = 6: No model found!
Solving for bitLength = 7: No model found!
Solving for bitLength = 8: No model found!
Solving for bitLength = 9: 100100101 011011010

【讨论】：