Z3: Hamming Distance between two bit vectors

1
votes

Is there an efficient way to find Hamming Distance between two BitVec() in Z3? That is, two equal length BitVectors that differ by a certain number of bits in their respective positions. I am trying to use some Z3-APIs from here.

This is what I have tried until now:

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)

Now, above constraint should give "SAT" only when BitVecs V_1 & V_2 differ at 9 bit-positions. However, it also gives SAT when V_1='0', V_2='1' & V_1='00', V_2='10'

I'm afraid I'm over-complicating my constraint. Is there a simple way to find HD between two BitVecs?

I am a beginner in the field of SAT-solving and SMT solvers. I am currently trying out Z3 to learn and would appreciate any help in this regard. Thanks in advance!

FYI - for the above code this is the output I get when I run in loop to check with 0 < bit_length < 10. V_1, V_2 values are represented in binary for readability:

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: After debugging my constraints using simplify(), I got it working with ZeroExt(int(ceil(log(bit_length)/log(2))+ <HD_value>), ) That is, the above s.add() changed to:

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)

Nonetheless, I would continue to explore if I can find a better method. Feel free to post your answers if you know a better approach. Thanks!

2
z3smtz3py

2 Answers

2
votes

The bit-vector addition based encoding is often very good. There is an optimization that uses log(target)+1 bits by checking for overflows after every binary addition.

You can also use cardinality constraints. To force Z3 to use the same solver as it would as with the bit-vector constraints you would have to set the solver as follows:

    s = SolverFor("QF_FD")

To encode the constraints using cardinalities formulate the hamming constraints as follows:

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

I think what you're doing is just fine. But from a stylistic point; you might want to use a few functions to improve readability/reusability:

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)]

When I run this, I get:

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