我是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]
编码此类问题的典型方法如下：
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中没有“开箱即用”的方法来获取所有可能的分配，因此您必须像上面那样小心地对其进行编码。之所以没有这样的函数，是因为通常很难实现它：考虑一下，如果变量是函数，数组，用户定义的数据类型等，而不是简单的布尔值，那么它应该如何工作。正确地，有效地处理所有这些可能性，以实现通用的全卫星功能可能会非常棘手。因此，它留给用户使用，因为在大多数时候，您只关心特定的全周概念，一旦学习了基本习语，通常就不难编写代码。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句