# 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:

1. Prover and Verifier share the input formula

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

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

-

Then, this protocol still have some problems. Let 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 say it is $y,z$? the verifier will check it, will see this set satisfies the formula, remove, say $y$ and send 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 this protocol works. Still, maybe the prover is able to identify the variable that previously was $z$ from the structure of the formula, and on the second level it will return the output $z$.