为什么Z3Py无法提供所有可能的解决方案 [英] Why Z3Py does not provide all possible solutions
问题描述
我遇到了一个问题，其中Z3Py并未枚举给定布尔条款的所有可能解决方案.我想知道是否有人知道为什么会这样.
这是我用于Z3Py的代码.有5个布尔值:1 2 3 4和5.
from z3 import *
a,b,c,d,e = Bools('1 2 3 4 5')
solver = Solver()
solver.add(Or(Not(a), Not(b)))
solver.add(Or(Not(b), Not(c)))
solver.add(Or(Not(c), Not(d)))
solver.add(Or(Not(d), Not(e)))
while solver.check() == sat:
model = solver.model()
block = []
for declaration in model:
constant = declaration()
block.append(constant != model[declaration])
solver.append(Or(block))
solution = []
for val in model:
if is_true(model[val]):
solution.append(str(val()))
else:
solution.append('-' + str(val()))
solution.sort()
print(solution)
这将产生以下模型:
['-1', '-2', '-3', '-4', '-5']
['-2', '-3', '-5', '1']
['-2', '-3', '-4', '1', '5']
['-2', '-4', '3', '5']
['-2', '-4', '-5', '3']
['-1', '-3', '-4', '-5', '2']
['-1', '-3', '-4', '2', '5']
['-1', '-2', '-3', '-4', '5']
['-1', '-2', '-3', '-5', '4']
['-1', '-3', '-5', '2', '4']
如果我使用带有以下代码的Pycosat运行相同的子句:
import pycosat
clauses = [(-1, -2), (-2, -3), (-3, -4), (-4, -5)]
for solution in pycosat.itersolve(clauses):
print(solution)
我得到那些结果:
[-1, -2, -3, -4, -5]
[-1, -2, -3, -4, 5]
[-1, -2, -3, 4, -5]
[-1, -2, 3, -4, -5]
[-1, -2, 3, -4, 5]
[-1, 2, -3, -4, -5]
[-1, 2, -3, -4, 5]
[-1, 2, -3, 4, -5]
[1, -2, -3, 4, -5]
[1, -2, -3, -4, -5]
[1, -2, -3, -4, 5]
[1, -2, 3, -4, -5]
[1, -2, 3, -4, 5]
因此，Z3Py根据Pycosat的结果漏掉了3种可能的解决方案.这些是:
[1, -2, 3, -4, 5]
[1, -2, -3, 4, -5]
[1, -2, 3, -4, -5]
我知道这些是不同的求解器，但是基于用于它们的相同子句，我希望结果匹配.任何人都知道为什么Z3Py在这种情况下会错过那些解决方案吗? 另一件事是，并非Z3Py中的所有解决方案都包含所有定义的变量.
请注意，模型将只包含对在sat结果中重要的变量的赋值.任何无关紧要的变量都不会显式分配.为避免此问题，请循环遍历您域中的变量，并将参数model_completion=True用作eval方法，如下所示:
from z3 import *
a,b,c,d,e = Bools('1 2 3 4 5')
solver = Solver()
solver.add(Or(Not(a), Not(b)))
solver.add(Or(Not(b), Not(c)))
solver.add(Or(Not(c), Not(d)))
solver.add(Or(Not(d), Not(e)))
while solver.check() == sat:
model = solver.model()
block = []
solution = []
for var in [a, b, c, d, e]:
v = model.eval(var, model_completion=True)
block.append(var != v)
solution.append(str(var) if is_true(v) else '-' + str(var))
solver.add(Or(block))
solution.sort()
print(solution)
此打印:
['-1', '-2', '-3', '-4', '-5']
['-2', '-3', '-4', '-5', '1']
['-2', '-3', '-5', '1', '4']
['-1', '-2', '-3', '-5', '4']
['-1', '-2', '-3', '-4', '5']
['-1', '-2', '-4', '3', '5']
['-2', '-4', '-5', '1', '3']
['-2', '-4', '1', '3', '5']
['-2', '-3', '-4', '1', '5']
['-1', '-3', '-4', '2', '5']
['-1', '-3', '-4', '-5', '2']
['-1', '-2', '-4', '-5', '3']
['-1', '-3', '-5', '2', '4']
我相信这是您要寻找的.
I ran into a problem where Z3Py does not enumerate all possible solutions for the given Boolean clauses. I was wondering if anyone knows why this is happening.
Here is the code I use for the Z3Py. There are 5 booleans: 1 2 3 4 and 5.
from z3 import *
a,b,c,d,e = Bools('1 2 3 4 5')
solver = Solver()
solver.add(Or(Not(a), Not(b)))
solver.add(Or(Not(b), Not(c)))
solver.add(Or(Not(c), Not(d)))
solver.add(Or(Not(d), Not(e)))
while solver.check() == sat:
model = solver.model()
block = []
for declaration in model:
constant = declaration()
block.append(constant != model[declaration])
solver.append(Or(block))
solution = []
for val in model:
if is_true(model[val]):
solution.append(str(val()))
else:
solution.append('-' + str(val()))
solution.sort()
print(solution)
This produces the following models:
['-1', '-2', '-3', '-4', '-5']
['-2', '-3', '-5', '1']
['-2', '-3', '-4', '1', '5']
['-2', '-4', '3', '5']
['-2', '-4', '-5', '3']
['-1', '-3', '-4', '-5', '2']
['-1', '-3', '-4', '2', '5']
['-1', '-2', '-3', '-4', '5']
['-1', '-2', '-3', '-5', '4']
['-1', '-3', '-5', '2', '4']
If I run the same clauses using Pycosat with the following code:
import pycosat
clauses = [(-1, -2), (-2, -3), (-3, -4), (-4, -5)]
for solution in pycosat.itersolve(clauses):
print(solution)
I get those results:
[-1, -2, -3, -4, -5]
[-1, -2, -3, -4, 5]
[-1, -2, -3, 4, -5]
[-1, -2, 3, -4, -5]
[-1, -2, 3, -4, 5]
[-1, 2, -3, -4, -5]
[-1, 2, -3, -4, 5]
[-1, 2, -3, 4, -5]
[1, -2, -3, 4, -5]
[1, -2, -3, -4, -5]
[1, -2, -3, -4, 5]
[1, -2, 3, -4, -5]
[1, -2, 3, -4, 5]
Hence, Z3Py missing out 3 possible solutions based on the results from Pycosat. And those are:
[1, -2, 3, -4, 5]
[1, -2, -3, 4, -5]
[1, -2, 3, -4, -5]
I know those are the different solvers but based on the same clauses used for both of them, I would expect the results to match. Anyone knows why Z3Py would miss out those solutions in this case? The other thing is that not all the solutions in Z3Py contain all the defined variables.
Note that a model will only contain assignments to variables that do matter in the sat outcome. Any variable that doesn't matter will not get assigned explicitly. To avoid this problem, loop over the variables in your domain and use the parameter model_completion=True to the eval method, like this:
from z3 import *
a,b,c,d,e = Bools('1 2 3 4 5')
solver = Solver()
solver.add(Or(Not(a), Not(b)))
solver.add(Or(Not(b), Not(c)))
solver.add(Or(Not(c), Not(d)))
solver.add(Or(Not(d), Not(e)))
while solver.check() == sat:
model = solver.model()
block = []
solution = []
for var in [a, b, c, d, e]:
v = model.eval(var, model_completion=True)
block.append(var != v)
solution.append(str(var) if is_true(v) else '-' + str(var))
solver.add(Or(block))
solution.sort()
print(solution)
This prints:
['-1', '-2', '-3', '-4', '-5']
['-2', '-3', '-4', '-5', '1']
['-2', '-3', '-5', '1', '4']
['-1', '-2', '-3', '-5', '4']
['-1', '-2', '-3', '-4', '5']
['-1', '-2', '-4', '3', '5']
['-2', '-4', '-5', '1', '3']
['-2', '-4', '1', '3', '5']
['-2', '-3', '-4', '1', '5']
['-1', '-3', '-4', '2', '5']
['-1', '-3', '-4', '-5', '2']
['-1', '-2', '-4', '-5', '3']
['-1', '-3', '-5', '2', '4']
which I believe is what you're looking for.
这篇关于为什么Z3Py无法提供所有可能的解决方案的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
