使用MaxSAT問合せは、Z3

Question

に私がZ3/SMTLibのAPIについて質問があります。液体タイプ ツールが必要

キーSMTサブルーチンは、次のクエリです：

現在

INPUT: A "background" formula P 
    , A list of "goal" formulas Qs = [Q1,...,Qn] 

OUTPUT: Largest Qs' \subset Qs s.t. forall Q in Qs', P => Q. 

、我々は明白な方法でこれを計算する：

def query1(P, Qs): 
    Qs' := [] 
    ASSERT(P) 
    for Q in Qs: 
    PUSH() 
    ASSERT (not Q) 
    if CHECKUNSAT(): 
     Qs'.add(Q) 
    POP() 
    return Qs' 

私の質問：ありMaxSAT経由でもっと速くやってみましょうか？ Hardある

def query2(P, Qs): 
    F = (Hard P) /\ ((Soft ~Q1) \/ ... \/ (Soft ~QN)) 
    Rs = MaxSat(F) 
    Qs' = Qs - Rs 
    return Qs' 

あなたはも 満足することができ~Qiの数を最大PとSoft 手段を満たさなければならないことを意味します。具体的には、

1. 私に上記をさせるAPIはありますか？
2. はquery2上記query1のループよりも速いだろうか？

Answer 1

やや混乱：これは本当のMAX-SAT問題ではありません。これは、暗黙のリテラルの最大セットを計算しています。これは、「真」に等しいリテラルであるか、例えば、暗黙の等式のセットを計算することに似ています。 我々は、get-暗黙の等式では、このために少し調整を行うには、ジョシュと特長とした紙。一般に、完全なチェックを行う前にフィルタリング（掃引）を使用して候補を削除するSATの特殊な方法があります。

あなたの "QUERY2は" 本当にこのような何かされている必要があります：

def query2(P, Qs): 
     while True: 
      F = And(P, Or[Not(Q) for Q in Qs]) 
      if sat == CheckSAT(F):     
       Qs = [Q for Q in Qs if is_false(model.eval(Q)) ] 
      else: 
       return Qs