hash - 用于 SAT 预处理的哈希函数

Question

在对包含子句数据库的 SAT 实例进行预处理期间，需要为每个变量分配一个单词。散列函数为每个变量返回一个仅由 0 组成的 32 位字，除了 16 个最高有效位 (MSB) 中的一位和 16 个最低有效位 (LSB) 中的一位，这取决于设置为 1多变的。子句的签名是其所有变量的散列函数值的按位或。

如何实现这个哈希函数？

Answer 1

嗯，每个半字有 16 种可能性；1 可以在 16 个位置。这给出了 16x16=256 个可能的“哈希”。对于变量计数 > 256，您肯定会遇到冲突。您可以做的是v % 256在将其传递给散列函数之前传递。这是一种可能的散列函数：

unsigned int hash_variable(int v)
{
  v = v % 256

  assert(v < 256);

  unsigned char lower_nibble = v & 0x0f;
  unsigned char upper_nibble = (v & 0xf0) >> 4;

  assert(lower_nibble < 16);
  assert(upper_nibble < 16);

  unsigned int result = 0;

  result |= (1 << upper_nibble);
  result |= (1 << (lower_nibble + 16));
  return result;
}