diff --git a/compile b/compile
index 1cd5ad5..bc3c5f4 100755
--- a/compile
+++ b/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" "$@"
diff --git a/equivalence_checking/0000.tex b/equivalence_checking/0000.tex
new file mode 100644
index 0000000..8f8cbd8
--- /dev/null
+++ b/equivalence_checking/0000.tex
@@ -0,0 +1 @@
+\item Explain the algorithm used to decide the equivalence of combinational circuits via the reduction to satisfiability.
diff --git a/equivalence_checking/0000_sol.tex b/equivalence_checking/0000_sol.tex
new file mode 100644
index 0000000..c3e32e4
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/0001.tex b/equivalence_checking/0001.tex
new file mode 100644
index 0000000..9334c0c
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/0001_sol.tex b/equivalence_checking/0001_sol.tex
new file mode 100644
index 0000000..56baeb7
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/0002.tex b/equivalence_checking/0002.tex
new file mode 100644
index 0000000..b861203
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/0002_sol.tex b/equivalence_checking/0002_sol.tex
new file mode 100644
index 0000000..68d0005
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/0003.tex b/equivalence_checking/0003.tex
new file mode 100644
index 0000000..1852aab
--- /dev/null
+++ b/equivalence_checking/0003.tex
@@ -0,0 +1 @@
+\item Explain the duality of \textit{satisfiability} and \textit{validity}.
diff --git a/equivalence_checking/0003_sol.tex b/equivalence_checking/0003_sol.tex
new file mode 100644
index 0000000..99fc04c
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/0004.tex b/equivalence_checking/0004.tex
new file mode 100644
index 0000000..1f258c8
--- /dev/null
+++ b/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}? 
\ No newline at end of file
diff --git a/equivalence_checking/0004_sol.tex b/equivalence_checking/0004_sol.tex
new file mode 100644
index 0000000..6a81ba5
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/0005.tex b/equivalence_checking/0005.tex
new file mode 100644
index 0000000..ae1321b
--- /dev/null
+++ b/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?
diff --git a/equivalence_checking/0005_sol.tex b/equivalence_checking/0005_sol.tex
new file mode 100644
index 0000000..5e2f786
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/0006.tex b/equivalence_checking/0006.tex
new file mode 100644
index 0000000..816684c
--- /dev/null
+++ b/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)$?
diff --git a/equivalence_checking/0006_sol.tex b/equivalence_checking/0006_sol.tex
new file mode 100644
index 0000000..c60a694
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/0007.tex b/equivalence_checking/0007.tex
new file mode 100644
index 0000000..801ec46
--- /dev/null
+++ b/equivalence_checking/0007.tex
@@ -0,0 +1 @@
+\item Give the definition of equisatisfiability.
diff --git a/equivalence_checking/0007_sol.tex b/equivalence_checking/0007_sol.tex
new file mode 100644
index 0000000..65d1e26
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/0008.tex b/equivalence_checking/0008.tex
new file mode 100644
index 0000000..e6aac63
--- /dev/null
+++ b/equivalence_checking/0008.tex
@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = \lnot (a \lor \lnot b) \lor (\lnot a \land c)$}
diff --git a/equivalence_checking/0008_sol.tex b/equivalence_checking/0008_sol.tex
new file mode 100644
index 0000000..be827f9
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/0009.tex b/equivalence_checking/0009.tex
new file mode 100644
index 0000000..2737d7f
--- /dev/null
+++ b/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.
+
diff --git a/equivalence_checking/0009_sol.tex b/equivalence_checking/0009_sol.tex
new file mode 100644
index 0000000..5a6d659
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/0010.tex b/equivalence_checking/0010.tex
new file mode 100644
index 0000000..03f92e2
--- /dev/null
+++ b/equivalence_checking/0010.tex
@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = ((p \lor q) \land r) \lor \lnot p$}
diff --git a/equivalence_checking/0010_sol.tex b/equivalence_checking/0010_sol.tex
new file mode 100644
index 0000000..c213474
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/1000.tex b/equivalence_checking/1000.tex
new file mode 100644
index 0000000..54d2a64
--- /dev/null
+++ b/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}
+
diff --git a/equivalence_checking/1001.tex b/equivalence_checking/1001.tex
new file mode 100644
index 0000000..e6b2590
--- /dev/null
+++ b/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}
+
diff --git a/equivalence_checking/1002.tex b/equivalence_checking/1002.tex
new file mode 100644
index 0000000..ad3eddc
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/1003.tex b/equivalence_checking/1003.tex
new file mode 100644
index 0000000..4d18e0f
--- /dev/null
+++ b/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?
+
diff --git a/equivalence_checking/1004.tex b/equivalence_checking/1004.tex
new file mode 100644
index 0000000..a081330
--- /dev/null
+++ b/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?
diff --git a/equivalence_checking/1005.tex b/equivalence_checking/1005.tex
new file mode 100644
index 0000000..11c7300
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/1006.tex b/equivalence_checking/1006.tex
new file mode 100644
index 0000000..c778ed9
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/1007.tex b/equivalence_checking/1007.tex
new file mode 100644
index 0000000..78c4b1c
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/1008.tex b/equivalence_checking/1008.tex
new file mode 100644
index 0000000..b73da13
--- /dev/null
+++ b/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?
\ No newline at end of file
diff --git a/equivalence_checking/1009.tex b/equivalence_checking/1009.tex
new file mode 100644
index 0000000..7412db6
--- /dev/null
+++ b/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}.
\ No newline at end of file
diff --git a/equivalence_checking/1010.tex b/equivalence_checking/1010.tex
new file mode 100644
index 0000000..c2c105f
--- /dev/null
+++ b/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?
diff --git a/equivalence_checking/1011.tex b/equivalence_checking/1011.tex
new file mode 100644
index 0000000..ecb9048
--- /dev/null
+++ b/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!)
diff --git a/equivalence_checking/1012.tex b/equivalence_checking/1012.tex
new file mode 100644
index 0000000..025bcdb
--- /dev/null
+++ b/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)$?
\ No newline at end of file
diff --git a/equivalence_checking/1013.tex b/equivalence_checking/1013.tex
new file mode 100644
index 0000000..1bf6c5a
--- /dev/null
+++ b/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)$?
\ No newline at end of file
diff --git a/equivalence_checking/1014.tex b/equivalence_checking/1014.tex
new file mode 100644
index 0000000..da181a8
--- /dev/null
+++ b/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)$?
\ No newline at end of file
diff --git a/equivalence_checking/1015.tex b/equivalence_checking/1015.tex
new file mode 100644
index 0000000..9087f3d
--- /dev/null
+++ b/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)$}
diff --git a/equivalence_checking/1016.tex b/equivalence_checking/1016.tex
new file mode 100644
index 0000000..7bea2b2
--- /dev/null
+++ b/equivalence_checking/1016.tex
@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = (q \land \lnot r) \lor \lnot (q \land \lnot r)$}
diff --git a/equivalence_checking/1017.tex b/equivalence_checking/1017.tex
new file mode 100644
index 0000000..4b4207b
--- /dev/null
+++ b/equivalence_checking/1017.tex
@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = (\lnot(\lnot a \land b) \land \lnot c)$}
diff --git a/equivalence_checking/1018.tex b/equivalence_checking/1018.tex
new file mode 100644
index 0000000..fd5a9b8
--- /dev/null
+++ b/equivalence_checking/1018.tex
@@ -0,0 +1 @@
+\item \applyTseitin{$\phi = (p \lor \lnot q) \lor (\lnot p \land \lnot r)$}
diff --git a/equivalence_checking/1019.tex b/equivalence_checking/1019.tex
new file mode 100644
index 0000000..a6ffe14
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/1020.tex b/equivalence_checking/1020.tex
new file mode 100644
index 0000000..3358dc2
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/1021.tex b/equivalence_checking/1021.tex
new file mode 100644
index 0000000..9089e86
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/1025.tex b/equivalence_checking/1025.tex
new file mode 100644
index 0000000..b4dc222
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/equivalence_checking.tex b/equivalence_checking/equivalence_checking.tex
new file mode 100644
index 0000000..22372dd
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/multiple_choice/2_0_relations_self.tex b/equivalence_checking/multiple_choice/2_0_relations_self.tex
new file mode 100644
index 0000000..11c7300
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/2_1_relations_self.tex b/equivalence_checking/multiple_choice/2_1_relations_self.tex
new file mode 100644
index 0000000..c778ed9
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/2_2_relations_self.tex b/equivalence_checking/multiple_choice/2_2_relations_self.tex
new file mode 100644
index 0000000..78c4b1c
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/3_0_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_0_normal_forms_self.tex
new file mode 100644
index 0000000..ee26d44
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/3_1_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_1_normal_forms_self.tex
new file mode 100644
index 0000000..9bbd4b7
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/3_2_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_2_normal_forms_self.tex
new file mode 100644
index 0000000..df56929
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/multiple_choice/3_3_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_3_normal_forms_self.tex
new file mode 100644
index 0000000..67f45a0
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/3_4_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_4_normal_forms_self.tex
new file mode 100644
index 0000000..5d0ecb6
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/multiple_choice/3_5_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_5_normal_forms_self.tex
new file mode 100644
index 0000000..f7dfa91
--- /dev/null
+++ b/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}
+
+
diff --git a/equivalence_checking/multiple_choice/3_6_normal_forms_self.tex b/equivalence_checking/multiple_choice/3_6_normal_forms_self.tex
new file mode 100644
index 0000000..e3078d0
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/1_1_circuit_lect.tex b/equivalence_checking/practical_questions/1_1_circuit_lect.tex
new file mode 100644
index 0000000..81ec344
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/1_1_circuit_lect_sol.tex b/equivalence_checking/practical_questions/1_1_circuit_lect_sol.tex
new file mode 100644
index 0000000..419c040
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/practical_questions/1_1_circuit_self.tex b/equivalence_checking/practical_questions/1_1_circuit_self.tex
new file mode 100644
index 0000000..54d2a64
--- /dev/null
+++ b/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}
+
diff --git a/equivalence_checking/practical_questions/1_2_circuit_self.tex b/equivalence_checking/practical_questions/1_2_circuit_self.tex
new file mode 100644
index 0000000..75992c8
--- /dev/null
+++ b/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}
+
diff --git a/equivalence_checking/practical_questions/3_1_normal_forms_lect.tex b/equivalence_checking/practical_questions/3_1_normal_forms_lect.tex
new file mode 100644
index 0000000..f6813c6
--- /dev/null
+++ b/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.
+
diff --git a/equivalence_checking/practical_questions/3_1_normal_forms_lect_sol.tex b/equivalence_checking/practical_questions/3_1_normal_forms_lect_sol.tex
new file mode 100644
index 0000000..42aefdf
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/practical_questions/3_1_normal_forms_self.tex b/equivalence_checking/practical_questions/3_1_normal_forms_self.tex
new file mode 100644
index 0000000..fec8682
--- /dev/null
+++ b/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. 
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/3_2_normal_forms_lect.tex b/equivalence_checking/practical_questions/3_2_normal_forms_lect.tex
new file mode 100644
index 0000000..7e2a3f6
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/3_2_normal_forms_lect_sol.tex b/equivalence_checking/practical_questions/3_2_normal_forms_lect_sol.tex
new file mode 100644
index 0000000..db59e6c
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/practical_questions/3_2_normal_forms_self.tex b/equivalence_checking/practical_questions/3_2_normal_forms_self.tex
new file mode 100644
index 0000000..fa7677d
--- /dev/null
+++ b/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. 
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/3_3_normal_forms_self.tex b/equivalence_checking/practical_questions/3_3_normal_forms_self.tex
new file mode 100644
index 0000000..2f8ed84
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/3_4_normal_forms_self.tex b/equivalence_checking/practical_questions/3_4_normal_forms_self.tex
new file mode 100644
index 0000000..d641d19
--- /dev/null
+++ b/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. 
diff --git a/equivalence_checking/practical_questions/3_5_normal_forms_self.tex b/equivalence_checking/practical_questions/3_5_normal_forms_self.tex
new file mode 100644
index 0000000..6f24114
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_1_tseitin_lect.tex b/equivalence_checking/practical_questions/4_1_tseitin_lect.tex
new file mode 100644
index 0000000..cbb6891
--- /dev/null
+++ b/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?
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_1_tseitin_lect_sol.tex b/equivalence_checking/practical_questions/4_1_tseitin_lect_sol.tex
new file mode 100644
index 0000000..65d1e26
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_1_tseitin_self.tex b/equivalence_checking/practical_questions/4_1_tseitin_self.tex
new file mode 100644
index 0000000..c1ecdb6
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_2_tseitin_lect.tex b/equivalence_checking/practical_questions/4_2_tseitin_lect.tex
new file mode 100644
index 0000000..bb8e67d
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_2_tseitin_lect_sol.tex b/equivalence_checking/practical_questions/4_2_tseitin_lect_sol.tex
new file mode 100644
index 0000000..0d55641
--- /dev/null
+++ b/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*}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_2_tseitin_self.tex b/equivalence_checking/practical_questions/4_2_tseitin_self.tex
new file mode 100644
index 0000000..2a3832d
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_3_tseitin_self.tex b/equivalence_checking/practical_questions/4_3_tseitin_self.tex
new file mode 100644
index 0000000..0cc997c
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_4_tseitin_self.tex b/equivalence_checking/practical_questions/4_4_tseitin_self.tex
new file mode 100644
index 0000000..22d1f2d
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_5_tseitin_self.tex b/equivalence_checking/practical_questions/4_5_tseitin_self.tex
new file mode 100644
index 0000000..e36fee0
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/practical_questions/4_6_tseitin_self.tex b/equivalence_checking/practical_questions/4_6_tseitin_self.tex
new file mode 100644
index 0000000..5e943bc
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/4_7_tseitin_self.tex b/equivalence_checking/practical_questions/4_7_tseitin_self.tex
new file mode 100644
index 0000000..425f8fc
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/5_1_cec_lect.tex b/equivalence_checking/practical_questions/5_1_cec_lect.tex
new file mode 100644
index 0000000..882c5ef
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/5_1_cec_lect_old.tex b/equivalence_checking/practical_questions/5_1_cec_lect_old.tex
new file mode 100644
index 0000000..d893737
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/5_1_cec_lect_sol.tex b/equivalence_checking/practical_questions/5_1_cec_lect_sol.tex
new file mode 100644
index 0000000..ac44427
--- /dev/null
+++ b/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*}
\ No newline at end of file
diff --git a/equivalence_checking/practical_questions/5_1_cec_self.tex b/equivalence_checking/practical_questions/5_1_cec_self.tex
new file mode 100644
index 0000000..0baee70
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/1_1_circuit_lect.tex b/equivalence_checking/theory_questions/1_1_circuit_lect.tex
new file mode 100644
index 0000000..9334c0c
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/1_1_circuit_lect_sol.tex b/equivalence_checking/theory_questions/1_1_circuit_lect_sol.tex
new file mode 100644
index 0000000..56baeb7
--- /dev/null
+++ b/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*}
diff --git a/equivalence_checking/theory_questions/1_1_equiv_algorithm_lect.tex b/equivalence_checking/theory_questions/1_1_equiv_algorithm_lect.tex
new file mode 100644
index 0000000..74da572
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/1_1_equiv_algorithm_lect_sol.tex b/equivalence_checking/theory_questions/1_1_equiv_algorithm_lect_sol.tex
new file mode 100644
index 0000000..c3e32e4
--- /dev/null
+++ b/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}
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/2_1_relations_lect.tex b/equivalence_checking/theory_questions/2_1_relations_lect.tex
new file mode 100644
index 0000000..ec88fc6
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/2_1_relations_lect_sol.tex b/equivalence_checking/theory_questions/2_1_relations_lect_sol.tex
new file mode 100644
index 0000000..cee580f
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/theory_questions/2_1_relations_self.tex b/equivalence_checking/theory_questions/2_1_relations_self.tex
new file mode 100644
index 0000000..d07278f
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/2_2_relations_lect.tex b/equivalence_checking/theory_questions/2_2_relations_lect.tex
new file mode 100644
index 0000000..1f258c8
--- /dev/null
+++ b/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}? 
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/2_2_relations_lect_sol.tex b/equivalence_checking/theory_questions/2_2_relations_lect_sol.tex
new file mode 100644
index 0000000..6a81ba5
--- /dev/null
+++ b/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}
diff --git a/equivalence_checking/theory_questions/2_2_relations_self.tex b/equivalence_checking/theory_questions/2_2_relations_self.tex
new file mode 100644
index 0000000..a1d5176
--- /dev/null
+++ b/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. 
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/2_3_relations_self.tex b/equivalence_checking/theory_questions/2_3_relations_self.tex
new file mode 100644
index 0000000..4d18e0f
--- /dev/null
+++ b/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?
+
diff --git a/equivalence_checking/theory_questions/2_4_relations_self.tex b/equivalence_checking/theory_questions/2_4_relations_self.tex
new file mode 100644
index 0000000..a081330
--- /dev/null
+++ b/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?
diff --git a/equivalence_checking/theory_questions/2_5_relations_self.tex b/equivalence_checking/theory_questions/2_5_relations_self.tex
new file mode 100644
index 0000000..b73da13
--- /dev/null
+++ b/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?
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/3_0_normal_forms_self.tex b/equivalence_checking/theory_questions/3_0_normal_forms_self.tex
new file mode 100644
index 0000000..184287d
--- /dev/null
+++ b/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.
diff --git a/equivalence_checking/theory_questions/3_1_normal_forms_lect.tex b/equivalence_checking/theory_questions/3_1_normal_forms_lect.tex
new file mode 100644
index 0000000..95bf635
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/3_1_normal_forms_self.tex b/equivalence_checking/theory_questions/3_1_normal_forms_self.tex
new file mode 100644
index 0000000..4c1c46b
--- /dev/null
+++ b/equivalence_checking/theory_questions/3_1_normal_forms_self.tex
@@ -0,0 +1,4 @@
+\item \self 
+Define the \emph{Conjunctive Normal Form (CNF)} of formulas in propositional logic.
+Use the proper terminology and give an example.
+
diff --git a/equivalence_checking/theory_questions/3_2_normal_forms_lect.tex b/equivalence_checking/theory_questions/3_2_normal_forms_lect.tex
new file mode 100644
index 0000000..6187a34
--- /dev/null
+++ b/equivalence_checking/theory_questions/3_2_normal_forms_lect.tex
@@ -0,0 +1,2 @@
+\item \lect Explain the following terms and give examples: (a) literal,
+(b) cube, and (c) clause.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/3_2_normal_forms_lect_sol.tex b/equivalence_checking/theory_questions/3_2_normal_forms_lect_sol.tex
new file mode 100644
index 0000000..9ed69a3
--- /dev/null
+++ b/equivalence_checking/theory_questions/3_2_normal_forms_lect_sol.tex
@@ -0,0 +1,9 @@
+Let $\varphi$ be a propositional formula defined
+over Boolean variables $x_1, . . . ,x_n$.
+
+\begin{itemize}
+    \item A \emph{literal} is one of the variables $x_i$ or the negation of a variable, e.g., $x_1$.
+    \item A \emph{clause} is a disjunction of literals, e.g., $x_1 \vee x_2$. 
+    \item A \emph{cube} is a conjunction of literals, e.g., $x_1 \wedge x_2$. 
+\end{itemize}
+
diff --git a/equivalence_checking/theory_questions/3_2_normal_forms_self.tex b/equivalence_checking/theory_questions/3_2_normal_forms_self.tex
new file mode 100644
index 0000000..2b8a318
--- /dev/null
+++ b/equivalence_checking/theory_questions/3_2_normal_forms_self.tex
@@ -0,0 +1 @@
+%\item \self Given the formula $\phi = (p \lor \lnot q \lor \lnot r) \land (\lnot p \lor q \lor \lnot r) \land (p \lor q \lor r)$, which type of normal form, does this formula represent? Name all parts of the formula with the correct terminology.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/3_3_normal_forms_self.tex b/equivalence_checking/theory_questions/3_3_normal_forms_self.tex
new file mode 100644
index 0000000..85c97ce
--- /dev/null
+++ b/equivalence_checking/theory_questions/3_3_normal_forms_self.tex
@@ -0,0 +1,6 @@
+
+
+
+
+
+\item \self Given a formula in propositional logic. Explain how to extract a \textit{CNF} representation as well as a \textit{DNF} representation of $\phi$ using the truth table from $\phi$. 
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_1_tseitin_lect.tex b/equivalence_checking/theory_questions/4_1_tseitin_lect.tex
new file mode 100644
index 0000000..16f9efa
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_1_tseitin_lect.tex
@@ -0,0 +1 @@
+\item \lect Why are truth tables, in general, not used to compute CNFs of formulas?
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_1_tseitin_self.tex b/equivalence_checking/theory_questions/4_1_tseitin_self.tex
new file mode 100644
index 0000000..7412db6
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_1_tseitin_self.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}.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_2_tseitin_lect.tex b/equivalence_checking/theory_questions/4_2_tseitin_lect.tex
new file mode 100644
index 0000000..9ef58dc
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_2_tseitin_lect.tex
@@ -0,0 +1,2 @@
+\item \lect What is the advantage of applying \textit{Tseitin encoding} to obtain a CNF,
+especially compared to using truth tables?
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_2_tseitin_lect_sol.tex b/equivalence_checking/theory_questions/4_2_tseitin_lect_sol.tex
new file mode 100644
index 0000000..ad9f904
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_2_tseitin_lect_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.
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_2_tseitin_self.tex b/equivalence_checking/theory_questions/4_2_tseitin_self.tex
new file mode 100644
index 0000000..7bbd091
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_2_tseitin_self.tex
@@ -0,0 +1,4 @@
+\item \self Suppose you have a propositional formula $\phi$. Let $\psi$ be the result 
+      of applying Tseitin's encoding to $\phi$. Is $\phi$ \emph{equivalent} to $\psi$?
+      Provide a reason for your answer and explain the relation between $\phi$ and $\psi$.
+
diff --git a/equivalence_checking/theory_questions/4_3_tseitin_lect_sol.tex b/equivalence_checking/theory_questions/4_3_tseitin_lect_sol.tex
new file mode 100644
index 0000000..d522bd8
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_3_tseitin_lect_sol.tex
@@ -0,0 +1,17 @@
+Given are two combinational circuits $C_1$ and $C_2$.
+First we translate $C_1$ and $C_2$ into their respective formula $\varphi_1$ and $\varphi_2$.
+We need to check, whether $\varphi_1 \oplus \varphi_2$ is not satisfiable, i.e, \emph{$\varphi_1 \equiv \varphi_2$ if and only if $\varphi_1 \oplus \varphi_2$ is UNSAT}. Therefore, we perform the following steps.
+
+\begin{itemize}
+    \item We construct the formula $\varphi$:
+    \begin{equation*}
+    \begin{split}
+    \varphi = \varphi_1 \oplus \varphi_2
+    \end{split}
+    \end{equation*}
+
+    \item Next, the formula $\varphi$ has to be transformed into a CNF formula by using Tseitin encoding.
+
+    \item Finally, the formula $CNF(\varphi)$ is given to a SAT solver. If the SAT solver determines that $CNF(\varphi)$ is unsatisfiable, then $\varphi_1 \equiv \varphi_2$.
+    If the SAT solver determines that $CNF(\varphi)$ is satisfiable, then $\varphi_1 \not\equiv \varphi_2$.
+\end{itemize}
diff --git a/equivalence_checking/theory_questions/4_3_tseitin_self.tex b/equivalence_checking/theory_questions/4_3_tseitin_self.tex
new file mode 100644
index 0000000..25d92e4
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_3_tseitin_self.tex
@@ -0,0 +1,5 @@
+\item \self Explain the concept of \emph{Tseitin's Encoding} to obtain
+    formulas in CNF. Give step-by-step instructions of how to
+    apply Tseitin's encoding to a propositional formula.\\
+    (Note: Focus on the concept. You do \emph{not} need to quote
+    the rewrite rules!)
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_4_tseitin_lect.tex b/equivalence_checking/theory_questions/4_4_tseitin_lect.tex
new file mode 100644
index 0000000..f340866
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_4_tseitin_lect.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)$?
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_4_tseitin_lect_sol.tex b/equivalence_checking/theory_questions/4_4_tseitin_lect_sol.tex
new file mode 100644
index 0000000..c60a694
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_4_tseitin_lect_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*}
diff --git a/equivalence_checking/theory_questions/4_4_tseitin_self.tex b/equivalence_checking/theory_questions/4_4_tseitin_self.tex
new file mode 100644
index 0000000..025bcdb
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_4_tseitin_self.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)$?
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_5_tseitin_self.tex b/equivalence_checking/theory_questions/4_5_tseitin_self.tex
new file mode 100644
index 0000000..1bf6c5a
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_5_tseitin_self.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)$?
\ No newline at end of file
diff --git a/equivalence_checking/theory_questions/4_6_tseitin_self.tex b/equivalence_checking/theory_questions/4_6_tseitin_self.tex
new file mode 100644
index 0000000..da181a8
--- /dev/null
+++ b/equivalence_checking/theory_questions/4_6_tseitin_self.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)$?
\ No newline at end of file
diff --git a/main.tex b/main.tex
index edf98f4..5b4dd2a 100644
--- a/main.tex
+++ b/main.tex
@@ -57,6 +57,7 @@
 \clearpage
 
 
+
 \ifchapterproplogic
   \setsectionnum{0}
   \section{Propositional Logic}
@@ -85,6 +86,54 @@
   \pagebreak
 \fi
 
+\ifchaptereqchecking
+  \setsectionnum{4}
+  \section{Combinational Equivalence Checking}
+  \input{equivalence_checking/equivalence_checking.tex}
+  \pagebreak
+\fi
+\ifchaptersmtzthree
+  \setsectionnum{5}
+  \section{SMT Solvers and Z3}
+  \input{smt_and_z3/smt_and_z3.tex}
+  \pagebreak
+\fi
+
+\ifchapterpredlogic
+  \setsectionnum{4}
+  \section{Predicate Logic}
+  \input{predicate_logic/predicate_logic.tex}
+  \pagebreak
+\fi
+
+\ifchapterndpred
+  \setsectionnum{5}
+  \section{Natural Deduction for Predicate Logic}
+  \input{natural_deduction_predicate_logic/natural_deduction_predicate_logic.tex}
+  \pagebreak
+\fi
+
+\ifchaptersmt
+  \setsectionnum{6}
+  \section{Satisfiability Modulo Theories}
+  \input{smt/smt.tex}
+  \pagebreak
+\fi
+
+
+\ifchaptersymbenc
+  \setsectionnum{9}
+  \section{Symbolic Encoding}
+  \input{symbolic_encoding/symbolic_encoding.tex}
+  \pagebreak
+\fi
+
+\ifchaptertemporal
+  \setsectionnum{10}
+  \section{Temporal Logic}
+  \input{temporal_logic/temporal_logic.tex}
+  \pagebreak
+\fi
 %---------------------------------------------------------
 
 
diff --git a/util/constants.tex b/util/constants.tex
index 7fe96fb..ab586b6 100644
--- a/util/constants.tex
+++ b/util/constants.tex
@@ -33,3 +33,13 @@ Transform the given Binary Decision Diagram into a reduced and ordered BDD.}
 \newcommand{\BDDToDNF}{%
 Given the following Binary Decision Diagram that represents the formula $f$. Compute its disjunctive normal form \DNF{f}.}
 
+
+\newcommand{\computeCNFDNF}[1][\varphi]{%
+Compute \DNF{#1} and \CNF{#1} using a truth table.
+}
+\newcommand{\CNFfromCircuit}{%
+Compute the propositional formula $\varphi$ represented by the following circuit. Furthermore, compute an equisatisfiable formula $\varphi'$ using the Tseitin transformation.
+}
+\newcommand{\applyTseitin}[1]{%
+  Apply the Tseitin transformation to #1. For each variable you introduce, clearly indicate which subformula it represents.
+}