SAT 전처리를위한 해시 함수

Question

절 데이터베이스로 구성된 SAT 인스턴스를 사전 처리하는 동안 모든 변수에 단어를 할당해야합니다. 해시 함수는 각 변수에 대해 16 개의 최상위 비트 (MSB) 중 하나의 비트와 16 개의 최하위 비트 (LSB) 중 하나의 비트를 제외하고는 0으로만 구성된 32 비트 워드를 반환합니다. 변하기 쉬운. 절의 서명은 모든 변수의 해시 함수 값의 비트 OR입니다.

이 해시 함수는 어떻게 구현합니까?

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