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
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.