In the proof in wikipedia, it goes like this:

Let $L \in \Pi_{2}$, so we can describe membership in $L$ as a formula:

$\forall_{y}\exists_{z} V(x,y,z)=1 \iff x \in L$

(where V is polynomial deterministic verifier etc...)
Now they look at the subformula : $s(y)=\exists_{z} V(x,y,z)$ and say that because it's an instance of $SAT$, and according to the hypothesis that $NP \subseteq P/poly$, its equivalent to $C(s(y))$, where $C$ is a valid circuit for solving $SAT$.

These are my questions:

  1. What does $s(y)$ mean? Like what's the meaning of saying that something equals some predicate? It look like merely a technical part of the proof but I can't wrap my head around it.

  2. What's the meaning of exchanging a logical predicate with circuit evaluation mean? Does it mean that we can decide if for every $y$ there exists $z$ such that $V(x,y,z)=1$ with a circuit?

  • $\begingroup$ The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$
    – Raphael
    Jun 21, 2016 at 8:54
  • $\begingroup$ karp-lipton thm / wikipedia $\endgroup$
    – vzn
    Jul 21, 2016 at 17:21

1 Answer 1


The subformula $s(y) = \exists z V(x,y,z)$ is a Boolean function which depends on $x$ and $y$. In this context we can assume that $x$ is fixed, so we only show the dependence on $s(y)$. Here $\exists z V(x,y,z)$ is the definition of the function: the value of $s$ on an input $y$ equals the truth value of the formula $\exists z V(x,y,z)$ (recall we're assuming that $x$ is fixed).

Since $V$ runs in polynomial time, as in Cook's theorem we can encode $V(x,y,z)$ is a polynomial size formula in the variables $x,y,z$. Given the fixed input $x$ and an input $y$, we can substitute $x$ and $y$ in the formula for $V(x,y,z)$ to get a formula $\varphi_{x,y}$ depending only on $z$. We can also convert this formula to CNF. The new formula is satisfiable, i.e. $s(y)$ is true, iff $\varphi_{x,y} \in SAT$.

If we have a circuit $C$ solving SAT we can use it to check whether $\varphi_{x,y}$ is satisfiable. That's what Wikipedia means when it writes $C(s(y))$: write $s(y)$ as an instance $\varphi_{x,y}$ of SAT, and then run $C$ on the instance to get the truth value of $s(y)$. Since $C$ solves SAT, $C(s(y)) = s(y)$, that is, on input $\varphi_{x,y}$ the circuit $C$ will output the truth value of $s(y)$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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