Bollobás–Brightwell–Leader conjecture on enumerating k-SAT functions

Let $k\geq 2$ be fixed. A $k$-SAT function on $n$ boolean variables is a Boolean function represented by a formula whose clauses have size $k$, and it is unate if it is monotone after replacing some variables with their negations.

Bollobás–Brightwell–Leader conjecture. The number of $k$-SAT functions on $n$ boolean variables is

$$(1+o(1))2^{n+\binom{n}{k}}.$$

Equivalently, a $1-o(1)$ fraction of all $k$-SAT functions on $n$ variables are unate.

This conjecture gives the asymptotically sharp count suggested by unate functions. It was proved for $k=2$ and $k=3$, while the general case remains open.