ビットベクトル演算の決定手順での用語書き換えの使用

Question

私は、固定長ビットベクトル演算の問題を解決/単純化するために用語書き換えを使用することに焦点を合わせたプロジェクトに取り組んでいます。ビットブラストに基づくもののようないくつかの決定手順への前のステップ。書き換えという用語は、まったく問題を解決するか、そうでなければより簡単な同等の問題を生成する可能性があるため、両方の組み合わせによってかなりのスピードアップが生じる可能性があります。

多くのSMTソルバーがこの戦略（Boolector、Beaver、Alt-Ergo、Z3など）を実装していることを知っていますが、これらの書き換え手順を詳細に記述した論文/技術レポート/ 。一般に、私は著者がいくつかの段落でそのような簡略化のステップを記述した論文しか見つけなかった。ルールの例を提供し、AC書き換えやその他の公理の公理、書き直し戦略の使用などを論じる文書を見つけることを希望します。

今のところ私はちょうどCVC Liteで行われる正規化/簡略化の手順を説明する技術レポートA Decision Procedure for Fixed-Width Bit-Vectorsが見つかりました。このような技術レポートを探したいと思います。私も約Term rewriting in STPのポスターを見つけましたが、それは簡単な要約です。

は、私はすでに、これらのSMTソルバーのウェブサイトを訪問していると私は、現在のバージョンで使用されている私は、任意の参照、またはどのように項書換えのいずれかの説明をいただければ幸いです

...その出版ページで検索しましたよく知られたSMTソルバーの私は特に賢明な簡素化フェーズの1つを持っているように見えるので、Z3に特別に興味があります。例えば、Z3 3. *は新しいビットベクトル決定手続きを導入しましたが、残念ながらそれを記述する論文は見つかりませんでした。

Answer 1

私はあなたに同意します。最新のSMTソルバーで使用される前処理ステップを説明する論文を見つけるのは難しいです。 ほとんどのSMTソルバ開発者は、これらの前処理ステップがビットベクトル理論にとって非常に重要であることに同意します。 私は、これらの手法はいくつかの理由で公開されていないと信じています。そのほとんどは、それ自体が科学的な重要な貢献ではない小さなトリックです。ほとんどのテクニックは特定のシステムのコンテキストでのみ機能します。ソルバAでうまく動作しているように見えるかもしれないテクニックは、ソルバBでは機能しません。 オープンソースのSMTソルバを持つことが、この問題に取り組む唯一の方法だと私は信じています。たとえ特定のソルバAで使用されている手法を公開しても、ソルバAの実際の動作をそのソースコードを見ずに再現することは非常に難しいでしょう。

とにかく、ここではZ3によって実行される前処理の概要と重要な詳細があります。

• いくつかの簡素化の規則は、このサイズをローカルに縮小することができますが、グローバルに増加させる可能性があります。シンプル化は、この種の単純化によって引き起こされるメモリの爆発を避けなければならない。例は次の場所にあります。http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

• 最初の簡略化ステップでは、等価を保存するローカル簡略化のみが実行されます。 例：

2*x - x -> x 
x and x -> x 

• 次に、Z3は、定数伝播を行います。与えられた等価性t = vここで、vは値です。どこでもtの代わりにvと置き換えられます。

t = 0 and F[t] -> t = 0 and F[0] 

• 次に、ビットベクトルのガウスの消去を行います。ただし、算術式では最大で2回発生する変数のみが削除されます。 この制限は、数式の加算器と乗算器の数が増加しないようにするために使用されます。 たとえば、およびxがp(x+z),p(x+2*z),p(x+3*z)およびp(x+4*z)で発生するとします。そして、xを除去した後、我々はp(y+2*z+w),p(y+3*z+w),p(y+4*z+w)およびp(y+5*z+w)となる。 xを削除しましたが、元の数式よりも多くの加算器があります。

• 次に、拘束されていない変数を削除します。このアプローチは、Robert Brummayer博士論文とRoberto Brutomesso博士論文で説明されています。

• 次に、もう1回の簡略化が行われます。今回は、局所的な文脈単純化が行われます。 これらの単純化は潜在的に非常に高価です。したがって、訪問するノードの最大数に対するしきい値が使用されます（デフォルト値は10million）。 ローカルコンテキストの簡略化は、

(x != 0 or y = x+1) -> (x != 0 or y = 1) 

• 次にとしてルールを含む、それが分配性を使用して乗算器の数を最小化しようとします。例：

B + C - >（B + C）*

• そして、連想を適用することによって、加算器および乗算器の数を最小限にしようとしそしてcommutativity。 数式にa + (b + c)およびa + (b + d)という語句が含まれているとします。次に、Z3はそれらを(a+b)+cと(a+b)+dに書き換えます。 変換の前に、Z3は4つの加算器をエンコードする必要があります。その後、Z3は完全に共有された式を使用するため、3つの加算器のみをエンコードする必要があります。

• 式に等号、連結、抽出などの演算子しか含まれていない場合。次に、Z3は、ユニオン検索と合同閉包に基づいた特殊ソルバを使用します。

• それ以外の場合は、すべてをビットブラストし、AIGを使用してブール式を最小化し、SATソルバーを呼び出します。

Answer 2

Z3は、前処理中に実行される多くの単純化のために書き換えを使用します。 （数量付き）UFBV戦略に使用書き換えルールの多くは、以下の論文にある程度詳細に説明されています

Wintersteiger, Hamadi, de Moura: Efficiently Solving Quantified Bit-Vector Formulas, FMCAD, 2010