10

私は、用語の書き換えを使用して固定サイズのビットベクトル算術問題を解決/簡素化することに焦点を当てたプロジェクトに取り組んでいます。これは、ビットブラストに基づくものなどの決定手順の前のステップとして役立つものです。書き換えという用語は、問題をまったく解決するか、そうでなければ、はるかに単純な同等の問題を生成する可能性があるため、両方を組み合わせると、かなりの速度向上が得られます。

多くの SMT ソルバーがこの戦略を実装していることは承知しています (Boolector、Beaver、Alt-Ergo、Z3 など)。一般に、著者がそのような単純化の手順をいくつかの段落で説明している論文しか見つけられませんでした。用語の書き換えの使用法を詳細に説明しているドキュメントを見つけたいと思います: ルールの例を提供し、AC 書き換えおよび/または他の等式公理の利便性について議論し、書き換え戦略の使用など.

今のところ、CVC Lite によって実行される正規化/単純化の手順について説明しているテクニカル レポートA Decision Procedure for Fixed-Width Bit-Vectorsを見つけました。このようなテクニカル レポートをもっと見つけたいと思います! STP での用語の書き換えに関するポスターも見つけましたが、これは簡単な要約にすぎません。

私はすでにそれらの SMT ソルバーの Web サイトにアクセスし、それらの出版物ページを検索しました...

よく知られているSMTソルバーの現在のバージョンで用語の書き換えがどのように使用されているかについての参照または説明をいただければ幸いです。Z3 は最もスマートな単純化フェーズの 1 つを備えているように見えるので、特に Z3 に興味があります。たとえば、Z3 3.* では新しいビット ベクトル決定手順が導入されましたが、残念ながら、それについて説明している論文を見つけることができませんでした。

4

2 に答える 2

14

仰るとおりです。最新の 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 = y+z+wおよび でx発生したとします。次に、 を削除すると、 、、およびが得られます。を削除しましたが、元の式よりも多くの加算器があります。p(x+z)p(x+2*z)p(x+3*z)p(x+4*z)xp(y+2*z+w)p(y+3*z+w)p(y+4*z+w)p(y+5*z+w)x

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

  • 次に、単純化の別のラウンドが実行されます。今回は、ローカルのコンテキスト単純化が実行されます。これらの単純化は潜在的に非常に高価です。そのため、訪問するノードの最大数に関するしきい値が使用されます (デフォルト値は 1000 万です)。ローカル コンテキストの単純化には、次のような規則が含まれます。

(x != 0 or  y = x+1) ->  (x != 0 or y = 1)
  • 次に、分配性を使用して乗数の数を最小化しようとします。例：

a b + a c -> (b+c)*a

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

  • 式に等号、連結、抽出、および同様の演算子のみが含まれている場合。次に、Z3 は、union-find および congruence クロージャに基づく特殊なソルバーを使用します。

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

于 2011-11-29T07:10:42.107 に答える
2

Z3 は、前処理中に実行される多くの単純化に書き換えを使用します。UFBV 戦略 (量指定子を使用) に使用される書き換え規則の多くは、次の論文で詳細に説明されています。

Wintersteiger、Hamadi、de Moura: 効率的に定量化されたビット ベクトル式を解く、FMCAD、2010

于 2011-11-25T19:03:36.710 に答える