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.
Circuit SAT
toCNF SAT
. The idea is to introduce one switching variable per gate. If all gates are restricted to two inputs, the transformation creates3-SAT CNF
clauses with three or fewer literals. $\endgroup$ – Axel Kemper Jun 1 '15 at 18:17