Z3：すべての満足できるモデルを見つける

Question

私は、Microsoft Researchによって開発されたSMTソルバーであるZ3を使って、一次理論のすべての可能なモデルを検索しようとしています。 f->trueとf->false 2つの満足の割り当てがある。この命題場合

(declare-const f Bool) 
(assert (or (= f true) (= f false))) 

：ここで最小実施例です。 Z3（とSMTソルバーは一般的に）モデルを満たすものを見つけることのみを試みるため、すべての解を見つけることは直接的に不可能です。 Here(next-sat)という便利なコマンドが見つかりましたが、Z3の最新バージョンはこれをサポートしていないようです。これは私にとって少し不幸なことですが、一般的にはこのコマンドは非常に便利だと思います。これを行う別の方法がありますか？

Answer 1

これを達成する1つの方法は、モデル生成機能とともにAPIの1つを使用することです。その後、1つの充足可能性チェックから生成されたモデルを使用して、満足のいく割り当てがなくなるまで、後続の充足可能性検査で以前のモデル値が使用されないように制約を追加できます。もちろん、有限のソートを使用する必要があります（またはこれを保証するいくつかの制約があります）が、可能なすべてのモデルを見つけたくない場合（つまり束を生成した後で停止する場合） 。一般に

a = Int('a') 
b = Int('b') 

s = Solver() 
s.add(1 <= a) 
s.add(a <= 20) 
s.add(1 <= b) 
s.add(b <= 20) 
s.add(a >= 2*b) 

while s.check() == sat: 
    print s.model() 
    s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model 

、関連するすべての定数の論理和を使用して（ここでは例えば、aとb）が動作する必要があり：ここ

はz3pyを用いた例（：http://rise4fun.com/Z3Py/a6MC z3pyスクリプトへのリンク）です。これは、a >= 2bを満たすaとb（1と20の間）のすべての整数の割り当てを列挙します。私たちが代わりに1と5の間に位置するaとbを制限した場合、出力は次のようになります。また、

[b = 1, a = 2] 
[b = 2, a = 4] 
[b = 1, a = 3] 
[b = 2, a = 5] 
[b = 1, a = 4] 
[b = 1, a = 5]