I know that SAT can be reduced to (3 vertex) Graph colouring, and there is a [Zero-knowlegde protocol (ZKP)](https://en.wikipedia.org/wiki/Zero-knowledge_proof) 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?