How to improve binary search based optimization in Z3py

I am trying to optimize with Z3py an instance of Set Covering Problem (SCP41) based on minimize.

The results are the following:

Using

(1) I know that Z3 supports optimization (https://rise4fun.com/Z3/tutorial/optimization). Many times I get to the optimum in SCP41 and others instances, a few do not.

(2) I understand that if I use the Z3py API without the optimization module I would have to do the typical sequential search described in (Minimum and maximum values of integer variable) by @Leonardo de Moura. It never gives me results.

My approach

(3) I have tried to improve the sequential search approach by implementing a binary search similar to how it explains @Philippe in (Does Z3 have support for optimization problems), when I run my algorithm it waits and I do not get any result.

I understand that the binary search should be faster and work in this case? I also know that the instance SCP41 is something big and that many restrictions are generated and it becomes extremely combinatorial, this is my full code (Code large instance) and this is my binary search it:

def min(F, Z, M, LB, UB, C):    
    i = 0
    s = Solver()

    s.add(F[0])
    s.add(F[1])
    s.add(F[2])
    s.add(F[3])
    s.add(F[4])
    s.add(F[5])

    r = s.check()

    if r == sat:
        UB = s.model()[Z]

        while int(str(LB)) <= int(str(UB)):

            C = int(( int(str(LB)) + int(str(UB)) / 2))

            s.push()
            s.add( Z > LB, Z <= C)

            r = s.check()

            if r==sat:
                UB = Z
                return s.model()
            elif r==unsat:
                LB = C
                s.pop()

            i = i + 1
            if (i > M):
                raise Z3Exception("maximum not found, maximum number of iterations was reached")
    return unsat

And, this is another instance (Code short instance) that I used in initial tests and it worked well in any case.

What is incorrect binary search or some concept of Z3 not applied correctly?

regards, Alex

I don't think your problem is to do with minimization itself. If you put a print r after r = s.check() in your program, you see that z3 simply struggles to return a result. So your loop doesn't even execute once.

It's impossible to read through your program since it's really large! But I see a ton of things of the form:

 Or(X250 == 0, X500 == 1)

This suggests your variables X250 X500 etc. (and there's a ton of them) are actually booleans, not integers. If that is indeed true, you should absolutely stick to booleans. Solving integer constraints is significantly harder than solving pure boolean constraints, and when you use integers to model booleans like this, the underlying solver simply explores the search space that's just unreachable.

If this is indeed the case, i.e., if you're using Int values to model booleans, I'd strongly recommend modelling your problem to get rid of the Int values and just use booleans. If you come up with a "small" instance of the problem, we can help with modeling.

If you truly do need Int values (which might very well be the case), then I'd say your problem is simply too difficult for an SMT solver to deal with efficiently. You might be better off using some other system that is tuned for such optimization problems.