z3求解器解决方案问题

Question

p = Int('p')
q = Int('q')

s = Solver()
s.add(1<=p<=9, 1<=q<=19, 5<(3*p-4*q)<10)
s.check() 
print s.model()

返回sat,并给出解决方案

[p = 0, q = 0]

这不符合约束.如果我删除最后的约束,它将返回一个满足前两个(平凡)约束的合理对.这是怎么回事？

永久链接在线试用:http://rise4fun.com/Z3Py/fk4

---

编辑:我是z3的新手,所以有可能我做了一些可怕的错误,让我知道.

Answer 1

Z3不支持使用Python的比较链,即与之a < b < c相同a < b and b < c.如果不进行重载and,则无法使Z3支持它,这在Python中是不可能的.所以a < b < c应写成:

b_ = b
Z3.And(a < b_, b_ < c)

只评估b一次表达式.

更换s.add线后:

s.add(1<=p, p<=9, 1<=q, q<=19, 5<(3*p-4*q), (3*p-4*q)<10)

我明白了:

[p = 6, q = 3]

所以你必须像我上面为解算器那样拆分它们.

Python的扩展1<=p<=9来1<=p and p<=9,当在解释这个结果p<=9作为bool(1 <= p)IS True,在求解问题结果代码:

s.add(p<=9, q<=19, (3*p-4*q)<10)

这[p = 0, q = 0]是其中一个解决方案.