私はZ3 C++ APIを使用して、いくつかのブール型変数（b0、...、bnを真と呼ぶ）に関して最小限の充足可能な式を見つけました。Z3が最後に有効なモデルを取得する
私はブール変数b0、...、bnを含む数式を持っています。そして、私はb0、...、bnの最小数が真であるいくつかの充足可能な数式を探したいと思います。
これは、真に割り当てられ、私の式を満たすことができるb0、...、bnのサブセットを最初に見つけることによって行います。そして、私はソルバーに段階的に小さい部分集合を見つけるように頼みます。偽にフリップ）。
小さいサブセットが見つからない場合、つまりZ3からの結果が不十分な場合にローカルミニマムを見つけました。この時点で、私は最後の有効なモデルにアクセスしたいと思います。
これは可能ですか？ 「チェック」の呼び出しが不成功の場合、Z3はモデルを変更しますか？ もしそうなら、私はC++ APIを使ってこれをどうやって行うことができますか？事前に
多くのおかげで、
ソルバーのリターンが「座って」いる場合は、モデルを取得することができます。モデルはソルバーの状態を参照するため、アサーションを追加すると、状態が変更され、モデルは適合性をチェックしてからsatを返すまで有効になりません。 ソルバーがSATを返すたびにモデルを取得し、最後のモデルを除くすべてのモデルを排出することができます。
Nikolajは、コールごとにsatのモデルを追跡し、あなたが概説した方法に従うとunsatが得られたら最後のモデルを返す必要があります。
しかし、繰り返し呼び出しをすべて避ける別の方法があるかもしれません。満足感の問題の代わりに、問題を最適化問題として投げかけることができます。あなたは制御変数b0、b1、.. bnを持っていると述べましたが、それは満足のいくモデルのためにtrueに設定されている数を最小にしたいと思っています。これらの変数の数を数えるメトリックを作成します。何かのように：次に
metric = (if b0 then 1 else 0)
+ (if b1 then 1 else 0)
+ ...
+ (if bn then 1 else 0)
metricを最小限に抑えるためにZ3の最適化ルーチンを使用します。私はこれが1つのコールだけであなたが探している解決策を提供すると信じています。
いくつかの有用な参考文献：http://rise4fun.com/z3opt/tutorialcontent/guide：
ここでZ3最適化チュートリアルです。
この例では、特にソフト制約について説明しており、あなたのケースでも同様に適用される可能性があります。http://rise4fun.com/z3opt/tutorialcontent/guide#h25。
ここに、オプティマイザのC++ APIリファレンス：http://z3prover.github.io/api/html/classz3_1_1optimize.htmlがあります。
ありがとう！それは非常に便利です！ – Pedro
ありがとうございました！ – Pedro