added eqchecking chapter

compile

@@ -104,7 +104,7 @@ compile_wrapper() {
 
 compile_chapter() {
   #for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal
-  for chapter in  bdd
+  for chapter in  smtzthree eqchecking
   do
     set_chapter "\\chapter${chapter}true"
     compile_wrapper "$chapter" "$@"

equivalence_checking/0000.tex

@@ -0,0 +1 @@
+\item Explain the algorithm used to decide the equivalence of combinational circuits via the reduction to satisfiability.

equivalence_checking/0000_sol.tex

@@ -0,0 +1,9 @@
+Let $C_1$ and $C_2$ denote the two combinational circuits.
+In order to check whether $C_1$ and $C_2$ are equivalent, one has to perform the following steps:
+\begin{enumerate}
+    \item Encode $C_1$ and $C_2$ into two propositional formulas $\varphi_1$ and $\varphi_2$.
+    \item Compute the Conjunctive Normal Form (CNF) of $\varphi_1 \oplus \varphi_2$,
+    using Tseitin encoding; i.e., $CNF(\varphi_1 \oplus \varphi_2)$. 
+    \item Give the formula  $CNF(\varphi_1 \oplus \varphi_2)$ to a SAT solver and check for satisfiability.
+    \item $C_1$ and $C_2$ are equivalent if and only if $CNF(\varphi_1 \oplus \varphi_2)$ is UNSAT.
+\end{enumerate}

equivalence_checking/0001.tex

@@ -0,0 +1,2 @@
+\item \lect Explain the process of translating a combinational circuit into a propositional formula. 
+Draw a combinational circuit with 2 or 3 gates and give the corresponding propositional formula.

equivalence_checking/0001_sol.tex

@@ -0,0 +1,33 @@
+\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 (z) at (6,-1) {$z$};
+
+    \node (am) at (1,0) {};
+    \node (bm) at (1,-1) {};
+
+    \node[and gate US, draw, logic gate inputs=nn] at ($(2,-.5)$) (and1) {\tiny AND};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-1)$) (or1) {\tiny OR};
+
+    \node (and1m) at (3,-.5) {};
+    \node (c1m) at (3,-2) {};
+
+    \draw (a.east) -| (am.center) |- (and1.input 1);
+    \draw (b.east) |- (bm.center) |- (and1.input 2);
+    \draw (and1.output) |-  (and1m.center) node[above] {$y$} |- (or1.input 1);
+    \draw (c.east) |- (c1m.center) |- (or1.input 2);
+    \draw (or1.output) -- (z);
+\end{tikzpicture}
+
+The inputs are denoted by $a$, $b$, and $c$ and the output is denoted by $z$.
+We assign temporary variable names to the inner wires; in this case we use $y$.
+Using these variables, we can create the propositional formula over the inputs and the output.
+%
+\begin{equation*} 
+\begin{split}
+z & = y \lor c \\
+ & = (a \land b) \lor c
+\end{split}
+\end{equation*}

equivalence_checking/0002.tex

@@ -0,0 +1,29 @@
+\item
+\CNFfromCircuit
+
+\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 (z) at (8,-1) {$z$};
+
+    \node (am) at (1,0) {};
+    \node (bm) at (1,-1) {};
+
+    \node[or gate US, draw, logic gate inputs=nn] at ($(2,-.5)$) (or1) {\tiny OR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2)$) (not1) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(4,-1)$) (and1) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(6,-1)$) (not2) {\tiny NOT};
+
+    \node (or1m) at (3,-.5) {};
+    \node (not1m) at (3,-2) {};
+
+    \draw (a.east) -| (am.center) |- (or1.input 1);
+    \draw (b.east) |- (bm.center) |- (or1.input 2);
+    \draw (or1.output) |-  (or1m.center) node[above] {$w$} |- (and1.input 1);
+    \draw (c.east) |- (not1.input);
+    \draw (not1.output) |- (not1m.center) node[below] {$x$} |- (and1.input 2);
+    \draw (and1.output) -- node[below] {$y$} (not2.input);
+    \draw (not2.output) -- (z);
+\end{tikzpicture}

equivalence_checking/0002_sol.tex

@@ -0,0 +1,8 @@
+\begin{equation*}
+\begin{split}
+z & = \neg y \\
+ & = \neg (w \land x) \\
+ & = \neg ((a \lor b) \land x) \\
+  & = \neg ((a \lor b) \land \neg c) \\
+\end{split}
+\end{equation*}

equivalence_checking/0003.tex

@@ -0,0 +1 @@
+\item Explain the duality of \textit{satisfiability} and \textit{validity}.

equivalence_checking/0003_sol.tex

@@ -0,0 +1,16 @@
+\emph{A formula $\varphi$ is valid, if and only if, $\neg \varphi$ is not satisfiable}.
+
+Consider the formula $\varphi=(x \lor \neg x)$. This formula is valid, i.e., all rows in the truth table
+would evaluate to \emph{true}. The negation of $\varphi$ is the following:
+$\neg \varphi = \neg (x \lor \neg x) = \neg x \land x$, which is not satisfiable, i.e., all rows the truth table would evaluate to \emph{false}.
+
+\noindent\emph{A formula $\varphi$ is satisfiable, if and only if, $\neg \varphi$ is not valid}.
+
+If $\varphi$ is satisfiable, there is at least one model that makes the formula true. If we negate the formula,
+these models make the negated formula false, and therefore, the negated formula cannot be valid.
+Consider the formula $\varphi=(x \lor y)$.
+There is at least one model that makes the formula true, e.g. $\mathcal{M} \coloneqq x = T, \ y = T$.
+The negation of $\varphi$ is the following:
+$\neg \varphi = \neg (x \lor y) = \neg x \land \neg y$.
+Under the same model $\mathcal{M}$ as before, $\neg \varphi$ evaluates to false.
+So the negated formula is not valid.

equivalence_checking/0004.tex

@@ -0,0 +1 @@
+\item \lect How can you check whether it is true that $\phi \models \psi$ using a decision procedure for (a) \textit{satisfiability} or (b) \textit{validity}? 

equivalence_checking/0004_sol.tex

@@ -0,0 +1,7 @@
+\begin{enumerate}
+\item \textbf{Decide entailment using satisfiability.}
+The question whether $\varphi \vDash  \psi$ can be decided by checking $\varphi \wedge \neg \psi$ not satisfiable.
+
+\item \textbf{Decide entailment using validity.}
+The question whether $\varphi \vDash \psi$ can be decided by checking $\varphi \rightarrow \psi$ is valid.
+\end{enumerate}

equivalence_checking/0005.tex

@@ -0,0 +1 @@
+\item \lect What is the advantage of applying \textit{Tseitin transformation} to obtain an equisatisfiable CNF, especially compared to using truth tables?

equivalence_checking/0005_sol.tex

@@ -0,0 +1,3 @@
+Given an original formula $\varphi$.
+The equisatisfiable formula in CNF after Tseitin encoding -- $CNF(\varphi)$ -- is \emph{linear} in the size of $\varphi$, since the number of variables and clauses introduced by Tseitin encoding is \emph{linear} in the size of $\varphi$.
+Using a truth table could result in an exponential blowup when constructing a CNF.

equivalence_checking/0006.tex

@@ -0,0 +1 @@
+\item \lect Derive a Rewrite-Rule for an implication node, i.e., what clauses are introduced by the node $x \leftrightarrow (p \rightarrow q)$?

equivalence_checking/0006_sol.tex

@@ -0,0 +1,12 @@
+\begin{equation*} 
+\begin{split}
+x \leftrightarrow (p \rightarrow q) &\Leftrightarrow x \leftrightarrow (p \rightarrow q)\\
+&\Leftrightarrow (x \rightarrow (p \rightarrow q)) \land ((p \rightarrow q) \rightarrow x)\\
+&\Leftrightarrow (x \rightarrow (\lnot p \lor q)) \land ((\lnot p \lor q) \rightarrow x)\\
+&\Leftrightarrow (\lnot x \lor (\lnot p \lor q)) \land (\lnot (\lnot p \lor q) \lor x)\\
+&\Leftrightarrow (\lnot x \lor \lnot p \lor q) \land ((\lnot\lnot p \land \lnot q) \lor x)\\
+&\Leftrightarrow (\lnot x \lor \lnot p \lor q) \land ((p \land \lnot q) \lor x)\\
+&\Leftrightarrow (\lnot x \lor \lnot p \lor q) \land ((p \lor x) \land (\lnot q \lor x))\\
+&\Leftrightarrow (\lnot x \lor \lnot p \lor q) \land (p \lor x) \land (\lnot q \lor x)\\
+\end{split}
+\end{equation*}

equivalence_checking/0007.tex

@@ -0,0 +1 @@
+\item Give the definition of equisatisfiability.

equivalence_checking/0007_sol.tex

