Definition of Circuit Satisfiability In The Context of zk-SNARKs

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?

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.