尝试在 python 中使用 Z3 找到布尔公式的所有解
Trying to find all solutions to a boolean formula using Z3 in python
我是 Z3 的新手,正在尝试制作一个求解器,其中 return 是布尔公式的每个可满足的解决方案。从其他 SO-posts 做笔记,我编写了我希望能工作的代码,但不是。问题似乎是通过添加以前的解决方案,我删除了一些变量,但是在以后的解决方案中它们 return?
目前我正在尝试解决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 个模型:除了 all-False 分配,你应该有一个模型。如果您想以这种方式获取所有变量的值,那么您应该显式查询它们,如下所示:
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 中没有一个“out-of-the-box”方法来获取所有可能的分配,所以你必须像上面一样小心地自己编码。之所以没有这样的函数,是因为它一般很难实现:想想如果你的变量是函数、数组、user-defined data-types 等,它应该如何工作,而不是到简单的布尔值。在正确有效地处理所有这些可能性的情况下,实现一个通用的 all-sat 函数可能会变得非常棘手。因此,它留给了用户,因为大多数时候您只关心 all-sat 的特定概念,一旦您学习了基本的习语,通常不难编写代码。
我是 Z3 的新手,正在尝试制作一个求解器,其中 return 是布尔公式的每个可满足的解决方案。从其他 SO-posts 做笔记,我编写了我希望能工作的代码,但不是。问题似乎是通过添加以前的解决方案,我删除了一些变量,但是在以后的解决方案中它们 return?
目前我正在尝试解决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 个模型:除了 all-False 分配,你应该有一个模型。如果您想以这种方式获取所有变量的值,那么您应该显式查询它们,如下所示:
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 中没有一个“out-of-the-box”方法来获取所有可能的分配,所以你必须像上面一样小心地自己编码。之所以没有这样的函数,是因为它一般很难实现:想想如果你的变量是函数、数组、user-defined data-types 等,它应该如何工作,而不是到简单的布尔值。在正确有效地处理所有这些可能性的情况下,实现一个通用的 all-sat 函数可能会变得非常棘手。因此,它留给了用户,因为大多数时候您只关心 all-sat 的特定概念,一旦您学习了基本的习语,通常不难编写代码。