How many 3-SAT expressions with up to N variables are satisfiable? TL;DR

There are exactly 255 possible 3-sat expressions with exactly 3 variables (more meticulously defined below). Of those, exactly 254 are satisfiable. There are exactly 4,294,967,295 possible 3-sat expressions with exactly 4 variables. Of those, how many are satisfiable? How did you get that number?

Problem Statement

Assume you have a 3-SAT equation where all the clauses have exactly 3 distinct variables (i.e. $X$ and $\neg X$ will never appear in the same clause), and no clause appears more than once (i.e. some expression won't have both $(X \lor Y \lor \neg Z)$ and $(X \lor \neg Z \lor Y)$). With this construction, there are a finite amount of expressions with only N variables.

For the class of expressions with up to N variables, is there an equation to compute how many are satisfiable? 

Example of N=3

For example, with N=3, there are 254 solutions. 

We know this because for N=K, there are exactly $8 *\binom{K}{3}$ distinct clauses, as you must select three distinct variables for each clause, and 1 of 8 possible sign values for those variables (+/+/+, +/+/-, +/-/+, +/-/-, ...). If there are $8 *\binom{K}{3}$ possible clauses, then there must be $2^{(8 *\binom{K}{3})} - 1$ possible boolean expressions, because each clause may appear or not (so $2^{(8 *\binom{K}{3})}$) and we have to subtract one for the case with no clauses.

For N=3, there are 255 possible expressions (using the lemma above), and only one is unsatisfiable. So there must be 254 distinct satisfiable expressions.

How about for N=4?
There is almost certainly no non-trivial formula that will tell you the number of solutions. By non-trivial, I mean something not of the form
$$
\sum_{x_1, \dots, x_n\in\{0,1\}} f(x_1, \dots, x_n)\,,
$$
where
$$f(x_1, \dots, x_n)=\begin{cases}1 &amp;\text{if $x_1, \dots, x_n$ satisfies the formula}\\
0&amp;\text{otherwise.}\end{cases}
$$

Note that if we have a formula&nbsp;$F$ (trivial or otherwise) that tells us how many satisfying assignments there are, we can decide 3-SAT just by computing&nbsp;$F$ and checking whether $F=0$ (unsatisfiable) or $F&gt;0$ (satisfiable). This means that computing&nbsp;$F$ is NP-hard so, assuming that P$\,\neq\,$NP, $F$&nbsp;is difficult to compute, which suggests that $F$&nbsp;can't have any nice form.

In fact, $F$&nbsp;is complete for the complexity class #P, which is essentially at least as hard as all of the polynomial hierarchy. This means that it seems to be quite a lot harder than "just NP-hard". Furthermore, we can't even approximately compute&nbsp;$F$ in any efficient way unless P=NP. Even being able to approximate&nbsp;$F$ with exponential additive error would allow us to distinguish between $F=0$ and $F&gt;0$ and thus allow us to solve 3-SAT. For example, given a formula with $N$&nbsp;variables and $F$&nbsp;solutions, we can create a formula with $2N$&nbsp;variables and exactly the same clauses (so variables $N+1, \dots, 2N$ aren't mentioned in the formula and can take any value). This formula has $2^NF$ satisfying assignments and being able to approximate that number strictly better than $\pm 2^{N-1}$ would allow us to tell the difference between $F=0$ and $F&gt;0$.