@@ -0,0 +1,4 @@
+Two propositional formulas $\varphi$ and $\psi$ are \emph{equisatisfiable} if and only if
+either \emph{both are satisfiable} or \emph{both are unsatisfiable}.
+
+When checking whether two formulas $\varphi_1$ and $\varphi_2$ are equivalent we check whether $\varphi = \varphi_1 \oplus \varphi_2$ is satisfiable. If $\varphi$ is \textit{SAT} we know that there is a model such that one of the input formulas evaluated to true, while the other evaluated to false. The equisatisfiable formula $CNF(\varphi)$ is satisfiable if and only if $\varphi$ is satisfiable and therefore answers our question of whether the two input formulas are equivalent.

equivalence_checking/0008.tex

@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = \lnot (a \lor \lnot b) \lor (\lnot a \land c)$}

equivalence_checking/0008_sol.tex

@@ -0,0 +1,27 @@
+$$
+  \underbracket{
+    \underbracket{
+      \lnot
+      \underbracket{
+        (a \lor \underbracket{\lnot b}_{x_4})
+      }_{x_3}
+    }_{x_1}
+    \lor
+    \underbracket{
+      (\underbracket{\lnot a}_{x_5} \land c)
+    }_{x_2}
+  }_{x_\varphi}
+$$
+
+
+
+
+\begin{align*}
+\varphi' = \ &x_\phi \land \\
+              &\tseitinAnd{x_\varphi}{x_1}{x_2} \land \\
+              &\tseitinNot{x_1}{x_3} \land \\
+              &\tseitinOr{x_3}{a}{x_4} \land \\
+              &\tseitinAnd{x_2}{x_5}{c} \land \\
+              &\tseitinNot{x_4}{b} \land \\
+              &\tseitinNot{x_5}{a}
+\end{align*}

equivalence_checking/0009.tex

@@ -0,0 +1,3 @@
+\item \lect Check whether $\phi_1 = a \land \lnot b$ and $\phi_2 = \lnot ( \lnot a \lor b)$ are semantically equivalent using the reduction to satisfiability.
+Follow the algorithm discussed in the lecture and state the final formula that is used as input for a SAT solver.
+

equivalence_checking/0009_sol.tex

@@ -0,0 +1,62 @@
+\begin{itemize}
+  \item We start by construction $\varphi$: \\
+    \begin{align*}
+      \varphi &= \varphi_1 \oplus \varphi_2 \\
+              &= [\varphi_1 \lor \varphi_2] \land \lnot [\varphi_1 \land \varphi_2] = \\
+              &= [(a \land \lnot b) \lor (\lnot(\lnot a \lor b))] \land \lnot [(a \land \lnot b) \land (\lnot(\lnot a \lor b))]
+    \end{align*}
+\end{itemize}
+
+$$
+  \underbracket{
+    \underbracket{\Big[
+      \underbracket{\big(
+        a
+        \land
+        \underbracket{\lnot b}_{x_{7}}
+      \big)}_{x_3}
+      \lor
+      \underbracket{\big(
+        \lnot
+          \underbracket{(
+            \underbracket{\lnot a}_{x_{8}}
+            \lor
+            b
+          )}_{x_6}
+      \big)}_{x_4}
+    \Big]}_{x_1}
+    \land
+    \underbracket{
+      \lnot
+      \underbracket{\Big[
+        \underbracket{\big(
+          a
+          \land
+          \underbracket{\lnot b}_{x_{7}}
+        \big)}_{x_3}
+        \lor
+        \underbracket{\big(
+          \lnot
+            \underbracket{(
+              \underbracket{\lnot a}_{x_{8}}
+              \lor
+              b
+            )}_{x_6}
+        \big)}_{x_4}
+      \Big]}_{x_1}
+    }_{x_2}
+  }_{x_\varphi}
+    $$
+
+
+\begin{align*}
+  \varphi' = \ &x_\phi \land \\
+                &\tseitinAnd{x_{\varphi}}{x_1}{x_2} \land \\
+                &\tseitinNot{x_1}{x_2} \land \\
+                &\tseitinOr{x_1}{x_3}{x_4} \land \\
+                &\tseitinAnd{x_3}{a}{x_{7}} \land \\
+                &\tseitinNot{x_4}{x_6} \land \\
+                &\tseitinOr{x_6}{x_{8}}{b} \land \\
+                &\tseitinNot{x_{7}}{b} \land \\
+                &\tseitinNot{x_{8}}{a} \land
+\end{align*}

equivalence_checking/0010.tex

@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = ((p \lor q) \land r) \lor \lnot p$}

equivalence_checking/0010_sol.tex

@@ -0,0 +1,23 @@
+$$
+\underbracket{(% 1
+\underbracket{(% 3
+\underbracket{(% 21
+p	\lor
+q)
+}_{x_{1}}% END:\lor
+\land
+r)
+}_{x_{2}}% END:\land
+\lor
+\underbracket{\lnot
+p}_{x_{3}})
+}_{x_{\varphi}}% END:\lor
+$$
+
+\begin{align*}
+\varphi' = \ &x_\varphi~\land\\
+            &\tseitinOr{x_{\varphi}}{x_{2}}{x_{3}}~\land \\
+            &\tseitinAnd{x_{2}}{x_{1}}{r}~\land \\
+            &\tseitinOr{x_{1}}{p}{q}~\land \\
+            &\tseitinNot{x_{3}}{p}
+\end{align*}

equivalence_checking/1000.tex

@@ -0,0 +1,34 @@
+\item \self Compute the propositional formula of the following circuit.
+
+\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 (z) at (8,-1) {$z$};
+
+    \node (bm) at (3,-1) {};
+    \node (cm1) at (2,-2) {};
+    \node (cm2) at (3,-2) {};
+    \node (bc_c1) at (2,-1.1) {};
+    \node (bc_c2) at (2.1,-1) {};
+    \node (bc_c3) at (2,-.9) {};
+    \node (not1m) at (3,0) {};
+    \node (and1m) at (5,-.5) {};
+    \node (nand1m) at (5,-1.5) {};
+
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,0)$) (not1) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(4,-.5)$) (and1) {\tiny AND};
+    \node[nand gate US, draw, logic gate inputs=nn] at ($(4,-1.5)$) (nand1) {\tiny NAND};
+    \node[xor gate US, draw, logic gate inputs=nn] at ($(6,-1)$) (xor1) {\tiny XOR};
+
+    \draw (a.east) -- (not1.input);
+    \draw (not1.output) -| (not1m.center) node[above] {$w$} |- (and1.input 1);
+    \draw (c.east) -| (cm1.center) node[circle, fill,inner sep=2pt] {} -- (bc_c1.center) -- (bc_c2.center) -- (bc_c3.center) |- (and1.input 2);
+    \draw (b.east) -| (bm.center) |- (nand1.input 1);
+    \draw (c.east) -| (cm2.center) |- (nand1.input 2);
+    \draw (and1.output) -| (and1m.center) node[above] {$x$} |- (xor1.input 1);
+    \draw (nand1.output) -| (nand1m.center) node[below] {$y$} |- (xor1.input 2);
+    \draw (xor1.output) -- (z);
+\end{tikzpicture}
+

equivalence_checking/1001.tex

@@ -0,0 +1,47 @@
+\item
+\CNFfromCircuit
+
+\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.5) {$c$};
+    \node (d) at (0,-3.5) {$d$};
+    \node (z) at (13.5,-1.5) {$z$};
+
+    \node (am) at (2,0) {};
+    \node (not1m) at (3,-1) {};
+    \node (not2m) at (3,-2.5) {};
+    \node (dm) at (2,-3.5) {};
+    \node (bm) at (1,-1) {};
+    \node (bm2) at (7,-1.875) {};
+    \node (not3m) at (7,-2.5) {};
+    \node (or1m) at (9,-.5) {};
+    \node (and1m) at (9,-2) {};
+
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-1)$) (not1) {\tiny NOT};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2.5)$) (not2) {\tiny NOT};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-.5)$) (or1) {\tiny OR};
+    \node[xor gate US, draw, logic gate inputs=nn] at ($(4,-3)$) (xor1) {\tiny XOR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(6,-3)$) (not3) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(8,-2)$) (and1) {\tiny AND};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(10,-1.5)$) (or2) {\tiny OR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(12,-1.5)$) (not4) {\tiny NOT};
+
+    \draw (a.east) -| (am.center) |- (or1.input 1);
+    \draw (b.east) -- (not1.input);
+    \draw (not1.output) -| (not1m.center) node[below] {$r$} |- (or1.input 2);
+    \draw (c.east) -- (not2.input);
+    \draw (not2.output) -| (not2m.center) node[above] {$s$} |- (xor1.input 1);
+    \draw (d.east) -| (dm.center) |- (xor1.input 2);
+    \draw (b.east) -| (bm.center) node[circle, fill,inner sep=2pt] {} |- (bm2.center) node[above] {$u$} |- (and1.input 1);
+    \draw (xor1.output) -- node[below] {$t$} (not3.input);
+    \draw (not3.output) -| node[below] {$v$} (not3m.center) |- (and1.input 2);
+    \draw (or1.output) -| (or1m.center) node[above] {$w$} |- (or2.input 1);
+    \draw (and1.output) -| (and1m.center) node[below] {$x$} |- (or2.input 2);
+    \draw (or2.output) -- node[below] {$y$} (not4.input);
+    \draw (not4.output) -- (z);
+
+
+\end{tikzpicture}
+

