Какие важные факторы определяют точность оптимизации в решателе Z3？

Чтобы получить оптимизирующее решение с помощью решателя 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.


java z3 smt
person 77Orange    schedule 05.11.2020    source источник
comment
Непонятно, что вы имеете в виду под «непоследовательностью». Эти два метода не должны быть эквивалентными. Если внутренний оптимизатор работает, отлично! Метод «цикла вокруг решателя» обязательно является ограниченным подходом. Если вы можете представить работоспособный пример того, какое несоответствие вы наблюдаете, вы можете получить более точные ответы.   -  person alias    schedule 05.11.2020
comment
Спасибо за ваши комментарии. Пример настолько длинный, что я не решаюсь его приводить. Я постараюсь упростить его, прежде чем предлагать. Позвольте мне попытаться это объяснить. (Следующий пример находится в целочисленной области) Когда результат R оптимизации цели O сгенерирован оптимизирующим решателем, я могу обнаружить, что существует выполнимость после добавления дополнительных ограничений, таких как add (O ‹Z). То есть, если оптимизирующий решатель сообщает мне, что минимум 8, я все равно могу найти меньшее, используя метод «цикла вокруг решателя».   -  person 77Orange    schedule 06.11.2020
comment
Раньше я думал, что неточность оптимизирующего решателя является обычным явлением, но я пришел к выводу, что иногда решение двух методов может быть одинаковым. Поэтому мне интересно, что приводит к неопределенной неточности   -  person 77Orange    schedule 06.11.2020
comment
Если оптимизирующий решатель дал вам минимальное значение, но есть другое удовлетворительное значение, которое меньше, то это ошибка в z3, о которой вы должны сообщить.   -  person alias    schedule 06.11.2020
comment
Ваша проблема случайно не содержит нелинейных ограничений?   -  person Patrick Trentin    schedule 07.11.2020
comment
Я думаю, это не совсем нелинейные ограничения. Я добавил пример. Интересно, можете ли вы проверить это снова   -  person 77Orange    schedule 16.11.2020
comment
@ 77Orange Я не вижу, чтобы значение модели time было извлечено и распечатано. Вместо этого я вижу, как печатается timeA. Может ли 557 быть значением timeA, а не time?   -  person Patrick Trentin    schedule 02.12.2020

Ответы (1)


arrow_upward
0
arrow_downward

К сожалению, сложно понять, о чем вы пытаетесь спросить. Но, судя по комментариям, я понимаю, что вы говорите, что происходит следующее:

  1. Вы используете оптимизатор z3, и он дает вам минимальное значение
  2. Вы перебираете решатель, запрашивая меньшее, чем это минимальное значение, которое по-прежнему удовлетворяет всем вашим ограничениям. Решатель говорит sat и дает вам лучшее значение.

Если это так, то следует сообщить об ошибке в z3. Если оптимизатор вернул вам значение, то оно действительно оптимальное: не должно быть лучшего (т.е. меньшего / большего в зависимости от того, какой вид оптимизации вы выполняете), удовлетворяющего вашим ограничениям.

Но так ли это по вашему описанию сказать невозможно. Stackoverflow работает лучше всего, если вы фактически сведете его к минимуму, который демонстрирует проблему, чтобы люди могли ее воспроизвести. У вас также могут быть некоторые проблемы, связанные с кодированием, которые сбивают вас с пути. Но если вы уверены в том, что происходит выше, то это ошибка в z3, и вам следует сообщить об этом в их трекере ошибок с как можно меньшим примером. (https://github.com/Z3Prover/z3/issues)

person alias    schedule 06.11.2020
comment
спасибо за помощь, добавляю пример. Пример может быть длинным, я уже добавил 2 случая, и один находится в комментарии. Мне нужна ваша помощь, спасибо - person 77Orange; 16.11.2020
comment
Вам действительно нужно предоставить минимально полные повторяемые примеры. См. Здесь: stackoverflow.com/help/minimal-reproducible-example - person alias; 16.11.2020