z3 - 尝试在 python 中使用 Z3 找到 bool 公式的所有解决方案

Question

我是 Z3 的新手，正在尝试制作一个求解器，将每个可满足的解决方案返回到 bool 公式。从其他 SO-posts 做笔记，我编写了我希望能工作的代码，但不是。问题似乎是通过添加以前的解决方案，我删除了一些变量，但随后它们在以后的解决方案中返回了？

目前我只是想解决a或b或c。

如果我解释得不好，请告诉我，我会尝试进一步解释。

预先感谢您的回复:)

我的代码:

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

while (s.check() == sat):
        print(s.check())
        print(s)
        print(s.model())
        print(s.model().decls())
        print("\n")
        s.add(Or([ f() != s.model()[f] for f in s.model().decls() if f.arity() == 0])) 

我的输出:

sat
[Or(a, b, c)]
[c = False, b = False, a = True]
[c, b, a]


sat
[Or(a, b, c), Or(c != False, b != False, a != True)]
[b = True, a = False]
[b, a]


sat
[Or(a, b, c),
 Or(c != False, b != False, a != True),
 Or(b != True, a != False)]
[b = True, a = True]
[b, a]


sat
[Or(a, b, c),
 Or(c != False, b != False, a != True),
 Or(b != True, a != False),
 Or(b != True, a != True)]
[b = False, c = True]
[b, c]

Answer 1

此类问题的典型编码方式如下:

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

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()

这打印:

[b = True, a = False, c = False]
[a = True]
[c = True, a = False]

您会注意到并非所有模型都是“完整的”。这是因为 z3 通常会在确定问题解决后“停止”分配变量，因为其他变量无关紧要。

我想您的困惑是您的问题应该有 7 个模型:除了全假分配之外，您应该有一个模型。如果您想以这种方式获取所有变量的值，那么您应该显式查询它们，如下所示:

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

myvars = [a, b, c]

res = s.check()
while (res == sat):
  m = s.model()
  block = []
  for var in myvars:
      v = m.evaluate(var, model_completion=True)
      print("%s = %s " % (var, v)),
      block.append(var != v)
  s.add(Or(block))
  print("\n")
  res = s.check()

这打印:

a = False  b = True  c = False

a = True  b = False  c = False

a = True  b = True  c = False

a = True  b = True  c = True

a = True  b = False  c = True

a = False  b = False  c = True

a = False  b = True  c = True

如您所料，正好有 7 个模型。

注意 model_completion 参数。对于新手来说这是一个常见的陷阱，因为在 z3 中没有一个“开箱即用”的方法来获取所有可能的分配，所以你必须像上面一样小心地自己编码。没有这样一个函数的原因是它通常很难实现:想想如果你的变量是函数、数组、用户定义的数据类型等而不是简单的 bool 值，它应该如何工作。在正确有效地处理所有这些可能性的情况下，实现一个通用的全卫星功能可能会变得非常棘手。因此，它留给了用户，因为大多数时候您只关心 all-sat 的特定概念，一旦您学习了基本习语，通常不难编写代码。