# Reduction from Circuit-Sat to 3-Sat

I'm reading the following notes on reduction from circuit-sat to 3-sat http://www.cs.cmu.edu/~avrim/451f11/lectures/lect1108.pdf

On the third page i'm unsure how they arrived at the following

In particular we just replace each statement of the form

$y_{3}=\mathrm{NAND}(y_{1},y_{2})$ as

$(y_{1} \cup y_{2} \cup y_{3})\cap(y_{1} \cup y_{2}' \cup y_{3})\cap(y_{1}' \cup y_{2} \cup y_{3}) \cap (y_{1}' \cap y_{2}' \cap y_{3}')$

I'm quite new to propositional logic, i've read a little bit about how to convert things to CNF so i thougt we should have $y_{3}=(y_{1}' \cup y_{2}')$. I'd appreciate any help on the reasoning behind how they replace the statement.

• Note that you're not just converting $\text{NAND}(y_1,y_2)$ to CNF, which is indeed $y_1' \cup y_2'$, but the whole statement $y_3 \iff \text{NAND}(y_1, y_2)$. – Magdiragdag May 30 '15 at 21:05
• The Tseitin Transformation is commonly used to transform Circuit SAT to CNF SAT. The idea is to introduce one switching variable per gate. If all gates are restricted to two inputs, the transformation creates 3-SAT CNF clauses with three or fewer literals. – Axel Kemper Jun 1 '15 at 18:17

One way to go about it is to just write down the truth table for both expressions and verify that they are equal (noting that in the first NAND expression, $y_3$ must be equal to the value of NAND$(y_1,y_2)$ or else the statement is false). There are only 8 possible ways to assign 3 variables, you just need to verify in each case that the values of the two Boolean expressions are equal.
• Ok so essentially we are only allowing the statement to equal 1 when $y_{3}=\mathrm{NAND}(y_{1},y_{2})$ is satisfied. So my next question is how exactly is this connected to the overall output equalling 1? – Pavan Sangha May 30 '15 at 21:57