SAT-Based Search for Minwise Independent Families

Abstract

Optimal minwise independent families of permutations are combinatorial structures designed to realize a large set of highly symmetric monotonicity patterns while using as few permutations as possible. Such families play a central role in efficient Jaccard similarity estimation and related applications in document analysis and machine learning. While practical variants often tolerate slight relaxations of their attributes, we focus on the computational construction of minwise independent families in their pure form. We introduce a constraint-based framework that (i) provides a direct SAT encoding of the underlying combinatorial conditions and (ii) extends a heuristic by Mathon and van Trung to guide the search within this constrained space. Our results show that this hybrid approach is effective in discovering new, provably optimal families and yields substantial speed-ups compared to previous methods. The framework also offers structural insights into these combinatorial objects and supports them with certified optimality proofs.