python - 为什么 Z3Py 不提供所有可能的解决方案

Question

我遇到了一个问题，Z3Py 没有为给定的 bool 子句枚举所有可能的解决方案。我想知道是否有人知道为什么会这样。

这是我用于 Z3Py 的代码。有 5 个 bool 值: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 中的所有解决方案都包含所有定义的变量。

Answer 1

请注意，模型将仅包含对在 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']

我相信这就是您要找的。