Questionnaire-2024/equivalence_checking/practical_questions/4_5_tseitin_self.tex

\item \self Compute the propositional formula of the following circuit and transform it into an equisatisfiable formula in CNF by applying Tseitin's encoding.
For each variable you introduce, clearly indicate which subformula of $\phi$ it represents.

\tikzstyle{branch}=[fill,shape=circle,minimum size=3pt,inner sep=0pt]
\begin{tikzpicture}[label distance=2mm]
    \node (a) at (0,0) {$a$};
    \node (b) at (0,-1) {$b$};
    \node (c) at (0,-2) {$c$};
    \node (d) at (0,-3) {$d$};
    \node (z) at (12,-1.5) {$z$};

    \node (am1) at (5,0) {};
    \node (am2) at (3,0) {};
    \node (ab_c1) at (3,-.9) {};
    \node (ab_c2) at (3.1,-1) {};
    \node (ab_c3) at (3,-1.1) {};
    \node (not1m) at (5,-1) {};
    \node (not2m) at (2,-2) {};
    \node (or2m) at (5,-2) {};
    \node (dm) at (5,-3) {};    
    \node (or1m) at (7,-.5) {};
    \node (or3m) at (7,-2.5) {};
    
    \node[not gate US, draw, logic gate inputs=n] at ($(1,-1)$) (not1) {\tiny NOT};
    \node[not gate US, draw, logic gate inputs=n] at ($(1,-2)$) (not2) {\tiny NOT};
    \node[or gate US, draw, logic gate inputs=nn] at ($(6,-.5)$) (or1) {\tiny OR};
    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-2)$) (or2) {\tiny OR};
    \node[or gate US, draw, logic gate inputs=nn] at ($(6,-2.5)$) (or3) {\tiny OR};
    \node[and gate US, draw, logic gate inputs=nn] at ($(8,-1.5)$) (and1) {\tiny AND};
    \node[not gate US, draw, logic gate inputs=n] at ($(10,-1.5)$) (not3) {\tiny NOT};

    \draw (b.east) -- (not1.input);
    \draw (c.east) -- (not2.input);
    \draw (a.east) |- (am1.center) |- (or1.input 1);
    \draw (not1.output) |- (not1m.center) node[below] {$u$} |- (or1.input 2);
    \draw (a.east) |- (am2.center) node[circle, fill,inner sep=2pt] {} -- (ab_c1.center) -- (ab_c2.center) -- (ab_c3.center) |- (or2.input 1);
    \draw (not2.output) |- (not2m.center) node[below] {$t$} |- (or2.input 2);
    \draw (or2.output) |- (or2m.center) node[above] {$v$} |- (or3.input 1);
    \draw (d.east) |- (dm.center) |- (or3.input 2);
    \draw (or1.output) |- (or1m.center) node[above] {$w$} |- (and1.input 1);
    \draw (or3.output) |- (or3m.center) node[below] {$x$} |- (and1.input 2);
    \draw (and1.output) -- node[below] {$y$} (not3.input);
    \draw (not3.output) -- (z.west);

\end{tikzpicture}