equivalence_checking/1002.tex

@@ -0,0 +1,2 @@
+\item \self \textit{A formula $\phi$ is valid, if and only if $\lnot \phi$ is not satisfiable.}
+Explain why this statement holds true.

equivalence_checking/1003.tex

@@ -0,0 +1,3 @@
+\item \self 
+Given two propositional logic formulas $\varphi$ and $\psi$. How can we check whether $\phi \equiv \psi$ using a decision procedure for (a) satisfiability, (b) for validity, and (c) for semantic entailment?
+

equivalence_checking/1004.tex

@@ -0,0 +1,3 @@
+\item \self 
+ Given a propositional logic formula $\varphi$. How can we check whether
+$\varphi$ is \emph{valid} using a decision procedure for (a) satisfiability and (b) equivalence?

equivalence_checking/1005.tex

@@ -0,0 +1,8 @@
+\item \self  Given a propositional logic formula $\varphi$.
+Tick all statements that are true. 
+\begin{enumerate}
+	\item[$\square$] A formula $\phi$ is \textit{valid}, if and only if $\lnot \phi$ is \textit{satisfiable}.
+	\item[$\square$] A formula $\psi$ is \textit{satisfiable}, if and only if $\lnot \phi$ is \textit{valid}.
+	\item[$\square$] A formula $\phi$ is \textit{satisfiable}, if and only if $\lnot \phi$ is \textit{not valid}.
+	\item[$\square$] A formula $\phi$ is \textit{valid}, if and only if $\lnot \phi$ is \textit{not satisfiable}.
+\end{enumerate}

equivalence_checking/1006.tex

@@ -0,0 +1,8 @@
+\item \self Given two propositional logic formulas $\varphi$ and $\psi$.
+Tick all statements that are true. 
+\begin{enumerate}
+	\item[$\square$] If $\lnot \phi$ is not satisfiable, $\phi$ is not valid.
+	\item[$\square$] If $\top \models \phi$, $\phi$ is valid.
+	\item[$\square$] If $\phi \leftrightarrow \psi$ is valid, $\phi$ entails $\psi$.
+	\item[$\square$] If $\phi \imp \psi$ is valid, both formulas are equivalent.
+\end{enumerate}

equivalence_checking/1007.tex

@@ -0,0 +1,8 @@
+\item \self Given two propositional logic formulas $\varphi$ and $\psi$.
+Tick all statements that are true. 
+\begin{enumerate}
+	\item[$\square$] If $\phi \land \lnot \psi$ is not satisfiable, $\phi$ entails $\psi$.
+	\item[$\square$] If $\lnot \phi$ is not valid, $\phi$ is satisfiable.
+	\item[$\square$] If $\phi$ entails $\psi$ and $\psi$ entails $\phi$, both formulas are equivalent.
+	\item[$\square$] If $\phi$ is equivalent to $\top$, $\phi$ is valid..
+\end{enumerate}

equivalence_checking/1008.tex

@@ -0,0 +1 @@
+%\item \self SAT solvers in general use an \textit{exclusive or} between two formulas (i.e. $\phi \; \oplus \; \psi$) to check if the given formulas are \textit{equivalent}. Why does the formula $\chi = \phi \; \oplus \; \psi$ have to be "UNSAT" in order to prove that the two formulas $\phi$ and $\psi$ are \textit{equivalent}? What is the big advantage of using this method for checking \textit{equivalency} between two formulas?

equivalence_checking/1009.tex

@@ -0,0 +1 @@
+\item \self (a) What does it mean that two formulas $\phi$ and $\psi$ are \textit{equisatisfiable}? (b) Explain the difference between \textit{satisfiability} and \textit{equisatisfiability}.

equivalence_checking/1010.tex

@@ -0,0 +1,3 @@
+\item Given a propositional logic formula $\varphi$, the Tseitin transformation computes an
+equisatisfiable formula $\varphi'$ in CNF.
+Why is this enough for equivalence checking?

equivalence_checking/1011.tex

@@ -0,0 +1,5 @@
+\item \self Explain the algorithm of \emph{Tseitin transformation} to obtain
+    an equisatisfiable formula in CNF. Give step-by-step instructions of how to
+    apply Tseitin transformation to a propositional formula.\\
+    (Note: Focus on the concept. You do \emph{not} need to quote
+    the rewrite rules!)

equivalence_checking/1012.tex

@@ -0,0 +1 @@
+\item \self Derive a Rewrite-Rule for a NAND node, i.e., what clauses are introduced by the node $x \leftrightarrow (p \; \text{NAND} \; q)$?

equivalence_checking/1013.tex

@@ -0,0 +1 @@
+\item \self Derive a Rewrite-Rule for a NOR node, i.e., what clauses are introduced by the node $x \leftrightarrow (p \; \text{NOR} \; q)$?

equivalence_checking/1014.tex

@@ -0,0 +1 @@
+\item \self Derive a Rewrite-Rule for a XOR node, i.e., what clauses are introduced by the node $x \leftrightarrow (p \; \oplus \; q)$?

equivalence_checking/1015.tex

@@ -0,0 +1 @@
+\item\ifassignmentsheet \points{3} \fi \applyTseitin{$\phi = \lnot (\lnot b \land \lnot c) \lor (\lnot c \land a)$}

equivalence_checking/1016.tex

@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = (q \land \lnot r) \lor \lnot (q \land \lnot r)$}

equivalence_checking/1017.tex

@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = (\lnot(\lnot a \land b) \land \lnot c)$}

equivalence_checking/1018.tex

@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = (p \lor \lnot q) \lor (\lnot p \land \lnot r)$}

equivalence_checking/1019.tex

@@ -0,0 +1,45 @@
+\item
+\CNFfromCircuit
+
+\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}

equivalence_checking/1020.tex

@@ -0,0 +1,38 @@
+\item
+\CNFfromCircuit
+
+\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 (z) at (10,-1) {$z$};
+
+    \node (am) at (1,0) {};
+    \node (cm) at (1,-2) {};
+    \node (bm) at (3,-1) {};
+    \node (not1m) at (3,-2) {};
+    \node (not2m) at (5,-.5) {};
+    \node (or1m) at (5,-1.5) {};
+    \node (bc_c1) at (1,-1.1) {};
+    \node (bc_c2) at (1.1,-1) {};
+    \node (bc_c3) at (1,-.9) {};
+
+    \node[and gate US, draw, logic gate inputs=nn] at ($(2,-.5)$) (and1) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2)$) (not1) {\tiny NOT};
+    \node[not gate US, draw, logic gate inputs=n] at ($(4,-.5)$) (not2) {\tiny NOT};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-1.5)$) (or1) {\tiny OR};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(6,-1)$) (and2) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(8,-1)$) (not3) {\tiny NOT};
+
+    \draw (a.east) -| (am.center) |- (and1.input 1);
+    \draw (c.east) -| (cm.center) node[circle, fill,inner sep=2pt] {} -- (bc_c1.center) -- (bc_c2.center) -- (bc_c3.center) |- (and1.input 2);
+    \draw (b.east) -| (bm.center)|- (or1.input 1);
+    \draw (c.east) -- (not1.input);
+    \draw (and1.output) -- node[above] {$u$} (not2.input);
+    \draw (not1.output) -| (not1m.center) node[below] {$v$} |- (or1.input 2);
+    \draw (not2.output) -| (not2m.center) node[above] {$w$} |- (and2.input 1);
+    \draw (or1.output) -| (or1m.center) node[below] {$x$} |-  (and2.input 2);
+    \draw (and2.output) -- node[below] {$y$} (not3.input);
+    \draw (not3.output) -- (z.west);
+\end{tikzpicture}

equivalence_checking/1021.tex

@@ -0,0 +1,2 @@
+\item \self Check whether $\phi_1 = (a \land b) \lor \lnot c$ and $\phi_2 = (a \lor \lnot c) \land (b \lor \lnot c)$ are semantically equivalent using the reduction to satisfiability.
+Follow the algorithm discussed in the lecture and state the final formula that is used as input for a SAT solver.

equivalence_checking/1025.tex

@@ -0,0 +1,2 @@
+\item \ifassignmentsheet \points{3} \fi \applyTseitin{$\phi = \lnot (p \imp q) \land (r \land p)$}
+Derive the Tseitin transformation rule for $\imp$ or transform the input such that you can use the rules above.

equivalence_checking/equivalence_checking.tex

