What is the important decision factors deciding the optimization accuracy in Z3 solver ？

Question

To get a optimizing solution using Z3 solver, I have learned 2 methods for optimization. The one is using the optimizing solver with the instructions "MkMaximize" or "MkMinimize". The other is to use the optimizer method with general solver as the question [optimization timeout1 ] describing.

I find there exists inconsistency sometime, well, which I become used to learn that the optimizer method can get a more accurate answer while the optimizing method of optimizing solver is limited. But I come to find the inconsistency is not permanent, the solution generated with 2 methods can be same sometimes.

I wonder which decides the inconsistency between 2 methods, is the formulation of constraints or the objectives? And I'd like to get information that what leads to the inaccuracy in the optimizing solver.

Adding examples:

      Context ctx = new Context();
     Optimize o = ctx.mkOptimize();
     ArithExpr M1A10 = ctx.mkIntConst("M1A10");
     ArithExpr M2A10 = ctx.mkIntConst("M2A10");
     ArithExpr M3A10 = ctx.mkIntConst("M3A10");
     ArithExpr M1A20 = ctx.mkIntConst("M1A20");
     ArithExpr M2A20 = ctx.mkIntConst("M2A20");
     ArithExpr M3A20 = ctx.mkIntConst("M3A20");
     
     ArithExpr M1B10 = ctx.mkIntConst("M1B10");
     ArithExpr M2B10 = ctx.mkIntConst("M2B10");
     ArithExpr M3B10 = ctx.mkIntConst("M3B10");
     ArithExpr M1B20 = ctx.mkIntConst("M1B20");
     ArithExpr M2B20 = ctx.mkIntConst("M2B20");
     ArithExpr M3B20 = ctx.mkIntConst("M3B20");
     ArithExpr M1B30 = ctx.mkIntConst("M1B30");
     ArithExpr M2B30 = ctx.mkIntConst("M2B30");
     ArithExpr M3B30 = ctx.mkIntConst("M3B30");
     
     ArithExpr M1C10 = ctx.mkIntConst("M1C10");
     ArithExpr M2C10 = ctx.mkIntConst("M2C10");
     ArithExpr M3C10 = ctx.mkIntConst("M3C10");
     ArithExpr M1C20 = ctx.mkIntConst("M1C20");
     ArithExpr M2C20 = ctx.mkIntConst("M2C20");
     ArithExpr M3C20 = ctx.mkIntConst("M3C20");
     ArithExpr M1C30 = ctx.mkIntConst("M1C30");
     ArithExpr M2C30 = ctx.mkIntConst("M2C30");
     ArithExpr M3C30 = ctx.mkIntConst("M3C30");
     
     ArithExpr M1A = ctx.mkAdd(M1A10,M1A20);
        ArithExpr M2A = ctx.mkAdd(M2A10,M2A20);
        ArithExpr M3A = ctx.mkAdd(M3A10,M3A20);
        ArithExpr M1B = ctx.mkAdd(M1B10,M1B20,M1B30);
        ArithExpr M2B = ctx.mkAdd(M2B10,M2B20,M2B30);
        ArithExpr M3B = ctx.mkAdd(M3B10,M3B20,M3B30);   
        ArithExpr M1C = ctx.mkAdd(M1C10,M1C20,M1C30);
        ArithExpr M2C = ctx.mkAdd(M2C10,M2C20,M2C30);
        ArithExpr M3C = ctx.mkAdd(M3C10,M3C20,M3C30);

        ArithExpr M1z10= ctx.mkAdd(M1A10,M1B10,M1C10);
        ArithExpr M2z10= ctx.mkAdd(M2A10,M2B10,M2C10);
        ArithExpr M3z10= ctx.mkAdd(M3A10,M3B10,M3C10);

        ArithExpr M1z20= ctx.mkAdd(M1A20,M1B20,M1C20);
        ArithExpr M2z20= ctx.mkAdd(M2A20,M2B20,M2C20);
        ArithExpr M3z20= ctx.mkAdd(M3A20,M3B20,M3C20);

        ArithExpr M1z30= ctx.mkAdd(M1B30,M1C30);
        ArithExpr M2z30= ctx.mkAdd(M2B30,M2C30);
        ArithExpr M3z30= ctx.mkAdd(M3B30,M3C30);
        
        o.Add(ctx.mkGe(M1A10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1A20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2A10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2A20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3A10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3A20,ctx.mkInt(0)));
        
        o.Add(ctx.mkGe(M1B10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1B20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1B30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2B10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2B20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3B30,ctx.mkInt(0)));
        
        o.Add(ctx.mkGe(M1C10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1C20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M1C30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2C10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2C20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M2C30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C30,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C10,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C20,ctx.mkInt(0)));
        o.Add(ctx.mkGe(M3C30,ctx.mkInt(0)));


        o.Add(ctx.mkLt(M1z10,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M1z20,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M1z30,ctx.mkInt(80)));

        o.Add(ctx.mkLt(M2z10,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M2z20,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M2z30,ctx.mkInt(80)));

        o.Add(ctx.mkLt(M3z10,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M3z20,ctx.mkInt(80)));
        o.Add(ctx.mkLt(M3z30,ctx.mkInt(80)));
        
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1A10,ctx.mkInt(100)),ctx.mkMul(ctx.mkInt(200),M2A10),ctx.mkMul(ctx.mkInt(150),M3A10)), ctx.mkInt(20000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1A,ctx.mkInt(100)),ctx.mkMul(ctx.mkInt(200),M2A),ctx.mkMul(ctx.mkInt(150),M3A)), ctx.mkInt(40000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(ctx.mkAdd(M1B10,M1B20),ctx.mkInt(150)),ctx.mkMul(ctx.mkInt(300),ctx.mkAdd(M2B10,M2B20)),ctx.mkMul(ctx.mkInt(200),ctx.mkAdd(M3B10,M3B20))), ctx.mkInt(25000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1B,ctx.mkInt(150)),ctx.mkMul(ctx.mkInt(300),M2B),ctx.mkMul(ctx.mkInt(200),M3B)), ctx.mkInt(45000)));
        o.Add(ctx.mkGe(ctx.mkAdd(ctx.mkMul(M1C,ctx.mkInt(200)),ctx.mkMul(ctx.mkInt(250),M2C),ctx.mkMul(ctx.mkInt(200),M3C)), ctx.mkInt(30000)));

        ArithExpr time = ctx.mkAdd( M1A,M2A,M3A,M1B,M2B,M3B,M1C,M2C,M3C);
