API Z3 Solver Java: непредвиденное поведение - PullRequest
Новая
       73

API Z3 Solver Java: непредвиденное поведение

3 голосов
/ 03 апреля 2020

Добавляя условия в решатель, я хочу проверить с помощью solver.check (), существует ли решение или нет. Поэтому я создал простой пример, чтобы найти решение для t1. Я знаю, что есть решение для t1, а именно t1 = 0. Тем не менее, решатель не имеет статуса «УДОВЛЕТВОРЕННЫЙ». 

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");

на 

t1 = ctx.mkReal(0);

решатель также находит решение, и статус решателя «УДОВЛЕТВОРЕН».

Почему решатель имеет такое поведение и как я могу заставить решатель найти решение? Есть ли альтернативные способы, которые я мог бы попробовать?

1 Ответ

1 голос
/ 03 апреля 2020

В общем случае, когда вы пишете: 

solver.check(c1)

, вы не просите z3 проверить, что c1 выполнимо. То, что вы просите z3 сделать, это проверить, что все введенные вами утверждения являются выполнимыми, предполагая, что c1 верно. Это называется «проверка по допущениям» и задокументировано здесь: https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a71882930969215081ef020ec8fec45f3

Поначалу это может быть довольно запутанным, но позволяет проверять выполнимость при допущениях без необходимости утверждать эти допущения глобально .

Относительно того, почему вы получаете UNKNOWN. Вы используете арифметику с плавающей точкой c и смешиваете ее с реальными. Это создаст множество нелинейных ограничений, то, что z3 на самом деле не так хорошо справляется. Постарайтесь разделить логику: не смешивайте реалы с поплавками, если можете. (Задайте отдельный вопрос, если у вас есть вопросы относительно того, как моделировать вещи.)

Наконец, написание t1 = ctx.mkReal(0) сильно отличается от написания t1 = ctx.mkRealConst("t1"). С первым гораздо проще иметь дело: t1 - это просто 0. Во втором случае это переменная. Так что совсем не удивительно, что первое приводит к гораздо более простым задачам для z3. Опять же, нет серебряной пули, но начните с того, что не смешивайте логику следующим образом: если вы хотите работать с плавающей точкой, держите все на этой земле. Если вы хотите работать с реальными ценностями, держите все по-настоящему ценным. Таким образом, вы получите гораздо больше пробега. Если вам нужно смешать два, то вы, скорее всего, увидите UNKNOWN результаты.

...