@@ -0,0 +1,151 @@
+
+\begin{questionSection}{Normal Forms}
+\question{sat_solvers_dpll/3001.tex}
+         {no_solution}
+         {3cm}
+\question{sat_solvers_dpll/3002.tex}
+         {no_solution}
+         {3cm}
+
+\mcquestion{sat_solvers_dpll/3019.tex}
+           {sat_solvers_dpll/3019.tex}
+\mcquestion{sat_solvers_dpll/2003.tex}
+           {sat_solvers_dpll/2003.tex}
+\mcquestion{sat_solvers_dpll/2004.tex}
+           {sat_solvers_dpll/2004.tex}
+\mcquestion{sat_solvers_dpll/3021.tex}
+           {sat_solvers_dpll/3021.tex}
+\mcquestion{sat_solvers_dpll/3022.tex}
+           {sat_solvers_dpll/3022.tex}
+\mcquestion{sat_solvers_dpll/3024.tex}
+           {sat_solvers_dpll/3024.tex}
+\mcquestion{sat_solvers_dpll/3025.tex}
+           {sat_solvers_dpll/3025.tex}
+\mcquestion{sat_solvers_dpll/3023.tex}
+           {sat_solvers_dpll/3023_sol.tex}
+
+\pagebreak
+\mcquestion{sat_solvers_dpll/3007.tex}
+           {sat_solvers_dpll/3007.tex}
+\mcquestion{sat_solvers_dpll/3014.tex}
+           {sat_solvers_dpll/3014.tex}
+\mcquestion{sat_solvers_dpll/3016.tex}
+           {sat_solvers_dpll/3016.tex}
+
+\end{questionSection}
+\begin{questionSection}{Relations between Satisfiability, Validity, Equivalence and Entailment}
+\question{equivalence_checking/0003.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/0004.tex}
+         {no_solution}
+         {3cm}
+\question{equivalence_checking/1002.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1003.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1004.tex}
+         {no_solution}
+         {3cm}
+
+\mcquestion{equivalence_checking/1005.tex}
+           {equivalence_checking/1005.tex}
+
+\mcquestion{equivalence_checking/1006.tex}
+           {equivalence_checking/1006.tex}
+
+\mcquestion{equivalence_checking/1007.tex}
+           {equivalence_checking/1007.tex}
+
+\question{equivalence_checking/1008.tex}
+         {no_solution}
+         {3cm}
+\end{questionSection}
+
+\pagebreak
+\begin{questionSection}{Combinational Equivalence Checking}
+
+\question{equivalence_checking/0000.tex}
+         {equivalence_checking/0000_sol.tex}
+         {5cm}
+\question{equivalence_checking/0007.tex}
+         {equivalence_checking/0007_sol.tex}
+         {3cm}
+\question{equivalence_checking/1010.tex}
+         {no_solution}
+         {3cm}
+\question{equivalence_checking/1009.tex}
+         {no_solution}
+         {3cm}
+
+
+\question{equivalence_checking/1011.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/0005.tex}
+         {equivalence_checking/0005_sol.tex}
+         {3cm}
+\question{equivalence_checking/0006.tex}
+         {equivalence_checking/0006_sol.tex}
+         {3cm}
+
+
+\question{equivalence_checking/0002.tex}
+         {no_solution}
+         {3cm}
+\question{equivalence_checking/1001.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1019.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1020.tex}
+         {no_solution}
+         {3cm}
+
+
+\tseitinRules
+\question{equivalence_checking/0008.tex}
+         {equivalence_checking/0008_sol.tex}
+         {3cm}
+
+\question{equivalence_checking/0010.tex}
+         {equivalence_checking/0010_sol.tex}
+         {3cm}
+
+\question{equivalence_checking/1015.tex}
+         {no_solution}
+         {3cm}
+
+
+\question{equivalence_checking/1016.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1017.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1018.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/1025.tex}
+         {no_solution}
+         {3cm}
+
+\question{equivalence_checking/0009.tex}
+         {equivalence_checking/0009_sol.tex}
+         {3cm}
+\question{equivalence_checking/1021.tex}
+         {no_solution}
+         {3cm}
+\end{questionSection}

equivalence_checking/multiple_choice/2_0_relations_self.tex

@@ -0,0 +1,8 @@
+\item \self  Given a propositional logic formula $\varphi$.
+Tick all statements that are true. 
+\begin{enumerate}
+	\item[$\square$] A formula $\phi$ is \textit{valid}, if and only if $\lnot \phi$ is \textit{satisfiable}.
+	\item[$\square$] A formula $\psi$ is \textit{satisfiable}, if and only if $\lnot \phi$ is \textit{valid}.
+	\item[$\square$] A formula $\phi$ is \textit{satisfiable}, if and only if $\lnot \phi$ is \textit{not valid}.
+	\item[$\square$] A formula $\phi$ is \textit{valid}, if and only if $\lnot \phi$ is \textit{not satisfiable}.
+\end{enumerate}

equivalence_checking/multiple_choice/2_1_relations_self.tex

@@ -0,0 +1,8 @@
+\item \self Given two propositional logic formulas $\varphi$ and $\psi$.
+Tick all statements that are true. 
+\begin{enumerate}
+	\item[$\square$] If $\lnot \phi$ is not satisfiable, $\phi$ is not valid.
+	\item[$\square$] If $\top \models \phi$, $\phi$ is valid.
+	\item[$\square$] If $\phi \leftrightarrow \psi$ is valid, $\phi$ entails $\psi$.
+	\item[$\square$] If $\phi \imp \psi$ is valid, both formulas are equivalent.
+\end{enumerate}

equivalence_checking/multiple_choice/2_2_relations_self.tex

@@ -0,0 +1,8 @@
+\item \self Given two propositional logic formulas $\varphi$ and $\psi$.
+Tick all statements that are true. 
+\begin{enumerate}
+	\item[$\square$] If $\phi \land \lnot \psi$ is not satisfiable, $\phi$ entails $\psi$.
+	\item[$\square$] If $\lnot \phi$ is not valid, $\phi$ is satisfiable.
+	\item[$\square$] If $\phi$ entails $\psi$ and $\psi$ entails $\phi$, both formulas are equivalent.
+	\item[$\square$] If $\phi$ is equivalent to $\top$, $\phi$ is valid..
+\end{enumerate}

equivalence_checking/multiple_choice/3_0_normal_forms_self.tex

@@ -0,0 +1,7 @@
+\item \self Tick all statements that are true.
+\begin{itemize}
+	\item[$\square$] A \textit{clause} is a disjunction of literals.
+	\item[$\square$] A \textit{clause} is a conjunction of literals.
+	\item[$\square$] A \textit{cube} is disjunction of literals.
+	\item[$\square$] A \textit{cube} is a conjunction of literals.
+\end{itemize}

equivalence_checking/multiple_choice/3_1_normal_forms_self.tex

@@ -0,0 +1,8 @@
+\item \self Given the formula $\phi$ with the variables $x_1, ..., x_n$. Tick all statements that are true. 
+\begin{itemize}
+	\item[$\square$] A \textit{literal} is a variables $x_i$ or its negation.
+	\item[$\square$] A \textit{literal} forms a formula in conjunctive normal form.
+	\item[$\square$] A \textit{literal} forms a formula in disjunctive normal form.	
+	\item[$\square$] A \textit{literal} is called \textit{positive}, if it is the negation of a variable.
+	\item[$\square$] A \textit{literal} is called \textit{negative}, if it is the negation of a variable.
+\end{itemize}

equivalence_checking/multiple_choice/3_2_normal_forms_self.tex

@@ -0,0 +1,15 @@
+\item \self Look a the following statements and tick all formulas that conform to a \textit{DNF} and all sentences, that describe a \textit{DNF} correctly.
+\begin{itemize}
+	\item[$\square$] $a \lor b$
+	\item[$\square$] A DNF is a conjunction of clauses.	
+	\item[$\square$] $(a \lor b) \land (\lnot b \lor \lnot a \lor c) \land \lnot c$
+	\item[$\square$] $(a \land b) \lor (\lnot b \land \lnot a \land c) \lor \lnot c$
+	\item[$\square$] A DNF is a conjunction of disjunctions of literals.
+	\item[$\square$] $b$
+	\item[$\square$] $a \land b \land \lnot c$
+	\item[$\square$] $(\lnot a \land b) \land (\lnot a \land c)$
+	\item[$\square$] A DNF is a disjunction of cubes.
+	\item[$\square$] $\lnot (a \land \lnot b) \land c$
+	\item[$\square$] A DNF is a disjunction of conjunctions of literals.
+	\item[$\square$] $a \land \lnot b$
+\end{itemize}

equivalence_checking/multiple_choice/3_3_normal_forms_self.tex

