optimizationz3minimizez3pybitvector

Z3 gives a different answer each time upon reordering parameters. Optimization problem

Each time I run my project, a different order of the Z3 formulae is generated. Even though the formula is exactly the same, it is reordered in different runs and as a result, the answers attained from Z3 are different in every run. This is causing issues since I need an optimal set which should be exactly the same in each run.

For example,

  1. the first run is:
(declare-const l1 (_ BitVec 1))
(declare-const l2 (_ BitVec 1))
(declare-const l3 (_ BitVec 1))
(declare-const l4 (_ BitVec 1))
(declare-const l5 (_ BitVec 1))
(declare-const l6 (_ BitVec 1))
(declare-const l7 (_ BitVec 1))
(declare-const l8 (_ BitVec 1))
(declare-const l9 (_ BitVec 1))
(declare-const l10 (_ BitVec 1))

(minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))

(maximize 
    (bvand 
        (bvor (bvand l3 l4 l1 l2) (bvand l4 l2) (bvand l4 l1 l2) (bvand l2 l3 l4)) 

        (bvor (bvand l4 l2) (bvand l2 l3 l4)) 

        (bvor (bvand l5 l7 l8 l10 l6) (bvand l5 l7 l8 l6) (bvand l5 l7 l8 l9 l6) (bvand l5 l7 l8 l9 l10 l6) (bvand l5 l7 l6) (bvand l5 l7 l9 l10 l6) (bvand l5 l7 l10 l6))
    )
)
(check-sat)
(get-model)

which gives the solution: l7, l5, l2, l4, l6, l8.
6 are true in this case.

  1. the second run is:
(declare-const l1 (_ BitVec 1))
(declare-const l2 (_ BitVec 1))
(declare-const l3 (_ BitVec 1))
(declare-const l4 (_ BitVec 1))
(declare-const l5 (_ BitVec 1))
(declare-const l6 (_ BitVec 1))
(declare-const l7 (_ BitVec 1))
(declare-const l8 (_ BitVec 1))
(declare-const l9 (_ BitVec 1))
(declare-const l10 (_ BitVec 1))

(minimize (bvadd l1 l2 l3 l4 l5 l6 l7 l8 l9 l10))

(maximize 
    (bvand
        (bvor (bvand l2 l3 l4) (bvand l2 l4) (bvand l1 l2 l4) (bvand l2 l3 l4 l1)) 

        (bvor (bvand l2 l3 l4) (bvand l2 l4)) 

        (bvor (bvand l10 l6 l5 l7 l9) (bvand l10 l6 l5 l7) (bvand l10 l6 l5 l7 l8 l9) (bvand l10 l6 l5 l7 l8) (bvand l7 l6 l5) (bvand l7 l8 l9 l6 l5) (bvand l7 l8 l6 l5))
    )
)

(check-sat)
(get-model)

which gives the solution: l7, l9, l5, l2, l4, l6, l8, l3.
8 are true in this case.

For my project, I need an optimal, minimized set. I need the smallest possible number of variables to be true, based on the conditions explained before. For both of these runs, the correct, optimal answer should be: l2, l4, l5, l6, l7 (5 true). Basically I need to minimize the cost and satisfy the conditions inside the maximize condition.

However, instead of ever giving the optimal solution with 5 variables true, I obtain either 6, 8, 10 true values.
Something that I also tried was (assert (= (bvand ...) #b1) ) in place of (maximize (bvand ...) ), to no avail.

How can I obtain the minimum, optimum number of true variables that also satisfies the condition and gives the same result each time, even upon reordering?

note: I cannot use Int or Bool since my programs are likely going to be huge and int/bool would be unable to handle it.

Solution

  • There are a couple of issues here. First of all, you're minimizing the sum using bvadd, which performs machine arithmetic. That is it will overflow over the bit-vector size. (That is, the value is either 0 or 1 at all times.) To avoid this, do the addition over a larger bit-vector size:

    (define-fun ext ((x (_ BitVec 1))) (_ BitVec 8)
    ((_ zero_extend 7) x))

(minimize (bvadd (ext l1) (ext l2) (ext l3) (ext l4) (ext l5) (ext l6) (ext l7) (ext l8) (ext l9) (ext l10)))

    Here I've extended the values to 8-bits before adding: Since you have 10 variables, 8-bits is more than enough to represent the total of 10. (You can get away with 4-bits in this case as well; not that it'd matter much. Just make sure it's wide enough to represent to total number of variables you're adding.)

    But there's a second problem here. You're asking z3 to first minimize this sum, and then maximize your second expression. Z3 will do lexicographic optimization, meaning that it'll first handle your first constraint, and then use the second one. But your first one will make all of the variables 0, to minimize the sum. To avoid this, make sure you swap the order of the constraints.

    And as a final comment: You did explicitly say that "note: I cannot use Int or Bool since my programs are likely going to be huge and int/bool would be unable to handle it." I find that very dubious. For a problem like this a Bool would be the most obvious and optimal choice. In particular, the optimizer will have much easier time dealing with booleans than with bit-vectors and integers. So, I'd recommend not dropping that idea without actually experimenting and having some evidence that it does not scale.