Using Redlog of Reduce is possible to solve the non-linear problem as follows:
How to perform quantifier elimination using Z3Py and an idea from Taylor in the case of an electrical network
题
Please consider the following electrical network
the SAT problem for this electrical network is
This problem is solved using Z3Py online using the following code:
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
and the output is:
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?]
Finally using Z3Py we solve a linear problem of quantifier elimination:
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
and the corresponding output is:
[[∃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?]
Run this example online here
Please let me know why Z3Py does not perform fully the quantifier elimination in the linear example; and if the original non-linear problem of quantifier elimination could be solved using Z3Py online. Many thanks.
解决方案 2
其他提示
Using Redlog of Reduce is possible to solve the linear problem as follows:
不隶属于 StackOverflow