基于 SAT 的最小独立置换族搜索

为了用于搜索引擎中的快速文档相似度估计，著名的最小独立性质对 $\{1,\ldots, n\}$ 的置换族 $\mathcal{F}$ 施加了高度对称的约束：如果对于每个 $j\in \{1,\ldots,n\}$、任意基数为 $j$ 的子集 $X\subseteq \{1,\ldots,n\}$ 以及任意固定元素 $x^\ast\in X$，从 $\mathcal{F}$ 中随机抽取的置换 $\pi$ 满足 $\pi(x^\ast)=\min \{\pi(x) : x\in X\}$ 的概率为 $1/j$，则 $\mathcal{F}$ 满足该性质。核心关注点在于找到满足上述约束且成员数尽可能少的置换族。我们提供了一个框架，首先，它被实现为纯 SAT 模型；其次，它将 Mathon 和 van Trung 的启发式方法推广到这些置换族的搜索中。后者最初强制执行底层的群论分解，以加速可与所谓秩独立置换族相关联的结构的计算机辅助搜索。我们观察到，该方法同样适用于寻找已被证明最优的最小独立置换族新代表，同时也能带来显著的加速。由于该问题的朴素搜索空间大小至少为 $(n!)^n$，我们也仔细处理了对称性破缺。最后，我们为 Bargachev 在推导最小秩独立置换族成员数下界时遇到的问题提供了一个双射证明。