SMTlib non overlapping but complementary Bitvectors

Question

I am struggling with the attempt to generate a correct assertion in SMTlib. The QV_BV (Bitvectors) theory is used. I use Python to generate the temp.smt2 file and then run it using z3. The goal is to assert that among an arbitrary number of vectors:

1. Pairwise conjunction must be #b0000000...00, i.e all zeroes
2. Total disjunction must be #b1111111...11, i.e all ones

Roughly speaking, each vector represents the timetable of an employee, and the requirements are that all timetable slots must be taken by only one employee at a time, but all slots must be taken.

Examples are as follows:

(1)   |  (2)   |  (3)
      |        |
1010  |  1000  |  1000
1001  |  0100  |  0110
0100  |  0010  |  0001
----  |  ----  |  ----   <--- "disjunction"
1111  |  1110  |  1111
      |        | 
fail  |  fail  |  sat! 

Example 1 is UNSAT, because, despite the fact that all slots are occupied, there is a collision between the first two bit-vectors

Example 2 is UNSAT because not all the slots are taken. The LSB of a result is 0.

Example 3 is SAT because all slots are taken and no collisions.

I attempted the following approach (N and M are arbitrary numbers):

(set-logic QF_BV)

(declare-const x0 (_ BitVec M))
(declare-const x1 (_ BitVec M))
...
(declare-const xN (_ BitVec M))

(assert (= #b00000...00 (bvand x0 x1 ... xN)))
(assert (= #b11111...11 (bvor x0 x1 ... xN)))

(check-sat)
(get-model)

Only later did I notice that this is insufficient. The disjunction (OR-ing) of overlapping ones is allowed. Then I considered other bitwise operations I got lost quickly. For example, XOR-ing more than one term can be unpredictable, since:

xor(1, 0, 1, 0, 1) == xor(1, xor(0, xor(1, xor(0, 1)))) == 0
xor(1, 0, 1, 1) == xor(1, xor(0, xor(1, 1))) == 1

I can use Python to generate each pairwise assertion in the smt2 file. But since I have arbitrary many bit-vectors, it may lead to high complexity. For example, given 100 bit-vectors, there are 4950 pairs, therefore 4950 assertions. I hope we can do better than that.

So what is a possible solution? Thank you!

Edit: Note that I am not using z3py. I am writing to .smt2 file

Answer 1

Your best bet is to keep NxM booleans, instead of N M-bit vectors. Then you want to assert exactly one of each column is set. (Note that you don't need to or them anymore, because the first constraint will handle that.)

To assert exactly one of them is true, you can use PbEq, which is supported by z3. Or you can add 1 for each set boolean, and assert the sum is 1, if you want to be generic.

Note that you can still have bit-vectors if you want, if that helps in some other part of the problem. If that's the case, also create NxM booleans and set them correspondingly. (Using calls to extract.) And then you can have both representations and use whichever is most suitable.

PS: You said you're not using z3py. If you did, that'd definitely simplify your coding. Note that you can always convert a z3py program to simple SMTLib using the sexpr method of the solver. Unless you've some other reason not to do so, I'd definitely go with that.