枚举 k-SAT 函数

在 $n$ 个布尔变量上有多少个 $k$-SAT 函数？这样一个典型函数是什么样子的？Bollob\'as、Brightwell 和 Leader 猜想：对每个固定的 $k \ge 2$，$n$ 个变量上的 $k$-SAT 函数个数为 $(1+o(1))2^{\binom{n}{k} + n}$，或等价地：比例为 $1-o(1)$ 的所有 $k$-SAT 函数是单式的（unate），即在否定某些变量后单调。他们对 $k=2$ 证明了该猜想的一个较弱版本。该猜想对 $k=2$ 由 Allen 证实，对 $k=3$ 由 Ilinca 和 Kahn 证实。我们证明枚举 $k$-SAT 函数的问题等价于部分有向超图的 Tur\'an 密度问题。我们的证明使用了超图容器方法。此外，我们通过求解相应的 Tur\'an 密度问题证实了 Bollob\'as--Brightwell--Leader 猜想在 $k=4$ 的情形。我们的解法应用了 F"uredi 和 Maleki 关于给定边密度的图中最小三角边密度的最近结果。在附录中（由 Nitya Mani 和 Edward Yu 撰写），我们通过暴力计算机搜索进一步证实了该猜想的 $k=5$ 情形。