试图在python中使用Z3找到布尔公式的所有解决方案

Question

我是Z3的新手，正在尝试制作一个求解器，将每个可满足的解返回到布尔公式。根据其他SO帖子的笔记，我已经对我希望能奏效的内容进行了编码，但事实并非如此。问题似乎是，通过添加以前的解决方案，我删除了一些变量，但随后它们在以后的解决方案中返回？

目前我只是想解决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将典型地"；停止"；一旦它决定问题是sat，就分配变量，因为其他变量是不相关的。

我想你的困惑是，你的问题应该有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参数。对于新来者来说，这是一个常见的陷阱；开箱即用"；方法来获得所有可能的赋值，所以你必须像上面一样小心地自己编码。没有这样一个函数的原因是，通常很难实现它：想想如果你的变量是函数、数组、用户定义的数据类型等，而不是简单的布尔值，它应该如何工作。在正确有效地处理所有这些可能性的情况下，实现一个通用的全sat函数可能会变得非常棘手。因此，这就留给用户了，因为大多数时候你只关心all-sat的一个特定概念，一旦你学会了基本的习惯用法，通常就不难编码。