@@ -0,0 +1,11 @@
+\item \self Tick each correct ending of the following sentence. "A
+    \emph{Conjunctive Normal Form} is \dots
+    \begin{itemize}
+        \item[$\square$] \dots a conjunction of disjunctions
+            of literals."
+        \item[$\square$] \dots a conjunction of clauses."
+        \item[$\square$] \dots a formula that consists only
+            of logical AND operations on sub-formulas which
+            only consist of OR operations on just variables
+            and negations of variables."
+    \end{itemize}

equivalence_checking/multiple_choice/3_4_normal_forms_self.tex

@@ -0,0 +1,11 @@
+\item \self SAT solvers usually require input formulas to be in
+    \emph{Conjunctive Normal Form} (CNF). In the following list, tick
+    all items that conform to CNF.
+
+\begin{itemize}
+  \item[$\square$] A formula $\phi$ that consists of a conjunction of clauses $c_1, c_2, \ldots, c_n$.
+  \item[$\square$] A formula $\phi$ that consists of a disjunction of clauses $c_1, c_2, \ldots, c_n$.
+  \item[$\square$] A formula $\phi$ that consists of a conjunction of cubes $c_1, c_2, \ldots, c_n$.
+  \item[$\square$] A formula $\phi$ that consists of a disjunction of cubes $c_1, c_2, \ldots, c_n$.
+  \item[$\square$] A literal $l$.
+\end{itemize}

equivalence_checking/multiple_choice/3_5_normal_forms_self.tex

@@ -0,0 +1,17 @@
+\item \self In the following list, tick
+    all items that conform to the Conjunctive Normal Form (CNF).
+
+\begin{itemize}
+  \item[$\square$] $(a \wedge b \wedge \neg c) \vee (\neg b
+      \wedge \neg c) \vee (e \wedge \neg f)$
+  \item[$\square$] $a$
+  \item[$\square$] $\neg b$
+  \item[$\square$] $a \wedge \neg b$
+  \item[$\square$] $a \vee \neg b$
+  \item[$\square$] $a \vee (\neg b \wedge c)$
+  \item[$\square$] $(a \vee \neg b) \wedge c$
+  \item[$\square$] $\neg(p \vee q)$
+  \item[$\square$] $x \vee \neg y \vee z$
+\end{itemize}
+
+

equivalence_checking/multiple_choice/3_6_normal_forms_self.tex

@@ -0,0 +1,16 @@
+\item \self In the following list, tick
+    all items that conform to the Disjunctive Normal Form (DNF).
+
+\begin{itemize}
+  \item[$\square$] $(a \wedge b \wedge \neg c) \vee (\neg b
+      \wedge \neg c) \vee (e \wedge \neg f)$
+  \item[$\square$] $(a \vee b \vee \neg c) \wedge (\neg b
+      \vee \neg c) \wedge (e \vee \neg f)$    
+  \item[$\square$] $\neg b$
+  \item[$\square$] $a \wedge \neg b$
+  \item[$\square$] $a \vee \neg b$
+  \item[$\square$] $a \vee (\neg b \wedge c)$
+  \item[$\square$] $(a \vee \neg b) \wedge c$
+  \item[$\square$] $\neg(p \vee q)$
+  \item[$\square$] $x \vee \neg y \vee z$
+\end{itemize}

equivalence_checking/practical_questions/1_1_circuit_lect.tex

@@ -0,0 +1,28 @@
+\item \lect Compute the propositional formula of the following circuit.
+
+\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 (z) at (8,-1) {$z$};
+
+    \node (am) at (1,0) {};
+    \node (bm) at (1,-1) {};
+
+    \node[or gate US, draw, logic gate inputs=nn] at ($(2,-.5)$) (or1) {\tiny OR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2)$) (not1) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(4,-1)$) (and1) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(6,-1)$) (not2) {\tiny NOT};
+
+    \node (or1m) at (3,-.5) {};
+    \node (not1m) at (3,-2) {};
+
+    \draw (a.east) -| (am.center) |- (or1.input 1);
+    \draw (b.east) |- (bm.center) |- (or1.input 2);
+    \draw (or1.output) |-  (or1m.center) node[above] {$w$} |- (and1.input 1);
+    \draw (c.east) |- (not1.input);
+    \draw (not1.output) |- (not1m.center) node[below] {$x$} |- (and1.input 2);
+    \draw (and1.output) -- node[below] {$y$} (not2.input);
+    \draw (not2.output) -- (z);
+\end{tikzpicture}

equivalence_checking/practical_questions/1_1_circuit_lect_sol.tex

@@ -0,0 +1,8 @@
+\begin{equation*} 
+\begin{split}
+z & = \neg y \\
+ & = \neg (w \land x) \\
+ & = \neg ((a \lor b) \land x) \\
+  & = \neg ((a \lor b) \land \neg c) \\
+\end{split}
+\end{equation*}

equivalence_checking/practical_questions/1_1_circuit_self.tex

@@ -0,0 +1,34 @@
+\item \self Compute the propositional formula of the following circuit.
+
+\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 (z) at (8,-1) {$z$};
+
+    \node (bm) at (3,-1) {};
+    \node (cm1) at (2,-2) {};
+    \node (cm2) at (3,-2) {};
+    \node (bc_c1) at (2,-1.1) {};
+    \node (bc_c2) at (2.1,-1) {};
+    \node (bc_c3) at (2,-.9) {};
+    \node (not1m) at (3,0) {};
+    \node (and1m) at (5,-.5) {};
+    \node (nand1m) at (5,-1.5) {};
+
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,0)$) (not1) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(4,-.5)$) (and1) {\tiny AND};
+    \node[nand gate US, draw, logic gate inputs=nn] at ($(4,-1.5)$) (nand1) {\tiny NAND};
+    \node[xor gate US, draw, logic gate inputs=nn] at ($(6,-1)$) (xor1) {\tiny XOR};
+
+    \draw (a.east) -- (not1.input);
+    \draw (not1.output) -| (not1m.center) node[above] {$w$} |- (and1.input 1);
+    \draw (c.east) -| (cm1.center) node[circle, fill,inner sep=2pt] {} -- (bc_c1.center) -- (bc_c2.center) -- (bc_c3.center) |- (and1.input 2);
+    \draw (b.east) -| (bm.center) |- (nand1.input 1);
+    \draw (c.east) -| (cm2.center) |- (nand1.input 2);
+    \draw (and1.output) -| (and1m.center) node[above] {$x$} |- (xor1.input 1);
+    \draw (nand1.output) -| (nand1m.center) node[below] {$y$} |- (xor1.input 2);
+    \draw (xor1.output) -- (z);
+\end{tikzpicture}
+

equivalence_checking/practical_questions/1_2_circuit_self.tex

@@ -0,0 +1,46 @@
+\item \self Compute the propositional formula of the following circuit.
+
+\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.5) {$c$};
+    \node (d) at (0,-3.5) {$d$};
+    \node (z) at (13.5,-1.5) {$z$};
+
+    \node (am) at (2,0) {};
+    \node (not1m) at (3,-1) {};
+    \node (not2m) at (3,-2.5) {};
+    \node (dm) at (2,-3.5) {};
+    \node (bm) at (1,-1) {};
+    \node (bm2) at (7,-1.875) {};
+    \node (not3m) at (7,-2.5) {};
+    \node (or1m) at (9,-.5) {};
+    \node (and1m) at (9,-2) {};
+
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-1)$) (not1) {\tiny NOT};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2.5)$) (not2) {\tiny NOT};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-.5)$) (or1) {\tiny OR};
+    \node[xor gate US, draw, logic gate inputs=nn] at ($(4,-3)$) (xor1) {\tiny XOR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(6,-3)$) (not3) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(8,-2)$) (and1) {\tiny AND};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(10,-1.5)$) (or2) {\tiny OR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(12,-1.5)$) (not4) {\tiny NOT};
+
+    \draw (a.east) -| (am.center) |- (or1.input 1);
+    \draw (b.east) -- (not1.input);
+    \draw (not1.output) -| (not1m.center) node[below] {$r$} |- (or1.input 2);
+    \draw (c.east) -- (not2.input);
+    \draw (not2.output) -| (not2m.center) node[above] {$s$} |- (xor1.input 1);
+    \draw (d.east) -| (dm.center) |- (xor1.input 2);
+    \draw (b.east) -| (bm.center) node[circle, fill,inner sep=2pt] {} |- (bm2.center) node[above] {$u$} |- (and1.input 1);
+    \draw (xor1.output) -- node[below] {$t$} (not3.input);
+    \draw (not3.output) -| node[below] {$v$} (not3m.center) |- (and1.input 2);
+    \draw (or1.output) -| (or1m.center) node[above] {$w$} |- (or2.input 1);
+    \draw (and1.output) -| (and1m.center) node[below] {$x$} |- (or2.input 2);
+    \draw (or2.output) -- node[below] {$y$} (not4.input);
+    \draw (not4.output) -- (z);
+
+
+\end{tikzpicture}
+

equivalence_checking/practical_questions/3_1_normal_forms_lect.tex

