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
Pergunta
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.
Solução 2
Outras dicas
Using Redlog of Reduce is possible to solve the linear problem as follows:
Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow