質問を説明するのは少し難しいので、小さな例を使用して質問を説明します。要素がブール変数a、b、cである命題式セットがあるとします。z3を使用してこの数式セットの真の割り当てを取得する場合、変数の優先度を設定する方法はありますか？つまり、優先度がa> b> cの場合、検索プロセス中にz3は最初にaが真であると見なし、aが真であることが不可能な場合は、bが真であると見なします。言い換えると、z3が真理の割り当てを与える場合：前述の優先度の下でa、b、cではなく、aはbと比較して優先度が高いため、aが真になることは不可能であることを意味します。質問を明確に説明してください。
1 に答える
4
現在のリリース (v4.3.1) では、これを行う簡単な方法はありません。私が確認できる唯一の方法は、Z3 ソース コード ( http://z3.codeplex.com ) をハック/変更することです。優先度の設定が一部のアプリケーションにとって便利な機能であることには同意しますが、いくつかの問題があります。
まず、Z3 は問題を解決する前にいくつかの変換 (別名、前処理ステップ) を適用します。変数が作成され、削除されます。したがって、元の問題のケース分割優先度は、Z3 によって解決される実際の問題 (すべての変換を適用した後に生成される問題) にとっては意味がない場合があります。
劇的な例の 1 つは、ビット ベクトルのみを含む数式です。デフォルトでは、Z3 はこの式を命題ロジックに縮小し、命題 SAT ソルバーを呼び出します。この縮小では、すべてのビット ベクトル変数が削除されます。
Z3 は、ソルバーとプリプロセッサのコレクションです。デフォルトでは、Z3 はユーザーのためにソルバーを自動的に選択します。これらのソルバーの中には、まったく異なるアルゴリズムを使用するものがあります。そのため、指定された優先順位は、使用されているソルバーには役に立たない場合があります。
GManNickGが指摘したように、特定のソルバーに対してフェーズ選択戦略を設定することが可能です。詳細については、彼のコメントで提供された投稿を参照してください。
于 2013-01-13T16:03:55.663 に答える