Попытка найти все решения булевой формулы, используя Z3 в python - PullRequest
Новая
       25

Попытка найти все решения булевой формулы, используя Z3 в python

1 голос
/ 03 августа 2020

Я новичок в Z3 и пытаюсь создать решатель, который возвращает каждое удовлетворительное решение булевой формулы. Делая заметки из других SO-сообщений, я закодировал то, что, как я надеялся, сработает, но это не так. Проблема заключается в том, что, добавляя предыдущие решения, я удаляю некоторые из переменных, но затем они возвращаются в более поздних решениях?

В настоящее время я просто пытаюсь решить 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]

1 Ответ

4 голосов
/ 03 августа 2020

Типичный способ кодирования таких проблем следующий: 

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 обычно "прекращает" присвоение переменных, как только решает, что проблема решена, так как другие переменные не имеют значения. 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 нет "готового" метода для получения всех возможных назначений, поэтому вы должны быть осторожны при написании кода самостоятельно, как описано выше. Причина, по которой такой функции нет, заключается в том, что ее действительно сложно реализовать в целом: подумайте о том, как она должна работать, если бы ваши переменные были функциями, массивами, пользовательскими типами данных и т. Д. c. в отличие от простых логических значений. Может быть очень сложно реализовать общую функцию c all-sat со всеми этими возможностями, обрабатываемыми правильно и эффективно. Таким образом, это остается на усмотрение пользователя, поскольку в большинстве случаев вас интересует только конкретное c понятие all-sat, которое, как правило, несложно закодировать, если вы изучите основные c идиомы.

...