SAT前処理用のハッシュ関数

Question

節データベースで構成されるSATインスタンスの前処理中に、すべての変数に単語を割り当てる必要があります。ハッシュ関数は、各変数について、16の最上位ビット（MSB）のうちの1つのビットと、16の最下位ビット（LSB）のうちの1つのビットを除いて、0からなる32ビットワードのみを返します。変数。節の署名は、すべての変数のハッシュ関数値のビットごとの論理和です。

このハッシュ関数を実装するにはどうすればよいですか？

Answer 1

まあ、各ハーフワードには16の可能性があります。 1は16箇所にあります。これにより16x16 = 256の可能な "ハッシュ"が得られます。変数count> 256の場合、間違いなく衝突が発生します。あなたができることは、ハッシュ関数に渡す前にv % 256を渡すことです。これは、そのようなハッシュ関数の1つです：

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