優化量詞和在Z3py

所以我lloking一種方式來簡化下面的代碼Z3py因爲每次我要檢查這一說法（我自己的電腦上或http://rise4fun.com/z3py/），它只是超時，所以我覺得有可能是最快的方法。優化量詞和在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）進行處理

非常感謝提前，如果你能幫助我（甚至只是一個暗示，可以幫助我改變這種公式將是巨大的）

編輯：我只是測試單靠約束和它的作品，它給奇怪的結果，但仍然有效，但我仍然需要它來與他人約束工作，所以如果你能幫助我去優化它你開山鼻祖即

來源

2013-05-27 a.fossart

可以部分地評估一些表達的。 Z3也應該爲你簡化它們，但是如果你掌握了這些信息，這並不會傷害到你。以您的示例爲例，我獲得了預處理的以下版本： http://rise4fun.com/Z3Py/29z 但是，它表明約束不會按照您的意圖書寫：每個分離符中的最後一個連接詞是相同的，並且p1（x）和p2（x）上的條件也可以重新分配。 –

感謝您的評論，我會盡量簡化它，但我仍然有一個困難時期時，試圖使用高清（我總是搞亂我的代碼...），所以我儘量避免它，但我想我應該停止做所以...如果你想看到我的實際代碼（所有約束添加）它在這裏：http://rise4fun.com/Z3Py/77sl –

感謝您的幫助，我能夠弄清楚如何改變我的代碼，現在我只需要找到爲什麼給我一個解決方案，讓我用我的最新版本來改變處理器的數量：http://rise4fun.com/Z3Py/F3mL。但是，在我無法改變自己的號碼版本的作品真的很好，給了我很好的效果：http://rise4fun.com/Z3Py/zTxE –

問題在評論部分看起來基本上回答。

來源

2013-06-22 18:12:35

優化量詞和在Z3py

回答

相關問題