尝试在Python中使用Z3找到布尔公式的所有解 [英] Trying to find all solutions to a boolean formula using Z3 in python

问题描述

我是Z3的新手，正在尝试创建一个求解器，它返回布尔公式的所有可满足解。我记下了其他帖子的笔记，我编写了我希望能起作用的代码，但事实并非如此。问题似乎是，通过添加前面的解决方案，我删除了一些变量，但它们在后来的解决方案中返回？

目前我只想解决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("
")
        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通常会在确定问题已解决后停止&q；赋值变量，因为其他变量是不相关的。

我想您的困惑是应该有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("
")
  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中没有一种开箱即用的方法来获得所有可能的任务，所以你必须像上面那样自己编写代码。之所以没有这样的函数，是因为它通常很难实现：想一想，如果您的变量是函数、数组、用户定义的数据类型等，而不是简单的布尔值，它应该如何工作。要正确高效地处理所有这些可能性，实现一个通用的全SAT函数可能会变得非常棘手。因此，它留给了用户，因为在大多数情况下，您只关心All-Sat的一个特定概念，一旦您学习了基本的习惯用法，这通常并不难编码。

这篇关于尝试在Python中使用Z3找到布尔公式的所有解的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！