The Long, the Short and the Random

We furnish solid evidence, both theoretical and empirical, towards the existence of a deterministic algorithm for random sparse $\#Ω(\log n)$-SAT instances, which computes the exact counting of satisfying assignments in sub-exponential time. The algorithm uses a nice combinatorial property that every CNF formula has, which relates its number of unsatisfying assignments to the space of its monotone sub-formulae.