如何使用Z3Py和想法來自泰勒在電網絡的情況下進行量詞消去

enter image description here

該電網的SAT問題是

enter image description here

此問題使用Z3Py在線使用以下代碼解決：

r01, r02, r12, r13, r23 = Reals('r01 r02 r12 r13 r23') 
i0, i01, i02, i12, i13, i23, i3 = Reals('i0 i01 i02 i12 i13 i23 i3') 
u0, u1, u2, u3 = Reals('u0 u1 u2 u3') 
r01=1000 
r02 = 100 
r12 = 300 
r13 = 47000 
u0 = 0 
u3 = 12 
s = Solver() 
s.add(u1-u0==r01*i01, u2-u0==r02*i02, u2-u1==r12*i12,u3-u1==r13*i13, u3-u2==r23*i23) 
s.add(-i0 + i01 + i02 ==0, -i01+i12+i13==0,-i02-i12+i23==0,-i13-i23+i3==0) 
s.add(i3==i0) 
s.add((u1-u0)*i01<=0.25, (u2-u0)*i02<=0.25, (u2-u1)*i12<=0.25,(u3-u1)*i13<=0.25, (u3-u2)*i23<=0.25)   
s.add(r23 > 0) 
print s 
print s.check() 
m = s.model() 
set_option(rational_to_decimal=True) 
print m

並且輸出是：

sat 
[u1 = 1, 
r23 = 824.4299674267?, 
i02 = 0.0122978723?, 
i12 = 0.0007659574?, 
u2 = 1.2297872340?, 
i23 = 0.0130638297?, 
i3 = 0.0132978723?, 
i0 = 0.0132978723?, 
i01 = 0.001, 
i13 = 0.0002340425?]

最後使用Z3Py我們解決量詞消去的線性問題：

g = Goal() 
g.add(Exists([i0, i01, i02, i12, i13, i23, i3, u1, u2], And(u1-u0==r01*i01, u2-u0==r02*i02, u2-u1==r12*i12, 
     u3-u1==r13*i13, u3-u2==r23*i23,-i0 + i01 + i02 ==0, -i01+i12+i13==0,-i02-i12+i23==0, 
     -i13-i23+i3==0,i3==i0,r23 > 0, (u1-u0)<=7, (u2-u0)<=7, (u2-u1)<=7, 
      (u3-u1)<=7, (u3-u2)<=7))) 
t = Tactic('qe') 
print t(g) 
print t(g).as_expr() 
s1 = Solver() 
s1.add(t(g).as_expr()) 
print s1.check() 
m1 = s1.model() 
print m1

和相應的輸出是：

[[∃x!5 : 
¬(r23 ≤ 0) ∧ 
0.0107817589?·r23·x!5 + x!5 ≤ 0.1291856677? ∧ 
-0.0107817589?·r23·x!5 + -1·x!5 ≤ -0.1291856677? ∧ 
x!5 + 0.0107817589?·r23·x!5 ≤ 0.1291856677? ∧ 
r23·x!5 ≥ 2.9319148936? ∧ 
r23·x!5 ≥ 5 ∧ 
r23·x!5 ≥ -18.0972222222? ∧ 
r23·x!5 ≤ 5.5446808510? ∧ 
r23·x!5 ≤ 7]] 

∃x!5 : 
¬(r23 ≤ 0) ∧ 
0.0107817589?·r23·x!5 + x!5 ≤ 0.1291856677? ∧ 
-0.0107817589?·r23·x!5 + -1·x!5 ≤ -0.1291856677? ∧ 
x!5 + 0.0107817589?·r23·x!5 ≤ 0.1291856677? ∧ 
r23·x!5 ≥ 2.9319148936? ∧ 
r23·x!5 ≥ 5 ∧ 
r23·x!5 ≥ -18.0972222222? ∧ 
r23·x!5 ≤ 5.5446808510? ∧ 
r23·x!5 ≤ 7 

sat 

[r23 = 68, x!5!54 = 0.0745376635?]

運行該在線示例here

請讓我知道爲什麼Z3Py不能完全執行線性例子中的量詞消除;並且如果消除量詞的原始非線性問題可以在線使用Z3Py解決。非常感謝。

來源

2013-08-04 Juan Ospina

當我將功率約束添加到第二個示例中，並將電壓限制從7V提升到12V時，我得到了類似於第一個示例中的類似解決方案。嘗試在第一個示例中添加「r23 <520」以獲得另一個解決方案。我認爲你的例子很好。它表明Z3可以很容易地解決這樣的計算。但這不僅僅是一個問題而是一個答案。 –

非常感謝您的意見。我的問題是：爲什麼Z3Py不能在線性示例中完全執行量詞消除;如果消除量詞消除的原始非線性問題可以使用Z3Py在線解決？請使用RedLog觀察下面的解決方案。祝一切順利。 –