用於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; 
}