Sketch an IP proof for minSAT

I have to sketch an IP proof for the minSAT problem. The minSAT problem is define in this way:

• For a given formulae find a satisfying assignment with a min subset of variables assigned to True;

My sketched IP protocol is:

-
Prover and Verifier share the input formula

-
Prover sends to the Verifier a set of variables assigned to True, which should be the minimum

-
Verifier checks if the given set indeed satisfies the formula. If it is the case, it chooses one variable, re-computes the formula and sends the new formula to the Prover

I would iterate this process untill the Prover gives an empty set or I reach a contradiction.

My questions are:

-
Is this a right protocol? If not, how can I exploit the cases in which the protocol doesn't work?

-
How can I evaluate the probability of completness and soundness for this protocol?

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.

StackExchange Computer Science Q#6788, answer score: 4