Z3 Solver Java API：意外行为

通过向求解器添加条件，我想使用“solver.check()”检查是否存在解。因此，我创建了一个简单的示例来寻找 t1 的解决方案。我知道 t1 有一个解，即 t1 = 0。然而，求解器的状态不是“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()”之前检查条件

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

它输出：

solver c2: UNKNOWN
solver c3: UNKNOWN

突然间，求解器的状态变为“可满足”。但如果我事先只检查一个条件，状态仍然是“无法满足”。

除此之外，如果我改变

t1 = ctx.mkRealConst("t1");

to

t1 = ctx.mkReal(0);

求解器也找到了一个解，并且求解器状态为“SATISFIABLE”。

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

一般来说，当你写：

solver.check(c1)

you are not要求 z3 检查c1是可以满足的。您要求 z3 做的是检查您输入的所有断言是否可满足，假设c1是真的。这称为“根据假设进行检查”并记录在此处：https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a71882930969215081ef020ec8fec45f3 https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a71882930969215081ef020ec8fec45f3

一开始这可能会相当令人困惑，但它允许检查假设下的可满足性，而不必在全局范围内断言这些假设。

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

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