在 Z3py 中优化量词和 for答案

【问题标题】：Optimize quantifiers and for in Z3py在 Z3py 中优化量词和 for
【发布时间】：2013-05-27 04:29:14
【问题描述】：

所以我正在寻找一种方法来简化 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）

如果你能帮助我，提前非常感谢（即使只是一个可以帮助我改变公式的提示也会很棒）

编辑：我只是单独测试了该约束并且它有效，它给出了奇怪的结果但仍然有效，但我仍然需要它与其他约束一起工作，所以如果你能帮助我优化它，欢迎你。

【问题讨论】：

您可以对某些表达式进行部分计算。 Z3 也应该为您简化它们，但是当您手头有信息时这样做并没有什么坏处。以你的例子为例，我得到了以下带有预处理的版本：rise4fun.com/Z3Py/29z 但是，它表明约束不是按照你想要的方式编写的：每个析取中的最后一个合取是相同的，并且 p1(x ) 和 p2(x) 也可以重新分配。
感谢您的评论，我会尽量简化它，但我在尝试使用 def 时仍然很难（我总是弄乱我的代码......）所以我尽量避免它，但我认为我应该停止这样做......如果你想查看我的实际代码（添加了所有约束），它就在这里：rise4fun.com/Z3Py/77sl
感谢您的帮助，我能够弄清楚如何更改我的代码，现在我只需要找出为什么要这么长时间才能给我一个最新版本的解决方案，让我可以更改处理器数量：rise4fun.com/Z3Py/F3mL。但是我不能改变他们的号码的版本真的很好，给了我很好的结果：rise4fun.com/Z3Py/zTxE

标签： python z3 first-order-logic

【解决方案1】：

这个问题似乎在 cmets 部分得到了基本解答。

【讨论】：