частичные назначения в Z3

Question

У меня есть булевая формула (формат: CNF), чья удовлетворительность я проверяю с помощью решателя Z3 SAT. Меня интересует получение частичных заданий, когда формула является выполнимой. Я попробовал model.partial=true по простой формуле для ворот OR и не получил никакого частичного назначения.

Можете ли вы предложить, как это можно сделать? У меня нет ограничений на назначение, кроме частичного.

Answer 1

Частичный режим модели Z3 предназначен только для моделей функций. Для пропозициональных формул нет уверенности в том, что модели используют минимальное количество присвоений. Напротив, режим SAT-решений по умолчанию - это то, что они находят полные назначения.

Предположим, что вас интересует минимальное количество литералов, так что соединение литералов подразумевает формулу. Вы можете использовать unsat core для получения таких подмножеств. Идея состоит в том, что вы сначала найдете модель своей формулы F как соединение литералов l1, l2, ..., ln. Тогда, учитывая, что это модель F, мы имеем, что l1 & l2 & ... & ln & не F является неудовлетворительным. Итак, идея состоит в том, чтобы утверждать «не F» и проверять выполнимость «не F» по модулю допущений l1, l2, ..., ln. Поскольку результат является неактивным, вы можете запросить Z3 для получения ненадежного ядра среди l1, l2, .., ln.

С питоном, что вы могли бы сделать, чтобы создать два решателя объекты:

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.