次の電気回路網を考慮してください
この電気回路網の SAT 問題は
この問題は、次のコードを使用してオンラインで 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?]
ここでこの例をオンラインで実行します
線形の例で Z3Py が量指定子の除去を完全に実行しない理由を教えてください。Z3Pyオンラインを使用して、量指定子の除去の元の非線形問題を解決できた場合。どうもありがとう。
