Constructing Minimal Perfect Hash Functions Using SAT Technology


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



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.




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.



AAAI Technical Track: Constraint Satisfaction and Optimization