3
$\begingroup$

A standard theorem is that boolean circuit satisfiability is NP-complete (shown in CLRS, for example).

I am interested in what these statements formally mean. From CLRS, I can cite that

$$\text{CIRCUIT-SAT} = \{C \mid \text{$C$ is a satisfiable boolean combinational circuit}\}$$

In Bitansky et al., boolean circuit satisfiability is used to capture the statement to be proved. However, this is not CIRCUIT-SAT: Bitansky et al. consider the satisfiability of a circuit $C$ for an input $x$. CIRCUIT-SAT merely describes the satisfiability of a circuit $C$ for any input $x$.

A zk-SNARK proves statements $x \in L$ for $L \in NP$. What is done to create a zk-SNARK for boolean circuit satisfiability is to reduce $L$ to a boolean circuit $C$ such that $C$ is satisfiable for an input $x$ iff $x \in L$. $C$ models $L$, so to speak.

I am confused by people saying that boolean (or arithmetic) circuit satisfiability is NP-complete. As I understand it, $L$ needs to be modeled by a circuit $C$. However, if I went by the definition of CIRCUIT-SAT, $x$ would need to be converted to a circuit $C$. What CIRCUIT-SAT for zk-SNARKs should look like is

$$\text{CIRCUIT-SAT} = \{ (C, x) \mid \text{$C$ is a satisfiable boolean combinational circuit for input $x$}\}$$

We want a circuit per language, not per input.

So, when someone says that satisfiability of circuits, R1CS, QSPs, or QAPs is NP-complete in the context of zk-SNARKs, are they in fact referring to my definition of CIRCUIT-SAT and similar ones?

$\endgroup$
1
$\begingroup$

Suppose $L$ is an NP language, and its witness checking algorithm is $R$, so that $L = \{ x \mid \exists w : R(x,w) = 1 \}$.

Here is how I can prove to you that $x \in L$:

  • Generate a circuit $C$ such that $C(w) = R(x,w)$. We can both do this because $R$ is a public algorithm and $x$ is also public. This circuit $C$ has the instance $x$ "hard-coded" into it, so that its only formal input is $w$.

  • Convince you that the circuit $C$ is satisfiable -- i.e., there is an input $w$ that causes $C$ to output 1.

In other words, I just have to convince you that some $C$ is in CIRCUIT-SAT.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.