Constructing Minimal Perfect Hash Functions Using SAT Technology

Authors

  • Sean Weaver National Security Agency
  • Marijn Heule Carnegie Mellon University

DOI:

https://doi.org/10.1609/aaai.v34i02.5529

Abstract

Minimal perfect hash functions (MPHFs) are used to provide efficient access to values of large dictionaries (sets of key-value pairs). Discovering new algorithms for building MPHFs is an area of active research, especially from the perspective of storage efficiency. The information-theoretic limit for MPHFs is 1/ln 2 ≈ 1.44 bits per key. The current best practical algorithms range between 2 and 4 bits per key. In this article, we propose two SAT-based constructions of MPHFs. Our first construction yields MPHFs near the information-theoretic limit. For this construction, current state-of-the-art SAT solvers can handle instances where the dictionaries contain up to 40 elements, thereby outperforming the existing (brute-force) methods. Our second construction uses XORSAT filters to realize a practical approach with long-term storage of approximately 1.83 bits per key.

Downloads

Published

2020-04-03

How to Cite

Weaver, S., & Heule, M. (2020). Constructing Minimal Perfect Hash Functions Using SAT Technology. Proceedings of the AAAI Conference on Artificial Intelligence, 34(02), 1668-1675. https://doi.org/10.1609/aaai.v34i02.5529

Issue

Section

AAAI Technical Track: Constraint Satisfaction and Optimization