Z3求解器中决定优化精度的重要决策因素是什么？

Question

为了使用 Z3 求解器获得优化解决方案，我学习了 2 种优化方法。一种是使用带有“MkMaximize”或“MkMinimize”指令的优化求解器。另一种是使用带有通用求解器的优化器方法作为问题[优化超时1]描述。

我发现有时存在不一致，好吧，我习惯了优化器方法可以得到更准确的答案，而优化求解器的优化方法是有限的。但是我发现这种不一致并不是永久性的，有时用两种方法生成的解决方案可能是相同的。

我想知道是哪个决定了两种方法之间的不一致，是约束的制定还是目标的制定？我想了解导致优化求解器不准确的原因。

添加示例：

      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());
 }

这个例子很长。 'mkMinimize' 指令的结果是 557，但是当我使用 'o.Add(ctx.mkLt(time, ctx.mkInt(550)));' 的约束时。它仍在工作并生成 549 的结果。

Answer 1

不幸的是，很难准确地理解您要询问的内容。但根据 cmets，我收集到您说正在发生以下情况：

1. 您使用 z3 的优化器，它会为您提供最小值
2. 您在求解器周围循环，要求一个小于该最小值但仍满足您的所有约束条件的值。 Solver 说 sat 并为您提供更好的价值。

如果是这种情况，那么应该报告 z3 中的错误。如果优化器返回了一个值，那么它确实是最优值：不应该有一个“更好”（即更小/更大，具体取决于您正在执行的优化）来满足您的约束。

但从您的描述中无法判断是否是这种情况。如果您实际上将 Stackoverflow 减少到显示问题的最小示例，以便人们可以复制问题，则 Stackoverflow 效果最好。您可能还会遇到一些导致您误入歧途的与编码相关的问题。但是，如果您确定以上是正在发生的事情，那么这就是 z3 上的一个错误，您应该在他们的错误跟踪器中报告它，并提供尽可能小的示例。 (https://github.com/Z3Prover/z3/issues)