proving specific language is a NP-Complete

I got this question and I'd happy for help.

$Satn^7$ is a language that containes all the CNF formula (P) which fulfill the next rule: There is a least $n^7$ satisfactory assignments, when n is the number of the variable in P.

I need to prove that $Satn^7$ is NP-Complete.

I tried reduction from SAT, when I add variable for each clause. But my big problem is that n is not known during the reduction, and also the number of variable for adding is change, and I didn't succss to find a rule about this changes.

Thank you

-
What is "stationing"? Do you mean assignments? – Gadi A Jun 3 '11 at 17:16
Yes, I fixed it. – Eyal Jun 3 '11 at 17:41

The solution, as you already said, is by adding "dummy" variables, but not into existing clauses but into a new one which can always be satisfied (something like $(y\vee \neg y)$. Each new variable doubles the number of satisfying assignments, so it grows exponentially. Now, given that you add $k$ new variables, then the size of the output, $n$, is the size of P plus some linear function in $k$ and it can be computed by the machine performing the reduction.

-
Thank you, It helps me. But I still don't understand How I can to know the number of varuables in P? as I understood, You say that the reducntion's function will be calculate the number of new variables, and adding them to P. But is it polynomial algorithm? and also - where we take care of the fact that this is $n^7$? I need to add 7 caluses for one variable? – Eyal Jun 3 '11 at 17:39
Go over P, bit by bit; each time you see a new variable, add it to a linked list; at the end sort the list and remove all duplicate values, and count its length. This is very obviously polynomial (and usually in such questions this implementation details are not needed) – Gadi A Jun 3 '11 at 18:56
As for $n^7$ - the only thing you need is to claim that there is a relatively small $k$ such that $2^k$ (number of satisfying assignments) is larger than $n^7$, n being the size of the new formula (hence linear in $k$). This happens for all $n^d$, for every constant $d$, since the exponential function grows much faster than polynomials. – Gadi A Jun 3 '11 at 18:57
@Gadi A: Thank you. I write the prove, but I have a difficult to prove the other side. If I have, for example CNF formula like this: $(x_1) and (not(x_1)) and (x_2) and (not(x_2))$, this is NOT satisfied, but in SATn^7 it will satisified. – Eyal Jun 4 '11 at 8:29
Why is it satisfied in SATn^7? You still can't satisfy both the $x_1$ clause and the $\neg x_1$ clause. – Gadi A Jun 4 '11 at 8:41