Enumerating k-SAT functions

TL;DR

This paper proves the conjecture that most $k$-SAT functions are unate by linking the enumeration problem to Turán density in hypergraphs, using the hypergraph container method, and confirms the conjecture for $k=4$ and $k=5$.

Contribution

It establishes the equivalence between counting $k$-SAT functions and a Turán density problem, and confirms the conjecture for $k=4$ and $k=5$ using advanced combinatorial methods.

Findings

Confirmed the conjecture for $k=4$ using Turán density solutions.

Confirmed the conjecture for $k=5$ via computer search.

Linked $k$-SAT function enumeration to hypergraph Turán problems.

Abstract

How many $k$-SAT functions on $n$ boolean variables are there? What does a typical such function look like? Bollob\'as, Brightwell, and Leader conjectured that, for each fixed $k \ge 2$, the number of $k$-SAT functions on $n$ variables is $(1+o(1))2^{\binom{n}{k} + n}$, or equivalently: a $1-o(1)$ fraction of all $k$-SAT functions are unate, i.e., monotone after negating some variables. They proved a weaker version of the conjecture for $k=2$. The conjecture was confirmed for $k=2$ by Allen and $k=3$ by Ilinca and Kahn. We show that the problem of enumerating $k$-SAT functions is equivalent to a Tur\'an density problem for partially directed hypergraphs. Our proof uses the hypergraph container method. Furthermore, we confirm the Bollob\'as--Brightwell--Leader conjecture for $k=4$ by solving the corresponding Tur\'an density problem. Our solution applies a recent result of F\"uredi and Maleki on the minimum triangular edge density in a graph of given edge density. In an appendix (by Nitya Mani and Edward Yu), we further confirm the $k=5$ case of the conjecture via a brute force computer search.