Is there a Zero-Knowledge proof for SAT?

Question

I know that SAT can be reduced to (3 vertex) Graph colouring, and there is a Zero-knowlegde protocol (ZKP) for graph colouring. However, I am interested in a ZKP that can be performed directly on a SAT instance, without graph colouring.

Is there a known ZKP for SAT, and if not how would you suggest coming up with one?

Answer 1

As usual with zero-knowledge proofs, this is an interactive proof. A prover is trying to prove that he has a satisfying assignment to some 3-SAT formula without giving away the assignment. A verifier is trying to build up enough statistical evidence to believe the prover. The proof proceeds as a series of rounds and continues until the verifier is convinced the prover has the assignment or convinced that he doesn't. 3-SAT is used so that clauses have uniform length, which along with other measures prevent the verifier from being able to identify any particular clause between the rounds. Since general SAT formulas can be easily converted into 3-SAT formulas, this works as a zero-knowledge proof for SAT as well.

For each round the prover should:

• Permute the variable labels randomly.
• Permute the clause order in the formula randomly.
• Permute the variable order in each clause randomly.
• Invert the parity of each variable's literals randomly with probability one-half.
• Commit to this new formula, but in a way that is hidden from the verifier.
• Commit to a satisfying assignment of this new formula, but in a way that is hidden from the verifier.

After this is done, the verifier can ask the prover for either:

1. The new formula and the permutation mappings so that he can verify that the new formula is the same as the original formula, or
2. One clause of the new formula and the variable assignments for the variables in that clause, taken from the satisfying assignment previously committed to.

If the verifier asks for (1), he can verify that the new formula is the same as the original formula by reversing the permutations and literal inversions. If the prover is cheating by altering the formula to something he can satisfy, this check should eventually catch him.

If the verifier asks for (2), he can check whether part of the committed satisfying assignment will satisfy a randomly selected clause. If the prover is cheating by not satisfying all the clauses, running enough rounds will eventually catch him leaving some clause unsatisfied. The permutations and inversions prevent the verifier from gathering meaningful information about variable assignments from these checks.

Answer 2

Here is a zero-knowledge protocol for E3SAT, the variant of SAT in which each clause contains exactly three literals.

Consider an instance of E3SAT, consisting of variables $x_1,\ldots,x_n$ and clauses $C_1,\ldots,C_m$.

Prover chooses a color in $\{1,2,3,4\}$ for each of the following:

• Variable literals $V(x_i), V(\lnot x_i)$ ($2n$ colors in total).
• Literals appearing in clauses ($3m$ colors in total): for each clause $C_j$ and literal $\ell$ appearing in it, $C_j(\ell)$.
• Three additional values $a,b,c$.

Verifier makes one of the following checks:

• The colors assigned to $a,b,c$ are all different.
• For a variable $x_i$, the colors assigned to $V(x_i),V(\lnot x_i),b,c$ are all different.
• For a clause $C_j$ consisting of literals $\ell_1,\ell_2,\ell_3$, the colors assigned to $C_j(\ell_1),C_j(\ell_2),C_j(\ell_3),a$ are all different.
• For a clause $C_j$ and a literal $\ell$ appearing in it, the colors assigned to $V(\ell),C_j(\ell)$ are different.

If the formula is satisfiable, the prover acts as follows:

• It chooses random colors for $a,b,c$. We call these colors $a,b,c$, and the remaining color $d$.
• If $x_i$ is assigned true then we color $V(x_i)$ by $a$ and $V(\lnot x_i)$ by $d$, otherwise we color $V(x_i)$ by $d$ and $V(\lnot x_i)$ by $a$.
• For a clause $C_j$, choose a satisfied literal $\ell$, assign $C_j(\ell)$ the color $d$, and assign the other two $C_j(\ell'),C_j(\ell'')$ associated with the clause the colors $b,c$.

It is not hard to check that this satisfies all constraints checked by the verifier. Moreover, since we chose $a,b,c,d$ at random, verifier can simulate the answers on her own, and so this is a zero knowledge protocol.

Finally, suppose that all potential checks of the verifier pass. Let $a,b,c$ be the colors assigned to $a,b,c$, and let $d$ be the remaining color. For each variable $x_i$, the variable literals $V(x_i),V(\lnot x_i)$ are assigned the colors $a,d$. We extract a truth assignment as follows: if $V(x_i)$ is colored $a$ then we let $x_i$ be true, otherwise it is false. Each clause $C_j$ is colored using $b,c,d$, and so some clause literal $C_j(\ell)$ is colored $d$. The corresponding variable literal $V(\ell)$ must be colored $a$, and so it satisfies the clause.