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

问题描述

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通知我多个答案？

解决方法

这个问题经常出现，有一些警告。本质上，您必须编写一个循环来“拒绝”较早的模型并保持查询的可满足性。对于您的特定问题，可以这样编写：

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后，它将停止产生分配。因此，您可能必须跟踪变量并显式使用模型完成。有关如何执行此操作的详细信息，请参见Trying to find all solutions to a boolean formula using Z3 in python。