Number of instances of SAT (boolean satisfiability) problems of size N?

I assume the size of an instance of the SAT problem is measured by its number of (Boolean) variables. What is total number of instances of SAT problems of size N?

I guess that amounts to counting the number of "distinct" formulas that can be formed by N boolean variables, using a normal form such as CNF or DNF.

Update: this question is partly answered for the 3SAT case:
https://cstheory.stackexchange.com/q/2168/15553

and the number of distinct clauses is:
$$ C = 2N \times 2(N-1) \times 2(N -2) / 3! = 4 N(N-1)(N-2)/3 $$

If you consider 3-Conjunctive Normal Form (3CNF) (every clause has exactly three literals) and you allow clauses with repeated variables, then it is easy to see that using $N$ variables the number of different 3SAT clauses is $(2N)^3$
($2N$ because every literal can appear unnegated or negated).

So the total number of distinct 3CNF formulas (without repeated clauses) is $2^{(2N)^3}$.

But be careful because the "size" of a 3CNF formula (e.g. considered as an input of a decision problem) is usually the size of its representation. For example, using alphabet $\Sigma = \{0,...,9,``,",-\}$
the 3CNF formula $(x_1\lor\bar{x}_2\lor x_3)\land (\lor x_2 \lor \bar{x}_3 \lor \bar{x}_4)$ can be represented with the string:

1,-2,3,2,-3,-4

and its length is 14.

StackExchange Computer Science Q#22054, answer score: 6