Z3 Solver Java API:意外行为 [英] Z3 Solver Java API: Unexpected behaviour

问题描述

通过向求解器添加条件，我想用solver.check()"检查是否存在解决方案.因此，我创建了一个简单的示例来为 t1 找到解决方案.我知道 t1 有一个解，即 t1 = 0.然而，解算器没有状态满足".

By adding conditions to the solver, I want to check with "solver.check()", whether there exists a solution or not. Therefore, I created a simple example to find a solution for t1. I know that there is a solution for t1, namely t1 = 0. Nevertheless, the solver has not the status "SATISFIABLE".

public static void main(String[] args) {
        int h_max = 7;
        HashMap<String, String> cfg = new HashMap<String, String>();
        cfg.put("model", "true");
        Context ctx = new Context(cfg);
        FPSort s = ctx.mkFPSort(5, 20);
        Solver solver = ctx.mkSolver();
        Model model = null;

        // Initialize constants
        RealExpr half = ctx.mkFPToReal(ctx.mkFP(0.5, s));
        RealExpr g = ctx.mkFPToReal(ctx.mkFP(9.81, s));
        RealExpr hmax = ctx.mkInt2Real(ctx.mkInt(h_max));
        RealExpr v = ctx.mkFPToReal(ctx.mkFP((Math.sqrt(2*h_max*9.81)), s));

        // Create query Information
        RealExpr q2 = ctx.mkReal(1);
        RealExpr q2Min = (RealExpr) ctx.mkSub(q2, half);
        RealExpr q2Max = (RealExpr) ctx.mkAdd(q2, half);

        // Initialize constraints 
        RealExpr tmax = ctx.mkFPToReal(ctx.mkFP((Math.sqrt(2*h_max/9.81)), s));
        RealExpr t0 = ctx.mkReal(0);

        // Initialize sampling interval
        RealExpr ts = ctx.mkFPToReal(ctx.mkFP(Math.sqrt(2*h_max/9.81)+0.1, s));

        // Variable t1
        RealExpr t1 = ctx.mkRealConst("t1");

        // 0 <= t1 <= tmax
        BoolExpr c1 = ctx.mkGe(t1, t0);
        BoolExpr c2 = ctx.mkLe(t1,tmax);

        // Elapsed Times
        RealExpr tE = (RealExpr) ctx.mkAdd(ts, t1);

        // Add conditions to solver
        solver.add(c1);
        solver.add(c2);

        // Calculating tE2 % tmax, since tE2 > tmax
        RealExpr quotient = (RealExpr) ctx.mkDiv(tE, tmax);
        IntExpr factor = ctx.mkReal2Int(quotient);
        RealExpr t2 = (RealExpr) ctx.mkSub(tE, ctx.mkMul(factor, tmax));

        // Calculating the observation h2 with t2.
        RealExpr h2 = (RealExpr) ctx.mkSub(ctx.mkMul(v,t2), ctx.mkMul(half, t2, t2, g));

        // Defining constraint q2Min <= h2 < q2Max
        BoolExpr c3 = ctx.mkAnd(ctx.mkGe(h2, q2Min),ctx.mkLt(h2, q2Max));

        solver.add(c3);

        //System.out.println("solver c1: " + solver.check(c1));
        //System.out.println("solver c2: " + solver.check(c2));
        //System.out.println("solver c3: " + solver.check(c3));

        if (solver.check() == Status.SATISFIABLE) {
            model = solver.getModel();
            System.out.println("System is Satisfiable");
        }
        else {
            System.out.println("Unsatisfiable");
        }

    ctx.close();
    }

我发现了一些意想不到的行为.如果我在执行solver.check()"之前尝试检查条件，例如

I discovered some unexpected behaviour. If I try to check conditions before I do "solver.check()", for example

System.out.println("solver c2: " + solver.check(c2));
System.out.println("solver c3: " + solver.check(c3));

它输出:

solver c2: UNKNOWN
solver c3: UNKNOWN

突然间，求解器的状态变为令人满意".但是如果我事先只检查一个条件，状态仍然是UNSATISFIABLE".

and suddenly, the solver's status is "SATISFIABLE". But if I only check one condition beforehand, the status is still "UNSATISFIABLE".

除此之外，如果我改变了

Other than that, if I change from

t1 = ctx.mkRealConst("t1");

到

t1 = ctx.mkReal(0);

求解器也找到了一个解，求解器状态为SATISFIABLE".

the solver also finds a solution and the solver status is "SATISFIABLE".

为什么求解器有这种行为，我怎么可能让求解器找到解决方案?有什么其他方法可以尝试吗?

Why does the solver have this behaviour and how could I possibly make the solver find a solution? Are there any alternative ways that I could try?

推荐答案

一般来说，当你写:

solver.check(c1)

您不是要求 z3 检查 c1 是否可满足.您要求 z3 做的是检查您输入的所有断言是否可满足，假设 c1 为真.这称为在假设下检查"并记录在此处:rel="nofollow noreferrer.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a71882930969215081ef020ec8fec45f3

you are not asking z3 to check that c1 is satisfiable. What you are asking z3 to do is to check that all the assertions you put in are satisfiable assuming c1 is true. This is called "check under assumptions" and is documented here: https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a71882930969215081ef020ec8fec45f3

这起初可能会相当混乱，但它允许检查假设下的可满足性，而不必全局断言这些假设.

This can be rather confusing at first, but it allows checking satisfiability under assumptions without having to assert those assumptions globally.

关于你为什么得到 UNKNOWN.您正在使用浮点运算，并将其与实数混合和匹配.这将产生很多非线性约束，z3 并不能很好地处理这些约束.尽量保持逻辑分离:如果可以，不要将实数与浮点数混合.(如果您对如何建模有疑问，请单独提问.)

Regarding why you get UNKNOWN. You are using floating-point arithmetic, and mixing and matching it with real's. That will create a lot of non-linear constraints, something that z3 doesn't really deal with all that well. Try to keep the logics separated: Don't mix reals with floats if you can. (Ask a separate question if you have questions regarding how to model things.)

最后，编写 t1 = ctx.mkReal(0) 与编写 t1 = ctx.mkRealConst("t1") 非常不同.第一个更容易处理:t1 只是 0.在第二种情况下，它是一个变量.因此，前者导致 z3 更容易处理的问题也就不足为奇了.同样，没有灵丹妙药，但首先不要以这种方式混合逻辑:如果您想处理浮点，请将所有内容保留在该土地上.如果你想用真正的价值观工作，就让一切都真正有价值.这样你会获得更多的里程.如果您必须将两者混合使用，那么您很可能会看到 UNKNOWN 结果.

Finally, writing t1 = ctx.mkReal(0) is very different than writing t1 = ctx.mkRealConst("t1"). The first one is much simpler to deal with: t1 is just 0. In the second case it's a variable. So, it isn't surprising at all that the former leads to much easier problems to handle for z3. Again, there's no silver bullet but start with not-mixing the logics this way: If you want to work on floating-point, keep everything in that land. If you want to work with real values, keep everything real valued. You'll get much more mileage that way. If you have to mix the two, then you'll most likely see UNKNOWN results.

这篇关于Z3 Solver Java API:意外行为的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！