Is there a Zero-Knowledge proof for SAT?

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?

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.

StackExchange Computer Science Q#135457, answer score: 2