У меня есть логическая формула (формат: CNF), выполнение которой я проверяю с помощью решателя Z3 SAT. Я заинтересован в получении частичных присвоений, когда формула выполнима. Я попробовал model.partial=true по простой формуле для OR гейта и не получил никакого частичного назначения.
Вы можете подсказать, как это можно сделать? У меня нет никаких ограничений на задание, кроме частичного.
Режим частичной модели Z3 предназначен только для моделей функций. Для пропозициональных формул нет гарантии, что модели используют минимальное количество присваиваний. Напротив, по умолчанию решатели SAT находят полные назначения.
Предположим, вас интересует минимальное количество литералов, так что соединение литералов подразумевает формулу. Вы можете использовать ядра unsat для получения таких подмножеств. Идея состоит в том, что вы сначала находите модель своей формулы F как соединение литералов l1, l2, ..., ln. Тогда, учитывая, что это модель F, мы получаем, что l1 & l2 & ... & ln & not F неудовлетворительно. Итак, идея состоит в том, чтобы утверждать «не F» и проверять выполнимость «не F» по модулю предположений l1, l2, .., ln. Так как результат не соответствует требованиям, вы можете запросить Z3 для получения неподтвержденного ядра среди l1, l2, .., ln.
В Python вам нужно создать два объекта решателя:
s1 = Solver()
s2 = Solver()
Затем вы добавляете F соответственно Not (F):
s1.add(F)
s2.add(Not(F))
тогда вы найдете сокращенную модель для F, используя оба решателя:
is_Sat = s1.check()
if is_Sat != sat:
# do something else, return
m = s1.model()
literals = [sign(m, m[idx]()) for idx in range(len(m)) ]
is_sat = s2.check(literals)
if is_Sat != unsat:
# should not happen
core = s2.unsat_core()
print core
где
def sign(m, c):
val = m.eval(c)
if is_true(val):
return c
else if is_false(val):
return Not(c)
else:
# should not happen for propositional variables.
return BoolVal(True)
Конечно, есть и другие способы сократить набор литералов. Частично дешевый способ - нетерпеливо оценить каждое предложение и добавить литералы из модели до тех пор, пока каждое предложение не будет удовлетворено хотя бы одним литералом в модели. Другими словами, вы ищете минимальный набор ударов. Вам придется реализовать это за пределами Z3.
