用于 SAT 预处理的哈希函数

【问题标题】：A hash function for SAT preprocessing用于 SAT 预处理的哈希函数
【发布时间】：2012-01-05 11:00:44
【问题描述】：

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

如何实现这个哈希函数？

【问题讨论】：

标签： hash logic boolean-logic satisfiability

【解决方案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;
}

【讨论】：