1

I'm currently computing the weight of bitvectors using the python api for z3.

After searching through the python API for more straight forward method, I'm implementing the weight function for a bitvector st1 in the following manner:

Sum([( (st1 & (2**(i)))/(2**(i)) ) for i in range(bits)])

My question is relatively straight-forward, is there an easier/more efficient way?

I have problems which contain 1500+ of these weight constraints and would like to make sure I'm doing things as efficiently as possible.

Edit: I'll add the following clarification, what I'm attempting to calculate has a name (it's the Hamming Weight), I know there are ultra efficient ways of implementing the functionality in imperative languages, but ultimately what I'm looking for is if there are any underlying methods to access individual bits of a z3 bitvector.

mborowczak
  • 181
  • 10

2 Answers2

1

I played a little bit with the example you posted in the question:

I believe the unsat instances are hard to solve because the problem seems to have many symmetries. If that is the case, we can improve the performance by including "symmetry breaking constraints". Z3 can't break the symmetries automatically for this kind of problem.

Here is a minor encoding improvement. The expression ((st1 & (2**(i)))/(2**(i)) is essentially extracting the i-th bit. We can use Extract(i, i, st1) to extract the i-th bit. The result is a Bit-vector of size 1. Then, we have to "expand" it to avoid overflows. The bit-vectors in your problem have at most 28 bits. So, 5 bits is enough to avoid overflows. Therefore, we can use ZeroExt(4, Extract(i, i, st1)). That is, we replace

Sum([( (st1 & (2**(i)))/(2**(i)) ) for i in range(bits)])

with

Sum([ ZeroExt(4, Extract(i,i,st1)) for i in range(bits) ])

I get a modest 2x speedup. So, Z3 still cannot solve the 6 bits unsat instance :(

Community
  • 1
  • 1
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thanks for taking the time to look at this for me - I appreciate the encoding enhancement suggestion - I'll look to see if I can come up with "symmetry breaking constraints" for my problem sets. – mborowczak Feb 07 '13 at 06:39
-1

You should try with recursive method and maybe you could take a look at this Dynamic programming

jdurango
  • 533
  • 1
  • 4
  • 15
  • unfortunately recursion probably won't work here. In most imperative languages, e.g c/c++/python/ruby/java, it's often costlier in memory usage not to overkill when dealing with linear data/data structures. Now if you want to see how to implement a lazy evaluation scheme in an imperative language, check out this [c++ code](https://github.com/borowcm/Sandbox-Nemesis/blob/master/lazyStream/scLazyStreamEx.cc) with the [associated paper](http://bit.ly/TKbNBJ). – mborowczak Feb 06 '13 at 15:12