@@ -0,0 +1,2 @@
+\item \lect Given the formula $\phi = (q \imp p) \land (r \lor \lnot p)$. Compute its representation in Disjunctive Normal Form (\textit{DNF}) using a truth table.
+

equivalence_checking/practical_questions/3_1_normal_forms_lect_sol.tex

@@ -0,0 +1,31 @@
+\begin{tabular}{|c|c|c||c|c|c||c|}
+\hline
+$p$&$q$&$r$&$\lnot p$&$r \lor \lnot p$&$q \imp p$&$\phi$\\
+\hline
+\hline
+\textbf{F} &\textbf{F} &\textbf{F} & \textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\textbf{F} &\textbf{F} &\textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\textbf{F} &\textbf{T} &\textbf{F} & \textbf{T} & \textbf{T} & \textbf{F} & \textbf{F} \\
+\hline
+\textbf{F} &\textbf{T} &\textbf{T} & \textbf{T} & \textbf{T} & \textbf{F} & \textbf{F} \\
+\hline
+\textbf{T} &\textbf{F} &\textbf{F} & \textbf{F} & \textbf{F} & \textbf{T} & \textbf{F} \\
+\hline
+\textbf{T} &\textbf{F} &\textbf{T} & \textbf{F} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\textbf{T} &\textbf{T} &\textbf{F} & \textbf{F} & \textbf{F} & \textbf{T} & \textbf{F} \\
+\hline
+\textbf{T} &\textbf{T} &\textbf{T} & \textbf{F} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\end{tabular}
+
+\begin{equation*} 
+\begin{split}
+\textit{DNF}(\phi) = & (\lnot p \land \lnot q \land \lnot r) \\
+ \lor & (\lnot p \land \lnot q \land r) \\
+ \lor & (p \land \lnot q \land r) \\
+ \lor & (p \land q \land r) \\
+\end{split}
+\end{equation*}

equivalence_checking/practical_questions/3_1_normal_forms_self.tex

@@ -0,0 +1 @@
+\item \self Given the formula $\phi = (a \land \lnot b \land \lnot c) \lor ((\lnot c \imp a) \imp b)$. Use the truth table of $\phi$ to compute its representation in (a) CNF and (b) DNF. 

equivalence_checking/practical_questions/3_2_normal_forms_lect.tex

@@ -0,0 +1 @@
+\item \lect Given the formula $\phi = (q \imp p) \land (r \lor \lnot p)$. Compute its representation in Conjunctive Normal Form (\textit{CNF}) using a truth table.

equivalence_checking/practical_questions/3_2_normal_forms_lect_sol.tex

@@ -0,0 +1,31 @@
+\begin{tabular}{|c|c|c||c|c|c||c|}
+\hline
+$p$&$q$&$r$&$\lnot p$&$r \lor \lnot p$&$q \imp p$&$\phi$\\
+\hline
+\hline
+\textbf{F} &\textbf{F} &\textbf{F} & \textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\textbf{F} &\textbf{F} &\textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\textbf{F} &\textbf{T} &\textbf{F} & \textbf{T} & \textbf{T} & \textbf{F} & \textbf{F} \\
+\hline
+\textbf{F} &\textbf{T} &\textbf{T} & \textbf{T} & \textbf{T} & \textbf{F} & \textbf{F} \\
+\hline
+\textbf{T} &\textbf{F} &\textbf{F} & \textbf{F} & \textbf{F} & \textbf{T} & \textbf{F} \\
+\hline
+\textbf{T} &\textbf{F} &\textbf{T} & \textbf{F} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\textbf{T} &\textbf{T} &\textbf{F} & \textbf{F} & \textbf{F} & \textbf{T} & \textbf{F} \\
+\hline
+\textbf{T} &\textbf{T} &\textbf{T} & \textbf{F} & \textbf{T} & \textbf{T} & \textbf{T} \\
+\hline
+\end{tabular}
+
+\begin{equation*} 
+\begin{split}
+\textit{CNF}(\phi) = & (p \lor \lnot q \lor r) \\
+ \land & (p \lor \lnot q \lor \lnot r) \\
+ \land & (\lnot p \lor q \lor r) \\
+ \land & (\lnot p \lor \lnot q \lor r) \\
+\end{split}
+\end{equation*}

equivalence_checking/practical_questions/3_2_normal_forms_self.tex

@@ -0,0 +1 @@
+\item \self Given the formula $\phi = (q \imp \lnot r) \land \lnot (p \lor q \lor \lnot r)$. Use the truth table of $\phi$ to compute its representation in (a) CNF and (b) DNF. 

equivalence_checking/practical_questions/3_3_normal_forms_self.tex

@@ -0,0 +1,26 @@
+\item \self Consider the propositional formula $\phi = (p \lor \lnot q) \imp (\lnot p \land \lnot r)$. Fill out the truth table for $\phi$ 
+and its subformulas. Compute a CNF as well as a DNF for $\phi$ from
+the truth table. 
+
+\begin{tabular}{|c|c|c||c|c|c|c|c||c|}
+\hline
+$p$ & $q$ & $r$ & $\lnot q$ & $p \lor \lnot q$ & $\lnot p$ & $\lnot r$ & $\lnot p \land \lnot r$ & $\phi = (p \lor \lnot q) \imp (\lnot p \land \lnot r)$\\
+\hline
+\hline
+\textbf{F} &\textbf{F} &\textbf{F} & & & & & &\\
+\hline
+\textbf{F} &\textbf{F} &\textbf{T} & & & & & &\\
+\hline
+\textbf{F} &\textbf{T} &\textbf{F} & & & & & &\\
+\hline
+\textbf{F} &\textbf{T} &\textbf{T} & & & & & &\\
+\hline
+\textbf{T} &\textbf{F} &\textbf{F} & & & & & &\\
+\hline
+\textbf{T} &\textbf{F} &\textbf{T} & & & & & &\\
+\hline
+\textbf{T} &\textbf{T} &\textbf{F} & & & & & &\\
+\hline
+\textbf{T} &\textbf{T} &\textbf{T} & & & & & &\\
+\hline
+\end{tabular}

equivalence_checking/practical_questions/3_4_normal_forms_self.tex

@@ -0,0 +1 @@
+\item \self Given the formula $\phi = \lnot (a \imp \lnot b) \lor (\lnot a \imp c)$.  Use the truth table of $\phi$ to compute its representation in (a) CNF and (b) DNF. 

equivalence_checking/practical_questions/3_5_normal_forms_self.tex

@@ -0,0 +1,27 @@
+\item \self Consider the propositional formula $\phi = (\lnot(\lnot a
+    \land b) \land \lnot c)$. Fill out the truth table for $\phi$ 
+    and its subformulas. Compute a CNF as well as a DNF for $\phi$ from
+    the truth table.
+
+\begin{tabular}{|c|c|c||c|c|c|c||c|}
+\hline
+$a$&$b$&$c$&$\lnot a$&$\lnot a \land b$&$\lnot(\lnot a \land b)$&$\lnot c$&$\phi = (\lnot(\lnot a \land b) \land \lnot c)$\\
+\hline
+\hline
+\textbf{F} &\textbf{F} &\textbf{F} & & & & &\\
+\hline
+\textbf{F} &\textbf{F} &\textbf{T} & & & & &\\
+\hline
+\textbf{F} &\textbf{T} &\textbf{F} & & & & &\\
+\hline
+\textbf{F} &\textbf{T} &\textbf{T} & & & & &\\
+\hline
+\textbf{T} &\textbf{F} &\textbf{F} & & & & &\\
+\hline
+\textbf{T} &\textbf{F} &\textbf{T} & & & & &\\
+\hline
+\textbf{T} &\textbf{T} &\textbf{F} & & & & &\\
+\hline
+\textbf{T} &\textbf{T} &\textbf{T} & & & & &\\
+\hline
+\end{tabular}

equivalence_checking/practical_questions/4_1_tseitin_lect.tex

@@ -0,0 +1,4 @@
+\item \lect Explain the concept of equisatisfiability.
+Given a propositional logic formula $\varphi$, the Tseitin algorithm computes an 
+equisatisfiable formula $CNF(\varphi)$ in CNF. 
+Why is this enough for equivalence checking?

equivalence_checking/practical_questions/4_1_tseitin_lect_sol.tex

@@ -0,0 +1,4 @@
+Two propositional formulas $\varphi$ and $\psi$ are \emph{equisatisfiable} if and only if
+either \emph{both are satisfiable} or \emph{both are unsatisfiable}.
+
+When checking whether two formulas $\varphi_1$ and $\varphi_2$ are equivalent we check whether $\varphi = \varphi_1 \oplus \varphi_2$ is satisfiable. If $\varphi$ is \textit{SAT} we know that there is a model such that one of the input formulas evaluated to true, while the other evaluated to false. The equisatisfiable formula $CNF(\varphi)$ is satisfiable if and only if $\varphi$ is satisfiable and therefore answers our question of whether the two input formulas are equivalent.