o.MkMinimize(time);
        //  o.Add(ctx.mkLt(time, ctx.mkInt(550)));
        o.Check();
        if(o.Check() == Status.SATISFIABLE)
        {
            
            M1A10=(ArithExpr) o.getModel().getConstInterp(M1A10).simplify();
            M1A20=(ArithExpr) o.getModel().getConstInterp(M1A20).simplify();
            M2A10=(ArithExpr) o.getModel().getConstInterp(M2A10).simplify();
            M2A20=(ArithExpr) o.getModel().getConstInterp(M2A20).simplify();
            M3A10=(ArithExpr) o.getModel().getConstInterp(M3A10).simplify();
            M3A20=(ArithExpr) o.getModel().getConstInterp(M3A20).simplify();
            
            M1B10=(ArithExpr) o.getModel().getConstInterp(M1B10).simplify();
            M1B20=(ArithExpr) o.getModel().getConstInterp(M1B20).simplify();
            M1B30=(ArithExpr) o.getModel().getConstInterp(M1B30).simplify();
            M2B10=(ArithExpr) o.getModel().getConstInterp(M2B10).simplify();
            M2B20=(ArithExpr) o.getModel().getConstInterp(M2B20).simplify();
            M2B30=(ArithExpr) o.getModel().getConstInterp(M2B30).simplify();
            M3B10=(ArithExpr) o.getModel().getConstInterp(M3B10).simplify();
            M3B20=(ArithExpr) o.getModel().getConstInterp(M3B20).simplify();
            M3B30=(ArithExpr) o.getModel().getConstInterp(M3B30).simplify();
            
            M1C10=(ArithExpr) o.getModel().getConstInterp(M1C10).simplify();
            M1C20=(ArithExpr) o.getModel().getConstInterp(M1C20).simplify();
            M1C30=(ArithExpr) o.getModel().getConstInterp(M1C30).simplify();
            M2C10=(ArithExpr) o.getModel().getConstInterp(M2C10).simplify();
            M2C20=(ArithExpr) o.getModel().getConstInterp(M2C20).simplify();
            M2C30=(ArithExpr) o.getModel().getConstInterp(M2C30).simplify();
            M3C10=(ArithExpr) o.getModel().getConstInterp(M3C10).simplify();
            M3C20=(ArithExpr) o.getModel().getConstInterp(M3C20).simplify();
            M3C30=(ArithExpr) o.getModel().getConstInterp(M3C30).simplify();
            
            ArithExpr timeA = ctx.mkAdd(M1A10,M1A20,M2A10,M2A20,M3A10,M3A20,M1B10,M1B20,M1B30,M2B10,M2B20,M2B30,M3B10,M3B20,M3B30,M1C10,M1C20,M1C30,M2C10,M2C20,M2C30,M3C10,M3C20,M3C30);
            
            System.out.println(timeA.simplify());
        }
        
        System.out.println(o.Check());
 }

