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

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?

• I think you need to fix a precise definition of succinct representation of $C$ as $S$. Then you will be able to easily extract the input gates $j$ and $k$ from it. For example if $S$ is a circuit that accepts four inputs $i,j,k \in \{0,1\}^{\log n}$, ${\rm op} \in \{0,1\}^2$ and returns 1 iff $j$ and $k$ are connected to $i$ and $i$ computes operation $\rm{op}$. Nov 27, 2021 at 11:57
• @ArturRiazanov Thank you, that helped! Then I can say $\forall i,j,k$ and now it makes sense. Nov 27, 2021 at 12:01

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.