equivalence_checking/practical_questions/4_1_tseitin_self.tex

@@ -0,0 +1,2 @@
+\item \self Apply Tseitin's encoding to the following formula: $$\phi = \lnot (\lnot b \land \lnot c) \lor (\lnot c \land a).$$
+For each variable you introduce, clearly indicate which subformula of $\phi$ it represents.

equivalence_checking/practical_questions/4_2_tseitin_lect.tex

@@ -0,0 +1,2 @@
+\item \lect Apply Tseitin's encoding to the following formula: $\phi = \lnot (a \lor \lnot b) \lor (\lnot a \land c)$.
+For each variable you introduce, clearly indicate which subformula of $\phi$ it represents.

equivalence_checking/practical_questions/4_2_tseitin_lect_sol.tex

@@ -0,0 +1,27 @@
+$$
+  \underbracket{
+    \underbracket{
+      \lnot
+      \underbracket{
+        (a \lor \underbracket{\lnot b}_{x_4})
+      }_{x_3}
+    }_{x_1}
+    \lor
+    \underbracket{
+      (\underbracket{\lnot a}_{x_5} \land c)
+    }_{x_2}
+  }_{x_\varphi}
+$$
+
+
+
+
+\begin{align*}
+CNF(\phi) = \ &x_\phi \land \\
+              &\tseitinAnd{x_\varphi}{x_1}{x_2} \land \\
+              &\tseitinNot{x_1}{x_3} \land \\
+              &\tseitinOr{x_3}{a}{x_4} \land \\
+              &\tseitinAnd{x_2}{x_5}{c} \land \\
+              &\tseitinNot{x_4}{b} \land \\
+              &\tseitinNot{x_5}{a} 
+\end{align*}

equivalence_checking/practical_questions/4_2_tseitin_self.tex

@@ -0,0 +1,2 @@
+\item \self Apply Tseitin's encoding to the following formula: $$\phi = (q \land \lnot r) \lor \lnot (q \land \lnot r)$$.
+For each variable you introduce, clearly indicate which subformula of $\phi$ it represents.

equivalence_checking/practical_questions/4_3_tseitin_self.tex

@@ -0,0 +1,2 @@
+\item \self Apply Tseitin's encoding to the following formula: $$\phi = (\lnot(\lnot a \land b) \land \lnot c).$$
+For each variable you introduce, clearly indicate which subformula of $\phi$ it represents.

equivalence_checking/practical_questions/4_4_tseitin_self.tex

@@ -0,0 +1,2 @@
+\item \self Apply Tseitin's encoding to the following formula: $$\phi = (p \lor \lnot q) \lor (\lnot p \land \lnot r).$$
+For each variable you introduce, clearly indicate which subformula of $\phi$ it represents.

equivalence_checking/practical_questions/4_5_tseitin_self.tex

@@ -0,0 +1,45 @@
+\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}

equivalence_checking/practical_questions/4_6_tseitin_self.tex

@@ -0,0 +1,38 @@
+\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 (z) at (10,-1) {$z$};
+
+    \node (am) at (1,0) {};
+    \node (cm) at (1,-2) {};
+    \node (bm) at (3,-1) {};
+    \node (not1m) at (3,-2) {};
+    \node (not2m) at (5,-.5) {};
+    \node (or1m) at (5,-1.5) {};
+    \node (bc_c1) at (1,-1.1) {};
+    \node (bc_c2) at (1.1,-1) {};
+    \node (bc_c3) at (1,-.9) {};
+    
+    \node[and gate US, draw, logic gate inputs=nn] at ($(2,-.5)$) (and1) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2)$) (not1) {\tiny NOT};
+    \node[not gate US, draw, logic gate inputs=n] at ($(4,-.5)$) (not2) {\tiny NOT};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-1.5)$) (or1) {\tiny OR};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(6,-1)$) (and2) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(8,-1)$) (not3) {\tiny NOT};
+
+    \draw (a.east) -| (am.center) |- (and1.input 1);
+    \draw (c.east) -| (cm.center) node[circle, fill,inner sep=2pt] {} -- (bc_c1.center) -- (bc_c2.center) -- (bc_c3.center) |- (and1.input 2);
+    \draw (b.east) -| (bm.center)|- (or1.input 1);
+    \draw (c.east) -- (not1.input);
+    \draw (and1.output) -- node[above] {$u$} (not2.input);
+    \draw (not1.output) -| (not1m.center) node[below] {$v$} |- (or1.input 2);
+    \draw (not2.output) -| (not2m.center) node[above] {$w$} |- (and2.input 1);
+    \draw (or1.output) -| (or1m.center) node[below] {$x$} |-  (and2.input 2);
+    \draw (and2.output) -- node[below] {$y$} (not3.input);
+    \draw (not3.output) -- (z.west);
+\end{tikzpicture}

equivalence_checking/practical_questions/4_7_tseitin_self.tex

@@ -0,0 +1,35 @@
+\item \lect Compute the propositional formula of the following circuit and transform it into an equisatisfiable formula in CNF by apply 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 (z) at (12,-1) {$z$};
+
+    \node (not1m) at (3,0) {};
+    \node (not2m) at (3,-1) {};
+    \node (not3m) at (7,-2) {};
+    \node (not4m) at (7,-.5) {};
+    
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-0)$) (not1) {\tiny NOT};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-1)$) (not2) {\tiny NOT};
+    \node[not gate US, draw, logic gate inputs=n] at ($(2,-2)$) (not3) {\tiny NOT};
+    \node[and gate US, draw, logic gate inputs=nn] at ($(4,-.5)$) (and1) {\tiny AND};
+    \node[not gate US, draw, logic gate inputs=n] at ($(6,-.5)$) (not4) {\tiny NOT};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(8,-1)$) (or1) {\tiny OR};
+    \node[not gate US, draw, logic gate inputs=n] at ($(10,-1)$) (not5) {\tiny NOT};
+
+    \draw (a.east) -- (not1.input);
+    \draw (b.east) -- (not2.input);
+    \draw (c.east) -- (not3.input);
+    \draw (not1.output) |- (not1m.center) node[above] {$t$} |- (and1.input 1);
+    \draw (not2.output) |- (not2m.center) node[below] {$u$} |- (and1.input 2);
+    \draw (and1.output) -- node[above] {$v$}  (not4.input);
+    \draw (not3.output) |- (not3m.center) node[below] {$x$} |- (or1.input 2);
+    \draw (not4.output) |- (not4m.center) node[above] {$w$} |- (or1.input 1);
+    \draw (or1.output) -- node[below] {$y$} (not5.input);
+    \draw (not5.output) -- (z.west);
+
+\end{tikzpicture}

equivalence_checking/practical_questions/5_1_cec_lect.tex

@@ -0,0 +1 @@
+\item \lect Check whether $\phi_1 = a \land \lnot b$ and $\phi_2 = \lnot ( \lnot a \lor b)$ are semantically equivalent using the reduction to satisfiability. Prepare everything until you have a formula CNF($\phi$), that you can give to a SAT solver.

equivalence_checking/practical_questions/5_1_cec_lect_old.tex

@@ -0,0 +1 @@
+\item \lect Check whether $\phi_1 = p \imp q$ and $\phi_2 = \lnot p \lor q$ are semantically equivalent using the reduction to satisfiability. Prepare everything until you have a formula CNF($\phi$), that you can give to a SAT solver.

equivalence_checking/practical_questions/5_1_cec_lect_sol.tex

@@ -0,0 +1,68 @@
+\begin{itemize}
+  \item We start by construction $\varphi$: \\
+    \begin{align*}
+      \varphi &= \varphi_1 \oplus \varphi_2 \\
+              &= [\varphi_1 \lor \varphi_2] \land \lnot [\varphi_1 \land \varphi_2] = \\
+              &= [(a \land \lnot b) \lor (\lnot(\lnot a \lor b))] \land \lnot [(a \land \lnot b) \land (\lnot(\lnot a \lor b))]
+    \end{align*}
+\end{itemize}
+
+$$
+  \underbracket{
+    \underbracket{\Big[
+      \underbracket{\big(
+        a
+        \land
+        \underbracket{\lnot b}_{x_{10}}
+      \big)}_{x_4}
+      \lor
+      \underbracket{\big(
+        \lnot
+          \underbracket{(
+            \underbracket{\lnot a}_{x_{11}}
+            \lor
+            b
+          )}_{x_8}
+      \big)}_{x_5}
+    \Big]}_{x_1}
+    \land
+    \underbracket{
+      \lnot
+      \underbracket{\Big[
+        \underbracket{\big(
+          a
+          \land
+          \underbracket{\lnot b}_{x_{12}}
+        \big)}_{x_6}
+        \lor
+        \underbracket{\big(
+          \lnot
+            \underbracket{(
+              \underbracket{\lnot a}_{x_{13}}
+              \lor
+              b
+            )}_{x_9}
+        \big)}_{x_7}
+      \Big]}_{x_3}
+    }_{x_2}
+  }_{x_\varphi}
+    $$
+
+
+\begin{align*}
+  CNF(\phi) = \ &x_\phi \land \\
+                &\tseitinAnd{x_{\varphi}}{x_1}{x_2} \land \\
+                &\tseitinNot{x_2}{x_3} \land \\
+                &\tseitinOr{x_1}{x_4}{x_5} \land \\
+                &\tseitinOr{x_3}{x_6}{x_7} \land \\
+                &\tseitinAnd{x_4}{a}{x_{10}} \land \\
+                &\tseitinNot{x_5}{x_8} \land \\
+                &\tseitinAnd{x_6}{a}{x_{12}} \land \\
+                &\tseitinNot{x_7}{x_9} \land \\
+                &\tseitinOr{x_8}{x_{11}}{b} \land \\
+                &\tseitinOr{x_9}{x_{13}}{b} \land \\
+                &\tseitinNot{x_{10}}{b} \land \\
+                &\tseitinNot{x_{11}}{a} \land \\
+                &\tseitinNot{x_{12}}{b} \land \\
+                &\tseitinNot{x_{13}}{a}
+\end{align*}