The example is a long. The result of the the instruction 'mkMinimize' is 557, but when I use the constraint of 'o.Add(ctx.mkLt(time, ctx.mkInt(550)));'. it is still working and generate the result of 549.

It isn’t clear what you mean by “inconsistency.” These two methods are not supposed to be equivalent. If the internal optimizer works, then that’s great! The “loop around the solver” method is necessarily a limited approach. If you can provide a runnable example of what discrepancy you’re observing, you might get better responses. — alias, Nov 05 '20 at 15:46
Thanks for your comments. The example is so lengthy that I am hesitant to provide it. I will try to simplify it before I provide. Let me try to explain that. (The following example is in the integer domain) When the result R of optimizing objective O generated by the optimizing solver, I can find there exists satisfiability after adding an extra constraints such as add(O — 77Orange, Nov 06 '20 at 01:23
I used to think the inaccuracy of optimizing solver is common, but I come to find the sometimes the solution of 2 methods can be same. So I wonder what leads to the uncertain inaccuracy — 77Orange, Nov 06 '20 at 01:25
If the optimizing solver gave you a minimum value, but there is another satisfying value that's smaller, then that's a bug in z3 that you should report. — alias, Nov 06 '20 at 01:39
Does your problem contain non-linear constraints, by any chance? — Patrick Trentin, Nov 07 '20 at 18:41
Not exact non-linear constraints, I think. I have added the example. I wonder if you could check it again — 77Orange, Nov 15 '20 at 23:33
@77Orange I don't see the model-value of `time` being extracted and printed. Instead, I see `timeA` being printed. By any chance, could `557` be the value of `timeA` and not `time`? — Patrick Trentin, Dec 01 '20 at 23:02

score 0 · Answer 1 · answered Nov 06 '20 at 18:29

It's hard to decipher exactly what you are trying to ask, unfortunately. But based on the comments, I'm gathering that you are saying the following is happening:

You use z3's optimizer, and it gives you a minimum value
You loop around the solver, asking for a smaller than this minimum value that still satisfies all your constraints. Solver says sat and gives you a better value.

If this is the case, then it would be a bug in z3 that should be reported. If the optimizer returned you a value, then it is really the optimal: There should not be a "better" (i.e., smaller/larger depending on which kind of optimization you are doing) that satisfies your constraints.

But it is impossible to say if this is the case from your description. Stackoverflow works the best if you actually reduce it to a minimum example that exhibits the problem so people can replicate the issue. You might as well have some coding related problems that lead you astray. But if you are sure above is what's happening, than that's a bug on z3 and you should report it in their bug tracker with as small an example as you can come up with. (https://github.com/Z3Prover/z3/issues)

thanks for your help, I add the example. The example may be long, I have already add the 2 cases and one is in the comment. I wonder your help thanks — 77Orange, Nov 15 '20 at 23:31
You really need to provide minimum-complete repeatable examples. See here: https://stackoverflow.com/help/minimal-reproducible-example — alias, Nov 16 '20 at 00:25

What is the important decision factors deciding the optimization accuracy in Z3 solver ？

1 Answers1