38

Microsoft Research が開発した SMT ソルバーである Z3 を使用して、一次理論の可能なすべてのモデルを取得しようとしています。最小限の作業例を次に示します。

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

この命題のケースでは、満足のいく代入が 2 つあります。f->trueとf->falseです。Z3 (および一般的な SMT ソルバー) は、満足のいくモデルを 1 つだけ見つけようとするため、すべての解を直接見つけることはできません。ここでという便利なコマンドを見つけました(next-sat)が、Z3 の最新バージョンではこれがサポートされなくなったようです。これは私にとっては少し残念なことですが、一般的にこのコマンドは非常に便利だと思います。これを行う別の方法はありますか？

4

2 に答える 2

39

これを実現する 1 つの方法は、API の 1 つとモデル生成機能を使用することです。次に、1 つの充足可能性チェックから生成されたモデルを使用して制約を追加し、満足のいく代入がなくなるまで、以前のモデル値が後続の充足可能性チェックで使用されないようにすることができます。もちろん、有限ソートを使用する必要があります (またはこれを保証するいくつかの制約があります) が、可能なモデルをすべて見つけたくない場合 (つまり、大量のモデルを生成した後に停止する場合) は、無限ソートでも使用できます。 .

以下は z3py を使用した例です (z3py スクリプトへのリンク: http://rise4fun.com/Z3Py/a6MC ):

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

一般に、関連するすべての定数の論理和を使用すると機能するはずです (たとえば、aand bhere)。これは、を満たす( と の間の)aとのすべての整数代入を列挙します。たとえば、andを制限し、代わりにandの間に配置すると、出力は次のようになります。b120a >= 2bab15

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]
于 2012-11-15T13:51:10.107 に答える
0

テイラーの答えに基づくより一般的な解決策は、使用することです

while s.check() == z3.sat:  
    solution = "False"
    m = s.model()
    for i in m:
        solution = f"Or(({i} != {m[i]}), {solution})"
    f2 = eval(solution)
    s.add(f2)

これにより、3 つ以上の変数が許可されます。

于 2022-01-13T09:33:27.470 に答える