Prove $\text{CorrectSuccintSolver} \in \mathbf{coNP}$

Question

Define the following languages:

$$ \text{SUCC-CVAL}=\{(S,x,i) : \substack{S \text{ is a succint representation for circuit } C \\ \text{ and } C_i(x)=1 \text{ where } C_i \text{ is the i'th gate in } C(x) } \} $$ $$ \text{CorrectSuccintSolver} = \{C \, | \, \forall S,x,i\,C(S,x,i)=1\Leftrightarrow (S,x,i)\in \text{SUCC-CVAL} \} $$

I need to prove that $\text{CorrectSuccintSolver} \in \mathbf{coNP}$.

I have tried to far constructing a $\forall$ sentence with a polynomial-time TM $M$ that validates the correctness of the given input circuit $C$, such that $C\in\text{CorrectSuccintSolver} \textbf{ iff } \, \forall S,x,i\ M(C,S,x,i)$.

We need to check if the circuit $C$ is correct. The machine $M$ uses the given input circuit $C$ to check whether $C$'s output on gate $i$ is consistent with $C$'s outputs for gates $j,k$ that are connected to gate $i$ (w.l.o.g., $i = j \text{ op } k$ where $\text{op}\in{\{\wedge,\vee,\neg}\}$).

I think that there is a problem in my solution (something is missing). In addition, I have few missing details. For example, how to find gates $i,j,k$ only from succint representation?

Please advise. Thank you.

Answer 1

Thanks to @ArturRiazanov for the help.

The following $\Pi_1=\mathbf{coNP}$ sentence solves the problem: $$ C\in\text{CorrectSuccintSolver} \quad\textbf{ iff } \quad \forall S,x,i,j,k\ [M(C,S,x,i,j,k)=1] $$

The TM $M(C,S,x,i,j,k)$: Using the input circuit $C$, checks the following:

• If $i$ is an input gates, checks that the input is consistent with $x$.
• If $i$ is a logical gate, check whether $C$'s output on gate $i$ is consistent with $C$'s outputs for gates $j,k$ that are connected to gate $i$ (w.l.o.g., $i = j \text{ op } k$ where $\text{op}\in{\{\wedge,\vee,\neg}\}$).

Assuming that the succint circuit $S$ on input $i,j,k\in\{0,1\}^{\log n}$, $\text{op}\in{\{\wedge,\vee,\neg}\}$ returns 1 iff $j,k$ are connected to $i$ and $i$ computes operation $\text{op}$.

If $C$ is consistent with all of the above, $C$ is correct succint solver as required.