Почему Z3Py не предоставляет все возможные решения - PullRequest
Новая
       31

Почему Z3Py не предоставляет все возможные решения

0 голосов
/ 06 ноября 2018

Я столкнулся с проблемой, когда 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 упускает 3 возможных решения на основе результатов Pycosat. А это: 

[1, -2, 3, -4, 5]
[1, -2, -3, 4, -5]
[1, -2, 3, -4, -5]

Я знаю, что это разные решатели, но, основываясь на одних и тех же предложениях, используемых для них обоих, я ожидаю, что результаты совпадут. Кто-нибудь знает, почему Z3Py пропустит эти решения в этом случае? Другое дело, что не все решения в Z3Py содержат все определенные переменные.

Ответы [ 2 ]

0 голосов
/ 06 ноября 2018

Обратите внимание, что модель будет содержать присваивания только тем переменным, которые имеют значение в результате 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']

что я считаю, это то, что вы ищете.

0 голосов
/ 06 ноября 2018

Другое дело, что не все решения в Z3Py содержат все определенные переменные.

Это означает, что не упомянутые переменные не влияют на результат. Таким образом, наличие ['-2', '-4', '3', '5'] в качестве решения эквивалентно наличию ['1', '-2', '-4', '3', '5'] и ['-1', '-2', '-4', '3', '5'].

Если вы принимаете это во внимание при сравнении решений, наборы решений, предоставляемые обоими решателями, эквивалентны.

...