Is there a Zero-Knowledge proof for SAT?
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.