したがって、Z3py で次のコードを単純化する方法を探しています。このアサーションを確認するたびに (自分のコンピューターまたはhttp://rise4fun.com/z3py/で) タイムアウトになったので、そこにあると思います最速の方法かもしれません。
Task = Datatype('Task')
Task.declare("cons",("num", IntSort()),("order",IntSort()),("arrival",IntSort()))
Task = Task.create()
order = Task.order
num = Task.num
x = Int('x')
y = Int('y')
s = Solver()
tasks = (Task.cons(0,0,0),\
Task.cons(0,1,0),\
Task.cons(0,2,0),\
Task.cons(0,3,0),\
Task.cons(1,0,1),\
Task.cons(1,1,1),\
Task.cons(1,2,1),\
Task.cons(2,0,3),\
Task.cons(2,1,3),\
Task.cons(2,2,3),\
Task.cons(2,3,3),\
Task.cons(2,4,3),\
Task.cons(3,0,1),\
Task.cons(3,1,1))
p1 = Function('p1',IntSort(),Task)
p2 = Function('p2',IntSort(),Task)
order = And([Exists([x,y],Or(And(p1(x)==t1,p1(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
And(p1(x)==t1,p2(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
And(p2(x)==t1,p1(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True)),\
And(p2(x)==t1,p2(y)==t2,If(num(t1)==num(t2),Implies(x<y,order(t1)<order(t2)),True))))\
for t1 in tasks for t2 in tasks])
s.add(order)
ご覧のとおり、これは非常に大きな式ですが、それを小さくする方法は見つかりませんでした...目的は、タスクのすべての部分が異なるプロセッサによって処理されている場合でも、順序どおりであることを確認することです (p1または p2)
あなたが私を助けることができれば、前もって感謝します（その式を変更するのに役立つヒントだけでも素晴らしいでしょう）
編集：その制約を単独でテストしたところ、機能します。奇妙な結果が得られますが、それでも機能しますが、他の制約と連携する必要があるため、最適化を手伝っていただければ大歓迎です。