问题标签 [bitvector]

数据由几条记录组成。一条记录如下：[位向量，数值向量，几个数值]。位向量对于每条记录具有不同的长度，对于数字向量也是如此。每条记录的数值数量是所有记录的常数。

输出是 2 个数字。它们的值（均在 [0.0, 1.0] 范围内）用于搜索算法中的评估/适应度函数逼近。

所以，我的问题是：如何为神经网络表示/标准化这些数据？特别是，是否有一种（棘手的）方法可以紧凑地表示位向量？它的长度可以达到几千。

我有一个关于使用位向量方法来查找字符串是否具有唯一字符的问题。我已经看到那些解决方案（其中之一）适用于 ASCII 和 UTF-16 字符集。

但是，相同的方法将如何适用于 UTF-32？Java中最长的连续位向量可以是长变量吗？UTF-16 需要 1024 个这样的变量。如果我们采用相同的方法，它将需要 2^26 个长变量（我认为）。是否可以使用位向量来解决如此大的字符集？

如何使用“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，但也没有列出这些细节。太令人沮丧了。

我们有一个有很多实例的类并且遇到了内存问题。因此，我们尽量减少这个类的内存需求。一个想法如下。

该类有许多布尔实例变量，在幼稚的实现中，每个变量都会占用一个单词。可以考虑将它们组合成一个存储在 int 中的迷你位向量，这样它们的组合内存需求将是一个单词。

但我怀疑 Java VM 无论如何都在进行这种优化，因此手动执行它不会获得任何额外的节省。正确的？

我正在尝试使用为每种化合物预先计算的 Avalon 指纹对化学数据库执行子结构搜索。在 RDKit 中有一种方法可以比较这些指纹：

DataStructs.AllProbeBitsMatch ( fp1, fp2 )

文档这样描述此方法：“如果第一个参数中的所有位与第二个参数中的泡菜定义的向量中的所有位匹配，则返回 True”。

他们谈论位向量，但这个指纹也可以“作为单词”计算（整数数组，通过 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

我有一个位向量来指示空元素：

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

并且只存储非空元素：

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

我想评估一个谓词： big then 5

我将非空元素与 5 进行了比较，得到了一个位向量：

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

我想为所有元素获得一个位向量：

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

粗体中的 0 是 null 元素，应该是 false。

我的代码很丑陋，有没有办法让它变快？太谢谢了！

我已经从使用 Int 切换到 SMT 中的位向量。但是，逻辑 QF_BV 不允许在您的脚本中使用任何量词，我需要定义 FOL 规则。我知道如何消除存在量词，但全称量词？怎么做？

想象一下这样的代码：

我正在寻找一种高效的（在空间和时间上）数据类型，它可以保存 384 位向量并支持高效的 XOR 和“位计数”（位数设置为 1）操作。

下面，请找到我的演示程序。我需要的操作都在SOQuestionOps类型类中，我已经为Natural和实现了它Data.Vector.Unboxed.Bit。尤其是后者似乎很完美，因为它有一个zipWords操作应该允许我进行“位计数”和逐字异或而不是逐位运算。它还声称存储打包的位（每字节 8 位）。

因此，让我们计算最佳情况下的数字：lotsOfVecs不需要分配太多，因为它只是相同 vector 的 10,000,000 倍initialVec。foldl 显然会在每个折叠操作中创建这些向量之一，因此它应该创建 10,000,000 个位向量。位计数应该创建除 10,000,000Int秒之外的任何值。因此，在最好的情况下，我的程序应该使用非常少（并且是恒定的）内存，并且总分配量应该大致为 10,000,000 * sizeof(bit vector) + 10,000,000 * sizeof(int) = 520,000,000 bytes 。

好的，让我们运行程序Natural：

让我们制作initialVec :: Natural，编译

结果（这是 GHC 7.10.1）：

其中有1,280,306,112 bytes allocated in the heap，这在预期数字的范围内（2x）。顺便说一句，在 GHC 7.8 上，这分配了 353,480,272,096 字节并运行了绝对年龄，因为popCount在 GHC 7.8 上效率不高Natural。

编辑：我稍微更改了代码。在原始版本中，所有其他向量都0在折叠中。这为版本提供了更好的分配数字Natural。我改变了它，使向量在不同的表示（设置了许多位）之间交替，现在我们看到2x了预期的分配。Natural这是(and )的另一个缺点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

第二个约束对我来说更重要；在我的情况下，它会扩展：假设它可能变成 [N] 数的最高位必须总和为 [M]。

我不确定为什么 z3 没有给出正确的结果。有什么提示吗？非常感谢。

更新：感谢克里斯托夫的回答。这是一个快速修复：

• Extract(3,3,x) -> ZeroExt(SZ, Extract(3,3,x)) 其中 SZ 是 RHS 的位宽减 1。

有没有任何有效的方法可以i从位向量中提取位数，同时i具有Int数据类型？换句话说，是否有任何高效的 smt 脚本可以执行以下脚本的功能？

先感谢您。