4

此代码仅运行i=4，但如果位置未初始化，则运行i=19????? location=BoolVal(False)位置在这里初始化

from z3 import *
x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')
location,location_next=Bools('location location_next')

x=20
#t1=0
t=0
location=BoolVal(False)
#set_option(precision=10)
k=20


for   i in range(k):
  s=Solver()

  s.add(Or(And((10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0,Not(location_next)),
           And((10*x_next)>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0,location_next)),
            location_next==If(And(Not(location),x_next<19),True,If(And(location,x_next>21),False,location)))


  print i
  print s.check()
  if s.check()==unsat:
      break

  m=s.model()
  x=m[x_next]
  #t1=m[t2]


  print m[x_next].as_decimal(10)
4

1 回答 1

2

简短的回答是：您在命令中添加的公式在第4 次迭代中s.add(...)是不可满足的。在第 4 次迭代开始时，我们有 that xis19和locationis False。通过替换公式中的x和location，我们得到：

[Or(And(10*x_next >= 3*t1 - 3*t2 + 190,
        10*x_next <= 190 - t2 + t1,
        x_next >= 18,
        t2 - t1 > 0,
        Not(location_next)),
    And(10*x_next >= t2 - t1 + 190,
        5*x_next <= 95 + t2 - t1,
        x_next <= 22,
        t2 - t1 > 0,
        location_next)),
 location_next ==
 If(And(Not(False), x_next < 19),
    True,
    If(And(False, x_next > 21), False, False))]

将上面的公式化简后，我们有：

[Or(And(10*x_next >= 190 + 3*t1 - 3*t2,
           10*x_next <= 190 - t2 + t1,
           x_next >= 18,
           t2  - t1 > 0,
           Not(location_next)),
       And(10*x_next >= 190 + t2 - t1,
           5*x_next <= 95 + t2 - t1,
           x_next <= 22,
           t2 - t1 > 0,
           location_next)),
    location_next == x_next < 19]

为了说明这个公式的不可满足性，让我们考虑以下两种情况：location_next为真，或location_next为假。

  1. location_next是真的。那么，x_next < 19也一定是True。而且，第一个参数Or是False。因此，只有当我们可以使第二个参数为 True 时，公式才是可满足的。情况并非如此，因为以下内容无法满足：

    10*x_next >= 190 + t2 - t1, 5*x_next <= 95 + t2 - t1, x_next < 19

    前两个不等式意味着x_next >= 19。

  2. location_next是假的。那么x_next >= 19一定是True。Or通过类似的论证，只有当我们可以使第一个论证为真时，该公式才可满足。这也是不可能的，因为以下是不可满足的：

    10*x_next <= 190 - t2 + t1, t2 - t1 > 0, 19 <= x_next

    前两个不等式意味着x_next < 19。

备注：您没有在循环结束时更新locationusing的值。location_next你这样做是为了x，但不是为了location。这是一个正交问题。我期待这样的声明：

location=m[location_next]
于 2012-08-07T16:58:07.183 回答