Sketch an IP proof for minSAT
Your protocol is not very clear. What do you mean at step 3 by "it chooses one variable, re-computes the formula"? 

I assume the verifier just sets that variable to 1 and re-computes the formula without that variable.

Then, this protocol still has some problems. Let's say that there are two sets of variables that satisfy the formula: $\{x\}$ and $\{y,z\}$. The minSat is $x$.
But what happens if the prover says it is $y,z$?
the verifier checks this proposed set, and  sees that the set satisfies the formula; then the verifier removes one variable, say $y$, and sends the formula back to the prover. The prover will then reply with $\{z\}$ and the verifier will accept it.

Even if the verifier renames the variables in a random way, (say, replace $x$ with $a$ and $z$ with $b$), it's not clear that this protocol works.
Still, maybe the prover is able to identify the variable that previously was $z$ from the structure of the formula, and repeat the faulty behaviour described above.

So although in the suggested protocol the prover cannot reply with a set that doesn't satisfy the formula, the prover can give a non-minimal set, and the verifier will (wrongly) accept it.