Z3中的部分分配

Question

我有一個布爾公式（格式：CNF），它的滿足性我使用Z3 SAT解算器進行檢查。當公式可以滿足時，我有興趣獲得部分作業。我試圖用model.partial=true對一個OR門的簡單公式進行分析，但沒有得到任何部分分配。

你能建議如何做到這一點嗎？除了它是部分的，我對任務沒有任何限制。

Answer 1

Z3的部分模型模式僅適用於功能模型。對於命題公式，不能保證模型使用最少數量的分配。相反，SAT求解器的默認模式是他們找到完整的分配。

假設您對最小化的文字數量感興趣，例如文字的連接意味着公式。你可以使用不飽和核心來獲得這樣的子集。這個想法是，你首先找到你的公式F的一個模型作爲文字l1，l2，...，ln的聯合。那麼鑑於這是F的一個模型，我們已經知道，不是F是不可滿足的。 所以這個想法是斷言「不是F」並檢查「不是F」模的假設l1，l2，...，ln的可滿足性。由於結果不一致，因此可以查詢Z3以檢索l1，l2，...，ln中不存在的核心。

從Python中，你會做什麼是創建兩個解算器對象：

s1 = Solver() 
    s2 = Solver() 

然後添加F時，不（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之外實現這一點。