What is the maximal length of a CNF formula?

Question

The question is quite short. Let $k$ be a given number. What is the maximal length of $k$-CNF formulae can we compute, over the set of binary variables $\left\{ x_1 ,\ldots, x_n \right\}$?

The way I see it, if we ignore the $k$ for a minute, we have $2^n$ different binary sequences, each sequence is a $1-1$ representation of a clause over $n$ variables.

This means that we already have $2^n$ different clauses, so the maximal length of a clause is $2^n$.

In here, we assumed each variable must either appear as $x_i$ or as its negation. And we didn't count the instances in which a variable does not appear and the length of a clause is less than $n$. So it might actually be $3^n$...

This is a huge number...

But what happens when we consider the size of each clause has (ver1: at most, ver2: exactly) $k$ literals?

I tried going at it in the following way:

Lets look at $2n$ possible literals...

We need to choose $k$ of them. So its $\left( \frac{2n}{k}\right)$ different possibilities (I meant $2n$ over $k$, not division...).

This is $\frac{(2n-k+1) \cdot \ldots \cdot 2n}{k!}$

And I'm at loss how to continue from here.

Also, looks like the answers I get are not the same (if, for example, $k=n$).

Clarification: I provide 2 definitions for $k$-CNF formula, and I am interested in both possibilities (versions). For both, a literal cannot appear more than once in the same clause and if a literal appears, its negation cannot appear (or we might as well remove this clause all together). Additionally, if a clause appeared, it won't appear again (orelse, there is no actual limit on the length of a formula). In the first version, a clause has exactly $k$ literals. In the second, at most $k$ literals.

Answer 1

For the version where every clause must have exactly $k$ literals:

There are ${n \choose k} 2^n$ possible clauses. (Why? Because you must choose exactly $k$ of the variables to appear in the clause, and then for each variable, you choose whether it appears negated or not.) A formula is obtained by choosing some subset of those possible clauses. So, the total number of possible formulas is

$$2^{{n \choose k} 2^n}.$$

---

For the version where every clause must have exactly $k$ literals:

By similar reasoning, the number of possible clauses is given by

$$c = \sum_{i=0}^k {n \choose i} 2^i.$$

It follows that there are exactly $2^c$ possible formulas.