0

手動の「追跡」変数を明示的に使用せずに、名前付き式を使用してソフト制約を実装できるかどうか疑問に思っています。

上記の最初のメッセージで説明したように手動追跡を使用するのはかなり面倒です。ソルバーへの複数の呼び出しが必要になるためです（実際2^n、ソフト制約がある場合に可能な限り多くのソフト制約のセットを取得するには、最悪の場合に呼び出しが必要になる場合がありnます） ）。これらの2つのアイデアを組み合わせて、Z3にはるかに簡単な方法でソフト制約を実装させることは可能でしょうか？これらの2つのメッセージからのアイデアに基づいて、私は素朴に次のことを試みました。

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(assert (! false :named absurd))
(check-sat)

モデルに参加することでこの不自然な例が満たされるsatので、z3が教えてくれることを期待していました。しかし、代わりに生成されました。これは合理的ですが、それほど有用ではありません。absurdfalseunsat

あなたが提供するかもしれない洞察に感謝します。または、z3が名前付き式をどのように使用するかについての詳細なドキュメントを教えてください。（私はマニュアルをざっと読みましたが、どこにも詳細に説明されているのを見ませんでした。）

4

1 に答える 1

1

名前付き式は、SMT-LIB2.0標準の一部です。Z3では、これらは補助ブール定数を使用するアプローチの単なる「構文糖衣構文」です。

SMT-LIB 2.0標準では、名前付き式は、などのコマンドの「追跡」アサーションに使用されます（ SMT-LIB 2.0リファレンスマニュアル(get-unsat-core)のセクション5.1.5を参照）。あなたの例では、を取得した後に実行すると。これがオンラインの例へのリンクです。(get-unsat-core)(check-sat)(absurd)

ソフト/ハード制約に関しては、MaxSATが必要なようです。Z3には、2つの異なるアルゴリズムを使用して、CAPIと補助ブール定数を使用してMaxSATを実装する例が付属しています。最も単純なものは、次の基本的な考え方を使用しています。

  • ソフト制約ごとに、は新しいブール変数であるC_iとアサートします。b_i implies C_ib_i

  • falseの割り当てb_iは、基本的に制約を無視しますC_i。

  • フォームの制約を使用して、多くてもfalseAtMostKであることを強制します。K b_i次に、線形探索を使用して、満たすことができるソフト制約の最大数を見つけることができます。二分探索を使用することもできます（この場合、必要なのはソフト制約の数であるlog N呼び出しのみです）。Nこのアプローチのバリエーションは、多くの疑似ブールソルバーで使用されます。

の例にexamples\maxsatは、FuとMalikによって提案されたよりスマートなアルゴリズムも含まれています。この例は、制約をエンコードする方法も示していますAtMostK。

于 2013-02-25T20:25:49.037 に答える