SMTソルバーは、次のように、疑似ブール問題の解（または割り当て）を効率的に見つけることができますか？
\sum {i..m} f_i x1 x2.. xn *w_i
ここf_i x1 x2 .. xnで、はブール関数であり、w_iはInt型の重みです。
便宜上、1ページと3ページの内容を強調表示します。これは、疑似ブール問題を指定するのに十分です。
2 に答える
3
SMT ソルバーは通常、以下の質問に対処します。論理式が与えられた場合、基礎となる理論 (算術理論、ビットベクトル、配列の理論など) からの関数と述語をオプションで使用して、その式が満足できるかどうかです。通常、これらは目的関数を指定する方法を公開しておらず、通常、最適化手順が組み込まれていません。
いくつかの特別なケースは、ブール値のみ、またはブール値とビットベクトルまたは整数の組み合わせを使用する式です。疑似ブール制約は、ビットベクトルを使用して整数またはエンコード (オーバーフロー セマンティクスを考慮して) で定式化するか、SAT に直接エンコードすることができます。疑似ブール問題のクラスに分類される制限された整数を使用する一部の数式では、Z3 はビット ベクトルへの自動削減を試みます。これは、QF_LIA としてタグ付けされた SMT-LIB2 形式のベンチマーカーにのみ適用されるか、この削減を実行するタクティックを明示的に呼び出す場合に適用されます (「qflia」タクティックが適用されます)。
Z3 は目的関数を直接公開していませんが、SMT ソルバーに目的関数を追加するという問題は、研究コミュニティで積極的に追求されています。SAT 2006 で Nieuwenhuis と Oliveras によって提案された 1 つのアプローチは、カスタム理論として「加重最大 SMT」問題の解決を組み込むことでした。Yices には加重最大 SMT の機能が組み込まれていますが、Z3 にはありませんが、加重最大 SMT ソルバーのバックトラッキング検索を実行するカスタム理論を作成することは可能ですが、すぐに使用できるものは何もありません。
定量化された式を使用して目的関数を指定しようとすることがあります。理論的には、量指定子の除去手順が目的を解決できることを期待できます。パフォーマンスに関しては、これは一般的にかなり悪いです。数量子の除去は過適合であり、(私たちが持っている) ルーチンは効率的ではありません。
于 2012-11-18T13:34:34.780 に答える