잘못된 결과를주는 Z3 .NET API에서 최적화 - 버그?

Question

Z3 용 .NET API를 사용 중입니다. 코드 우물쭈물을 사용하여 이상한 동작 (아마도 최적화 프로그램의 버그)을 발견했습니다. Optimize 클래스를 사용하여 실행하면 솔루션을 잘못 찾게되는 반면 Solver 클래스를 실행하면 실행 불가능하다고 올바르게보고됩니다. 아무도 내 진술을 확인하기 위해 코드를 실행 해 주시겠습니까? 무슨 일이 일어나고 있는지 어떤 힌트라도 높게 평가 될 것입니다.

종류는 내가 마스터 지점의 현재 버전으로 버그를 재현하기 위해 노력했다

마렉

using System; 
using System.Collections.Generic; 
using Microsoft.Z3; 

namespace DS 
{ 
    class Program 
    { 
     static void Main(string[] args) 
     { 
      SMTtest smt = new SMTtest(); 
      if (smt.Solve()) 
      { 
       Console.WriteLine("Solved"); 
      } 
      else 
      { 
       Console.WriteLine("Infeasible"); 
      } 
     } 
    } 

    class SMTtest 
    { 
     public bool Solve() 
     { 
      using (Context ctx = new Context(new Dictionary<string, string>() { { "model", "true" } })) 
      { 
       Optimize optimizer = ctx.MkOptimize(); 
       //Solver optimizer = ctx.MkSolver(); 

       int numOfTasks = 19; 
       IntExpr[] time = new IntExpr[numOfTasks * 2]; 
       BoolExpr[] select = new BoolExpr[numOfTasks]; 

       for (int i = 0; i < numOfTasks; i++) 
       { 
        select[i] = ctx.MkBoolConst("valid" + i.ToString()); 
       } 
       for (int i = 0; i < numOfTasks * 2; i++) 
       { 
        time[i] = ctx.MkIntConst("time" + i.ToString()); 
       } 

       optimizer.Assert(ctx.MkEq(select[1], select[0])); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkLe(time[0], time[1]))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkGe(time[19], time[20]))); 
       optimizer.Assert(ctx.MkEq(select[8], select[0])); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkLe(time[0], time[8]))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkGe(time[19], time[27]))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkOr(ctx.MkEq(time[0], time[1]), ctx.MkEq(time[0], time[8])))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkOr(ctx.MkEq(time[19], time[20]), ctx.MkEq(time[19], time[27])))); 
       optimizer.Assert(ctx.MkEq(select[2], select[1])); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkLe(time[1], time[2]))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkGe(time[20], time[21]))); 
       optimizer.Assert(ctx.MkEq(select[5], select[1])); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkLe(time[1], time[5]))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkGe(time[20], time[24]))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkOr(ctx.MkEq(time[1], time[2]), ctx.MkEq(time[1], time[5])))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkOr(ctx.MkEq(time[20], time[21]), ctx.MkEq(time[20], time[24])))); 
       optimizer.Assert(ctx.MkImplies(select[3], ctx.MkEq(time[2], time[3]))); 
       optimizer.Assert(ctx.MkImplies(select[3], ctx.MkEq(time[21], time[22]))); 
       optimizer.Assert(ctx.MkImplies(select[4], ctx.MkEq(time[2], time[4]))); 
       optimizer.Assert(ctx.MkImplies(select[4], ctx.MkEq(time[21], time[23]))); 
       optimizer.Assert(ctx.MkEq(select[2], ctx.MkOr(select[3], select[4]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[3], select[4] }, 1)); 
       optimizer.Assert(select[3]); 
       optimizer.Assert(ctx.MkEq(time[3], ctx.MkInt(0))); 
       optimizer.Assert(ctx.MkEq(time[22], ctx.MkInt(4))); 
       optimizer.Assert(ctx.MkNot(select[4])); 
       optimizer.Assert(ctx.MkImplies(select[6], ctx.MkEq(time[5], time[6]))); 
       optimizer.Assert(ctx.MkImplies(select[6], ctx.MkEq(time[24], time[25]))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[5], time[7]))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[24], time[26]))); 
       optimizer.Assert(ctx.MkEq(select[5], ctx.MkOr(select[6], select[7]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[6], select[7] }, 1)); 
       optimizer.Assert(select[6]); 
       optimizer.Assert(ctx.MkEq(time[6], ctx.MkInt(0))); 
       optimizer.Assert(ctx.MkEq(time[25], ctx.MkInt(1))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkGe(time[7], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[26], ctx.MkAdd(time[7], ctx.MkInt(1))))); 
       optimizer.Assert(ctx.MkEq(select[9], select[8])); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkLe(time[8], time[9]))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkGe(time[27], time[28]))); 
       optimizer.Assert(ctx.MkEq(select[12], select[8])); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkLe(time[8], time[12]))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkGe(time[27], time[31]))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkOr(ctx.MkEq(time[8], time[9]), ctx.MkEq(time[8], time[12])))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkOr(ctx.MkEq(time[27], time[28]), ctx.MkEq(time[27], time[31])))); 
       optimizer.Assert(ctx.MkImplies(select[10], ctx.MkEq(time[9], time[10]))); 
       optimizer.Assert(ctx.MkImplies(select[10], ctx.MkEq(time[28], time[29]))); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[9], time[11]))); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[28], time[30]))); 
       optimizer.Assert(ctx.MkEq(select[9], ctx.MkOr(select[10], select[11]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[10], select[11] }, 1)); 
       optimizer.Assert(ctx.MkNot(select[10])); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkGe(time[11], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[30], ctx.MkAdd(time[11], ctx.MkInt(14))))); 
       optimizer.Assert(ctx.MkEq(select[13], select[12])); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkLe(time[12], time[13]))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkGe(time[31], time[32]))); 
       optimizer.Assert(ctx.MkEq(select[16], select[12])); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkLe(time[12], time[16]))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkGe(time[31], time[35]))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkOr(ctx.MkEq(time[12], time[13]), ctx.MkEq(time[12], time[16])))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkOr(ctx.MkEq(time[31], time[32]), ctx.MkEq(time[31], time[35])))); 
       optimizer.Assert(ctx.MkImplies(select[14], ctx.MkEq(time[13], time[14]))); 
       optimizer.Assert(ctx.MkImplies(select[14], ctx.MkEq(time[32], time[33]))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[13], time[15]))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[32], time[34]))); 
       optimizer.Assert(ctx.MkEq(select[13], ctx.MkOr(select[14], select[15]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[14], select[15] }, 1)); 
       optimizer.Assert(select[14]); 
       optimizer.Assert(ctx.MkEq(time[14], ctx.MkInt(1))); 
       optimizer.Assert(ctx.MkEq(time[33], ctx.MkInt(5))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkGe(time[15], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[34], ctx.MkAdd(time[15], ctx.MkInt(11))))); 
       optimizer.Assert(ctx.MkImplies(select[17], ctx.MkEq(time[16], time[17]))); 
       optimizer.Assert(ctx.MkImplies(select[17], ctx.MkEq(time[35], time[36]))); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[16], time[18]))); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[35], time[37]))); 
       optimizer.Assert(ctx.MkEq(select[16], ctx.MkOr(select[17], select[18]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[17], select[18] }, 1)); 
       optimizer.Assert(ctx.MkNot(select[17])); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkGe(time[18], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[37], ctx.MkAdd(time[18], ctx.MkInt(12))))); 
       optimizer.Assert(select[0]); 

       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[5], select[8]), ctx.MkLe(ctx.MkSub(time[8], time[5]), ctx.MkInt(0)))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[8], select[5]), ctx.MkLe(ctx.MkSub(time[5], time[8]), ctx.MkInt(0)))); 

       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[3], select[7]), ctx.MkOr(ctx.MkGe(time[3], time[26]), ctx.MkGe(time[7], time[22])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[3], select[15]), ctx.MkOr(ctx.MkGe(time[3], time[34]), ctx.MkGe(time[15], time[22])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[4], select[10]), ctx.MkOr(ctx.MkGe(time[4], time[29]), ctx.MkGe(time[10], time[23])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[4], select[17]), ctx.MkOr(ctx.MkGe(time[4], time[36]), ctx.MkGe(time[17], time[23])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[11]), ctx.MkOr(ctx.MkGe(time[6], time[30]), ctx.MkGe(time[11], time[25])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[14]), ctx.MkOr(ctx.MkGe(time[6], time[33]), ctx.MkGe(time[14], time[25])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[18]), ctx.MkOr(ctx.MkGe(time[6], time[37]), ctx.MkGe(time[18], time[25])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[7], select[15]), ctx.MkOr(ctx.MkGe(time[7], time[34]), ctx.MkGe(time[15], time[26])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[10], select[17]), ctx.MkOr(ctx.MkGe(time[10], time[36]), ctx.MkGe(time[17], time[29])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[11], select[14]), ctx.MkOr(ctx.MkGe(time[11], time[33]), ctx.MkGe(time[14], time[30])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[11], select[18]), ctx.MkOr(ctx.MkGe(time[11], time[37]), ctx.MkGe(time[18], time[30])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[14], select[18]), ctx.MkOr(ctx.MkGe(time[14], time[37]), ctx.MkGe(time[18], time[33])))); 


       if (optimizer.Check() == Status.SATISFIABLE) 
       { 
        ctx.Dispose(); 
        return true; 
       } 
       ctx.Dispose(); 
       return false; 
      } 
     } 
    } 
} 

Answer 1

간주한다. Optimize 옵션으로 Infeasible을보고합니다. Solver와 Optimize 기능의 불일치가 수정 된 것 같습니다.