Enumerating k-SAT functions

How many k -SAT functions on n boolean variables are there? What does a typical such function look like? Bollobas, Brightwell, and Leader conjectured that, for each fixed k >= 2, the number of k-SAT functions on n variables is (1+o(1))2((n/k)+n), or equivalently: a 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 Turan density problem for partially directed hypergraphs. Our proof uses the hypergraph container method. Furthermore, we confirm the Bollobas-Brightwell-Leader conjecture for k = 4 by solving the corresponding Turan density problem.