Хеширование битового состояния
Хеширование битового состояния — это метод хеширования , изобретенный Моррисом в 1968 году. [1] Он используется для хеширования состояний, где каждое состояние (например, автомата) представляется числом и передается некоторой хеш-функции .
Результат функции затем принимается как индекс массива битов ( битовое поле ), где ищется 1, если состояние уже наблюдалось ранее, или сохраняется 1 отдельно, если нет.
Обычно он служит методом «да-нет» без необходимости хранения полного представления битов состояния.
Недостатком этой структуры является потеря точности, как и в других методах хеширования. Следовательно, некоторые инструменты используют этот метод с более чем одной хэш-функцией, так что битовое поле расширяется за счет количества используемых функций, каждая из которых имеет свою собственную строку. И даже после того, как все функции возвращают значения (индексы) указывают на поля с содержимым, равным 1, состояние можно назвать посещенным с гораздо большей вероятностью.
Хеширование битового состояния, хотя и было предложено ранее, представляет собой применение фильтров Блума . [2]
Использовать
[ редактировать ]- Хеширование битового состояния используется в средстве проверки модели SPIN для определения того, посещалось ли состояние уже алгоритмом вложенного поиска в глубину или нет. Якобы это привело к экономии памяти 98% в случае использования одной хеш-функции (от 175 МБ до 3 МБ) и 92% при использовании двух хеш-функций (13 МБ). В первом случае государственное покрытие упало до 97%. [3]
Ссылки
[ редактировать ]- ^ Моррис, Р. (1968). Методы разбросанного хранения
- ^ Эделькамп С. и Штейн Б. (ред.). (2004). Новые результаты в планировании, составлении графиков и дизайне (Puk2004): Семинар; Слушания . Университет Ульма.
- ^ Хольцманн, GJ (2003) Аддисон Уэсли. Spin Model Checker, The: Учебное пособие и справочное руководство