equivalence_checking/practical_questions/5_1_cec_self.tex

@@ -0,0 +1 @@
+\item \self Check whether $\phi_1 = (a \land b) \lor \lnot c$ and $\phi_2 = (a \lor \lnot c) \land (b \lor \lnot c)$ are semantically equivalent using the reduction to satisfiability. Prepare everything until you have a formula CNF($\phi$), that you can give to a SAT solver.

equivalence_checking/theory_questions/1_1_circuit_lect.tex

@@ -0,0 +1,2 @@
+\item \lect Explain the process of translating a combinational circuit into a propositional formula. 
+Draw a combinational circuit with 2 or 3 gates and give the corresponding propositional formula.

equivalence_checking/theory_questions/1_1_circuit_lect_sol.tex

@@ -0,0 +1,33 @@
+\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 (z) at (6,-1) {$z$};
+
+    \node (am) at (1,0) {};
+    \node (bm) at (1,-1) {};
+
+    \node[and gate US, draw, logic gate inputs=nn] at ($(2,-.5)$) (and1) {\tiny AND};
+    \node[or gate US, draw, logic gate inputs=nn] at ($(4,-1)$) (or1) {\tiny OR};
+
+    \node (and1m) at (3,-.5) {};
+    \node (c1m) at (3,-2) {};
+
+    \draw (a.east) -| (am.center) |- (and1.input 1);
+    \draw (b.east) |- (bm.center) |- (and1.input 2);
+    \draw (and1.output) |-  (and1m.center) node[above] {$y$} |- (or1.input 1);
+    \draw (c.east) |- (c1m.center) |- (or1.input 2);
+    \draw (or1.output) -- (z);
+\end{tikzpicture}
+
+The inputs are denoted by $a$, $b$, and $c$ and the output is denoted by $z$.
+We assign temporary variable names to the inner wires; in this case we use $y$.
+Using these variables, we can create the propositional formula over the inputs and the output.
+%
+\begin{equation*} 
+\begin{split}
+z & = y \lor c \\
+ & = (a \land b) \lor c
+\end{split}
+\end{equation*}

equivalence_checking/theory_questions/1_1_equiv_algorithm_lect.tex

@@ -0,0 +1 @@
+\item \lect Explain the algorithm of how to decide the equivalence of combinational circuits via the reduction to satisfiability.

equivalence_checking/theory_questions/1_1_equiv_algorithm_lect_sol.tex

@@ -0,0 +1,9 @@
+Let $C_1$ and $C_2$ denote the two combinational circuits.
+In order to check whether $C_1$ and $C_2$ are equivalent, one has to perform the following steps:
+\begin{enumerate}
+    \item Encode $C_1$ and $C_2$ into two propositional formulas $\varphi_1$ and $\varphi_2$.
+    \item Compute the Conjunctive Normal Form (CNF) of $\varphi_1 \oplus \varphi_2$,
+    using Tseitin encoding; i.e., $CNF(\varphi_1 \oplus \varphi_2)$. 
+    \item Give the formula  $CNF(\varphi_1 \oplus \varphi_2)$ to a SAT solver and check for satisfiability.
+    \item $C_1$ and $C_2$ are equivalent if and only if $CNF(\varphi_1 \oplus \varphi_2)$ is UNSAT.
+\end{enumerate}

equivalence_checking/theory_questions/2_1_relations_lect.tex

@@ -0,0 +1 @@
+\item \lect Explain the duality of \textit{satisfiability} and \textit{validity} and additional provide examples that show the duality.

equivalence_checking/theory_questions/2_1_relations_lect_sol.tex

@@ -0,0 +1,16 @@
+\emph{A formula $\varphi$ is valid, if and only if, $\neg \varphi$ is not satisfiable}.
+
+Consider the formula $\varphi=(x \vee \neg x)$. This formula is valid, i.e., all rows in the truth table 
+would evaluate to \emph{true}. The negation of $\varphi$ is the following: 
+$\neg \varphi = \neg (x \vee \neg x) = \neg x \wedge x$, which is not satisfiable, i.e., all rows the truth table would evaluate to \emph{false}.
+
+\noindent\emph{A formula $\varphi$ is satisfiable, if and only if, $\neg \varphi$ is not valid}.
+
+If $\varphi$ is satisfiable, there is at least one model that makes the formula true. If we negate the formula,
+these models make the negated formula false, and therefore, the negated formula cannot be valid.
+Consider the formula $\varphi=(x \vee y)$.
+There is at least one model that makes the formula true, e.g. $\mathcal{M} \coloneqq x = T, \ y = T$.
+The negation of $\varphi$ is the following: 
+$\neg \varphi = \neg (x \vee y) = \neg x \wedge \neg y$.
+Under the same model $\mathcal{M}$ as before, $\neg \varphi$ evaluates to false.
+So the negated formula is not valid.

equivalence_checking/theory_questions/2_1_relations_self.tex

@@ -0,0 +1 @@
+\item \self Considering the duality of \textit{satisfiability} and \textit{validity}, what can you deduce from a formula $\phi$ that is \textit{not valid}, regarding \textit{satisfiability}? Give also a short example of a not valid formula.

equivalence_checking/theory_questions/2_2_relations_lect.tex

@@ -0,0 +1 @@
+\item \lect How can you check whether it is true that $\phi \models \psi$ using a decision procedure for (a) \textit{satisfiability} or (b) \textit{validity}? 

equivalence_checking/theory_questions/2_2_relations_lect_sol.tex

@@ -0,0 +1,7 @@
+\begin{enumerate}
+\item \textbf{Decide entailment using satisfiability.}
+The question whether $\varphi \vDash  \psi$ can be decided by checking $\varphi \wedge \neg \psi$ not satisfiable.
+
+\item \textbf{Decide entailment using validity.}
+The question whether $\varphi \vDash \psi$ can be decided by checking $\varphi \rightarrow \psi$ is valid.
+\end{enumerate}

equivalence_checking/theory_questions/2_2_relations_self.tex

@@ -0,0 +1 @@
+\item \self \textit{A formula $\phi$ is valid, if and only if $\lnot \phi$ is not satisfiable.} Explain why this statement holds in your own words. 

equivalence_checking/theory_questions/2_3_relations_self.tex

@@ -0,0 +1,3 @@
+\item \self 
+Given two propositional logic formulas $\varphi$ and $\psi$. How can we check whether $\phi \equiv \psi$ using a decision procedure for (a) satisfiability, (b) for validity, and (c) for semantic entailment?
+

equivalence_checking/theory_questions/2_4_relations_self.tex

@@ -0,0 +1,3 @@
+\item \self 
+ Given a propositional logic formula $\varphi$. How can we check whether
+$\varphi$ is \emph{valid} using a decision procedure for (a) satisfiability and (b) equivalence?

equivalence_checking/theory_questions/2_5_relations_self.tex

@@ -0,0 +1 @@
+%\item \self SAT solvers in general use an \textit{exclusive or} between two formulas (i.e. $\phi \; \oplus \; \psi$) to check if the given formulas are \textit{equivalent}. Why does the formula $\chi = \phi \; \oplus \; \psi$ have to be "UNSAT" in order to prove that the two formulas $\phi$ and $\psi$ are \textit{equivalent}? What is the big advantage of using this method for checking \textit{equivalency} between two formulas?

equivalence_checking/theory_questions/3_0_normal_forms_self.tex

@@ -0,0 +1,3 @@
+\item \self 
+Define the \emph{Disjunctive Normal Form (DNF)} of formulas in propositional logic.
+Use the proper terminology and give an example.

equivalence_checking/theory_questions/3_1_normal_forms_lect.tex

@@ -0,0 +1 @@
+\item \lect Usually there are two standard \textit{normal forms}. Name both and give an example of each \textit{normal form} to highlight the differences between them.