如果是这种情况，如何强制 z3py 显示多个答案？

Question

from z3 import *

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

solve(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

给我[p = 2, q = 1]，但 p 可能是 2 或 3。所以答案应该是 {2,3}。我如何告诉 z3 通知我多个答案？

Answer 1

这个问题经常出现，有一些注意事项。本质上，您必须编写一个循环来“拒绝”早期模型并继续查询可满足性。对于您的特定问题，您可以像这样编码：

from z3 import *

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

s = Solver()
s.add(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)

res = s.check()
while (res == sat):
  m = s.model()
  print(m)
  block = []
  for var in m:
      block.append(var() != m[var])
  s.add(Or(block))
  res = s.check()

当我运行这个时，我得到：

[p = 2, q = 1]
[p = 3, q = 1]

请注意，z3 并不总是生成“完整”模型：一旦确定问题是 ，它将停止生成分配sat。因此，您可能必须跟踪变量并显式使用模型完成。有关如何执行此操作的详细信息，请参阅尝试在 python 中使用 Z3 查找布尔公式的所有解决方案。