Z3の部分的な割り当て

Question

私はZ3 SATソルバを使って充足可能性をチェックするブール式（形式：CNF）を持っています。私は数式が充足可能であるときに部分的な割り当てを得ることに興味があります。私はORゲートの簡単な公式でmodel.partial=trueを試しましたが、部分的な割り当てはありませんでした。

これはどのように行うことができますか？私はそれが部分的であること以外の課題には制約がありません。

Answer 1

Z3の部分モデルモードは、関数のモデル用です。命題式の場合、モデルが最小限の割り当てを使用するという保証はない。それどころか、SATソルバーのデフォルトモードは完全な割り当てを見つけることです。

最小のリテラル数に関心があり、そのリテラルの連接が数式を暗示するとします。このようなサブセットを取得するには、unsatコアを使用できます。考え方は、まず、数式Fのモデルをリテラルl1、l2、...、lnの連結詞として見つけることです。これがFのモデルであるとすれば、l1 &l2 & ... &ln &であり、Fは満たされない。 したがって、 "not F"をアサートし、 "not F"モジュロ仮説l1、l2、..、lnの充足可能性をチェックすることです。結果はunsatなので、Z3にクエリを実行して、l1、l2、..、lnのうちunsatコアを取得できます。あなたがどうなるのかのpythonから

2つのソルバーのオブジェクトを作成することです：

s1 = Solver() 
    s2 = Solver() 

次にあなたは、Fをそれぞれ、未（F）追加：

s1.add(F) 
    s2.add(Not(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 

012：Fは、両方のソルバーを使用して

もちろん、リテラルの縮小セットを取得する他の方法もあります。部分的に安価な方法は、各節を熱心に評価し、各節がモデル内の少なくとも1つのリテラルによって満たされるまで、モデルからリテラルを追加することです。言い換えれば、あなたは最小のヒットセットを探しています。これをZ3の外部に実装する必要があります。