問題タブ [bitvector]

データは複数のレコードから構成されています。レコードは次のとおりです: [ビット ベクトル、数値ベクトル、いくつかの数値]。ビット ベクトルの長さはレコードごとに異なり、数値ベクトルについても同じことが言えます。レコードごとの数値の数は、すべてのレコードの定数です。

出力は 2 つの数値です。それらの値 (両方とも [0.0, 1.0] の範囲) は、検索アルゴリズムで評価/適合度関数の近似に使用されます。

だから、私の質問は次のとおりです:ニューラルネットワークのこれらのデータをどのように表現/正規化するのですか? 特に、ビットベクトルをコンパクトに表現する (トリッキーな) 方法はありますか? その長さは最大数千です。

「repeat」および「rotate_left」ビットベクトル操作はどのように使用しますか?

より一般的に言えば、Z3 で使用される SMT2 スクリプト形式でのビットベクター操作の詳細なドキュメントはどこにありますか?

私が見つけたものはすべて、チュートリアルまたは壊れたリンクに行くようです:
https://github.com/Z3Prover/z3/wiki/Documentation
http://research.microsoft.com/en-us/um/redmond/projects/z3 /old/documentation.html

「repeat」、「rotate_left」、「rotate_right」を当て推量で理解しようとすると、イライラしてしまいます。それらの使い方がわかりません。例えば

与える

ドキュメントはどこにありますか? これはすべて標準であるため、彼らが説明していないことを願って、smt-lib.orgも見ましたが、これらの詳細もリストされていません。とてもイライラします。

すべての化合物について事前に計算された Avalon フィンガープリントを使用して、化学データベースで部分構造検索を実行しようとしています。これらのフィンガープリントを RDKit で比較する方法があります。

DataStructs.AllProbeBitsMatch ( fp1, fp2 )

ドキュメントでは、このメソッドを次のように説明しています。

彼らはビットベクトルについて話しますが、このフィンガープリントは「単語として」計算することもできます (整数の配列、RDKit の GetAvalonFPAsWords メソッドを介して、MongoDB に保存し、できれば RDKit なしでデータベースの力のみを使用して検索を実行できます (これは必要です)はるかに高速になります）。

これが私の質問です。ビット ベクトルの AllProbeBitsMatch と同等の配列の操作が必要です。理想的には、この操作は MongoDB で実行する必要があります。おそらく、パフォーマンスを向上させるために集約機能を使用します。

これは、参照用に使用する RDKit および Avalon フィンガープリントの記事です: http://rdkit.blogspot.com/2013/11/fingerprint-based-substructure.html

私は寄木細工のファイル形式を扱っています。例えば：

データのグループ:

1 2ヌル3 4 5 6ヌル7 8ヌル ヌル9 10 11 12 13 14

null 要素を示すビット ベクトルを取得しました。

1 1 0 1 1 1 1 0 1 1 0 0 1 1 1 1 1 1

null 以外の要素のみを保存します。

1 2 3 4 5 6 7 8 9 10 11 12 13 14

述語を評価したい: big then 5

非 null 要素を 5 と比較し、ビット ベクトルを取得しました。

0 0 0 0 0 1 1 1 1 1 1 1 1

すべての要素のビット ベクトルを取得したい:

0 0 0 0 0 1 0 1 1 0 0 1 1 1 1 1 1

太字の 0 は null 要素です。false にする必要があります。

私のコードはかなり醜いです。とにかく速くする方法はありますか? まことにありがとうございます！

SMT で Int から Bit Vector を使用するように切り替えました。ただし、ロジック QF_BV では、スクリプトで量指定子を使用できないため、FOL ルールを定義する必要があります。存在量指定子を削除する方法は知っていますが、普遍的な量指定子は? どうやってするか？

次のようなコードを想像してください。

384ビットベクトルを保持でき、効率的なXORと「ビットカウント」（1に設定されたビット数）操作をサポートする効率的な（空間と時間の両方で）データ型を探しています。

以下に、私のデモプログラムを見つけてください。必要な操作はすべてSOQuestionOps型クラスにあり、 と に実装しましNaturalたData.Vector.Unboxed.Bit。特に後者は、zipWords「ビットカウント」やビットごとではなく単語ごとの XOR などの操作を実行できる操作があるため、完璧に思えます。また、パックされたビット (1 バイトあたり 8 ビット) を格納すると主張しています。

それでは、最良のケースの数値を計算してみましょう。lotsOfVecs同じ vector の 10,000,000 倍にすぎないため、多くを割り当てる必要はありませんinitialVec。foldl は明らかに、フォールド操作ごとにこれらのベクトルの 1 つを作成するため、10,000,000 ビット ベクトルを作成する必要があります。ビット カウントは、10,000,000Int秒以外のものを作成する必要があります。したがって、最良の場合、私のプログラムはごくわずかな (そして一定の) メモリを使用する必要があり、割り当ての合計はおよそ 10,000,000 * sizeof(bit vector) + 10,000,000 * sizeof(int) = 520,000,000 バイトになるはずです。

では、次のプログラムを実行してみましょうNatural:

作っinitialVec :: Naturalてコンパイルしよう

結果 (これは GHC 7.10.1 の場合):

これは1,280,306,112 bytes allocated in the heap、予想される数字の球場 (2x) にあります。GHC 7.8 では、これは 353,480,272,096 バイトを割り当て、GHC 7.8popCountではあまり効率的ではないため、絶対年齢に対して実行されNaturalます。

編集：コードを少し変更しました。元のバージョンでは、他のすべてのベクトルが0フォールドに含まれていました。Naturalこれにより、バージョンの割り当て数値が大幅に向上しました。ベクトルが異なる表現 (多くのビットが設定された状態) に切り替わるように変更したところ2x、予想される割り当てが表示されるようになりました。Naturalこれは(and )のもう 1 つの欠点ですInteger。割り当て率は値によって異なります。

しかし、もっとうまくできるかもしれません。密集した を試してみましょうData.Vector.Unboxed.Bit:

それinitialVec :: BV.Vector BV.Bitは、同じオプションで再コンパイルして再実行することです。

それは非常に遅く、割り当ての約100倍です:(。

では、両方の実行を再コンパイルしてプロファイリングしましょう ( ghc --make -rtsopts -O3 -prof -auto-all -caf-all -fforce-recomp MemStuff.hs):

Naturalバージョン:

Data.Vector.Unboxed.Bitバージョン:

Natural固定サイズのビットベクトルに最適なオプションは本当にありますか? そしてGHC 6.8はどうですか？SOQuestionOpsそして、私の型クラスを実装できるより良いものはありますか?

次の python コードを使用して、次の 2 つの 2 進数を見つけています。

• 合計して特定の数にする
• 整数にキャストされた最上位ビットの合計は 2 になる必要があります

2 番目の制約は、私にとってより重要です。私の場合、それはスケーリングします: [N] 数の最上位ビットを合計すると [M] になる可能性があるとしましょう。

z3 が正しい結果を返さない理由がわかりません。ヒントはありますか？どうもありがとう。

更新: Christoph からの回答に感謝します。ここに簡単な修正があります：

• Extract(3,3,x) -> ZeroExt(SZ, Extract(3,3,x)) ここで、SZ は RHS のビット幅から 1 を引いた値です。

データ型を持っているi間にビットベクトルからビット番号を抽出する効率的な方法はありますか? つまり、次のスクリプトが行うことを実行できる効率的な smt スクリプトはありますか?iInt

前もって感謝します。