z3でブール変数の優先順位を設定できますか？

Question

質問は説明が少し難しいので、私は私の質問を説明するために小さな例を使用します。 ブール変数a、b、cである命題数式集合があるとします。 z3を使用してこの数式セットの真理値代入を取得する場合、変数の優先順位を設定する方法はありますか？つまり、優先順位が> b> cの場合、検索プロセス中にz3が最初にaが真であると仮定し、aが真であることが不可能な場合はbが真であると仮定します。言い換えれば、z3が真の割当てを与えるならば、前述の優先順位の下でa、b、cではないということは、aがbと比較して優先度が高いため真実であることが不可能であることを意味する。私は質問をはっきりと記述したいと思っています。

Answer 1

現在のリリース（v4.3.1）では簡単に実行できません。私が見ることができる唯一の方法は、Z3ソースコード（http://z3.codeplex.com）をハック/修正することです。優先順位の設定は、一部のアプリケーションでは便利な機能ですが、いくつかの問題があります。

まず、Z3は問題を解決する前にいくつかの変換（前処理ステップとも呼ばれます）を適用します。変数は作成され、削除されます。したがって、元の問題のケース分割優先度は、Z3によって解決される実際の問題（すべての変換を適用した後に生成される問題）では無意味である可能性があります。

劇的な例の1つは、ビットベクトルのみを含む式です。デフォルトでは、Z3はこの式を命題論理に縮小し、命題SATソルバーを呼び出します。この削減では、すべてビットベクトル変数は削除されます。

Z3は、ソルバーとプリプロセッサの集合です。デフォルトでは、Z3は自動的にソルバを選択します。これらのソルバの中には、全く異なるアルゴリズムを使用するものがあります。したがって、提供される優先順位は、使用されているソルバにとっては役に立たない可能性があります。

GManNickGとして指摘されているように、特定のソルバーの位相選択戦略を設定することができます。詳細については、彼のコメントに掲載されている記事を参照してください。