added smt chapter

compile

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

main.tex

@@ -112,9 +112,8 @@
   \input{natural_deduction_predicate_logic/natural_deduction_predicate_logic.tex}
   \pagebreak
 \fi
-
 \ifchaptersmt
-  \setsectionnum{6}
+  \setsectionnum{8}
   \section{Satisfiability Modulo Theories}
   \input{smt/smt.tex}
   \pagebreak

smt/0001.tex

@@ -0,0 +1,2 @@
+
+\item \lect Give the definition of a theory of formulas in first-order logic.

smt/0001_sol.tex

@@ -0,0 +1,4 @@
+A theory is as a pair $(\Sigma;\mathcal{A})$ where $\Sigma$ is a signature 
+which defines a set of constant, function, and predicate symbols.
+The set of axioms $\mathcal{A}$ is a set of closed predicate logic formulas in which only
+constant, function, and predicate symbols of $\Sigma$ appear.

smt/0002.tex

@@ -0,0 +1 @@
+\item \lect Explain the concept of a theory in first-order logic using the \emph{theory of Linear Integer Arithmetic} $\mathcal{T}_{LIA}$ as example.

smt/0002_sol.tex

@@ -0,0 +1,16 @@
+Variables in  $\mathcal{T}_{LIA}$ are of integer sort ($\mathbb{Z}$).
+The functions of $\mathcal{T}_{LIA}$ are $+$ and $-$ and the predicates are
+$=, \neq, <, >, \leq,$ and  $\geq$. The axioms withing $\mathcal{T}_{LIA}$
+define the meaning for these functions and predicates.
+
+Therefore, for the theory of Linear Integer Arithmetic $\mathcal{T}_{LIA}$ we have:
+
+\begin{itemize}
+  \item $\Sigma = \Z \union \{+,-\} \union \{=, \neq, <, \leq,>,\geq\} $
+\item $\mathcal{A}$ defines the usual meaning to all symbols:
+  \begin{itemize}
+    \item Constant symbols are mapped to the corresponding value in $\Z$.
+    \item $+$ is interpreted as the function $0+0 \rightarrow 0, 0+1 \rightarrow 1, \ldots$. $-$ follows it analogous interpretation.
+    \item The predicate symbols are interpreted as their respective comparison operator.
+  \end{itemize}
+\end{itemize}

smt/0003.tex

@@ -0,0 +1,7 @@
+\item Explain the problem of satisfiability modulo theories. As part of your explanation, explain what a theory is and explain the meaning of theory-satisfiability.
+
+
+
+
+
+

smt/0003_sol.tex

@@ -0,0 +1,7 @@
+The satisfiability modulo theories (SMT) problem refers
+to the problem of determining whether a formula in predicate logic is satisfiable
+with respect to some theory. A theory fixes the interpretation/meaning of certain
+predicate and function symbols. Checking whether a formula in predicate logic is
+satisfiable with respect to a theory means that we are not interested in arbitrary
+models but in models that interpret the functions and predicates contained in
+the theory as defined by the axioms in the theory.

smt/0004.tex

@@ -0,0 +1 @@
+\item Give the definitions of \emph{$\mathcal{T}$-terms}, \emph{$\mathcal{T}$-atoms} and \emph{$\mathcal{T}$-literals} for SMT formulas.

smt/0004_sol.tex

@@ -0,0 +1,13 @@
+\begin{itemize}
+  \item $\Theory$-terms: A \emph{$\Theory$-term} is either a constant or variables $x,y,\ldots$.
+    An application of a function symbol in $\Sigma$ where all inputs are $\Theory$-terms is a $\Theory$-term.
+
+Examples for $\Theory$-terms in $\LIA$ are: $x+2$, $5$, $x-y$.
+
+\item $\Theory$-atom: A \emph{$\Theory$-atom} is the application of a predicate symbol in $\Sigma$ where all inputs are $\Theory$-terms.
+
+Examples for $\Theory$-atoms in $\LIA$ are: $x+2>0$, $5\leq 2$, $x-y>10$.
+
+\item $\Theory$-literal: A \emph{$\Theory$-literal} is a $\Theory$-atoms or its negation.
+
+\end{itemize}

smt/0005.tex

@@ -0,0 +1,2 @@
+\item \lect What is the difference between a model of an SMT formula
+and a model of a predicate logic formula without a theory? 

smt/0005_sol.tex

@@ -0,0 +1,4 @@
+A model in predicate logic needs to define the domain of the variables and needs to define a concrete meaning to all predicate
+and function symbols and free variables involved. 
+
+In SMT, the domain and the interpretation of the predicate and function symbols is fixed. A model for an SMT formula only defines an assignment to all free variables within the formula.

smt/0006.tex

@@ -0,0 +1,3 @@
+\item \lect Given the signature $\Sigma_{EUF}\coloneqq \{a,b,c,\ldots\} \union \{f,g,h,\ldots\} \union \{=,P,Q,R,\ldots\},$
+ of the \textit{Theory of Equality and Uninterpreted Functions} $\mathcal{T}_{EUF}$.
+State the axioms $\mathcal{A}_{EUF}$ of $\mathcal{T}_{EUF}$.

smt/0006_sol.tex

@@ -0,0 +1,9 @@
+The axioms $\mathcal{A}_{EUF}$ are the following:
+
+\begin{enumerate}
+    \item  $\forall x.~~x = x$ (reflexivity)
+    \item  $\forall x, y.~~x = y \rightarrow y = x$ (symmetry)
+    \item  $\forall x, y, z.~~x = y \wedge y = z \rightarrow x = z$ (transitivity)
+    \item  $\forall \overline{x}, \overline{y}.~~ ( \bigwedge_{i=1}^n x_i = y_i ) \rightarrow f(\overline{x}) = f(\overline{y})$ (congruence)
+    \item  $\forall \overline{x}, \overline{y}.~~ ( \bigwedge_{i=1}^n x_i = y_i ) \rightarrow (P(\overline{x}) \leftrightarrow P(\overline{y}))$ (equivalence)
+\end{enumerate}

smt/0007.tex

@@ -0,0 +1 @@
+\item Explain the concepts of eager encoding and lazy encoding in the context of solving  formulas in SMT.

smt/0007_sol.tex

@@ -0,0 +1,10 @@
+\begin{itemize}
+    \item In eager encoding, all axioms of the theory are explicitly incorporated into the input formula. The resulting equisatisfiable propositional formula is then given to a SAT solver.
+
+\item SMT solvers that use lazy encoding use specialized theory solvers in combination with SAT solvers to decide the satisfiability of formulas within a given theory.
+In contrast to eager encoding, where a
+sufficient set of constraints is computed at the beginning, lazy encoding starts
+with no constraints at all, and lazily adds constraints only when required.
+\end{itemize}
+
+

smt/0008.tex

@@ -0,0 +1,2 @@
+\item Explain the concept of eager encoding to solve formulas in
+in SMT. State the 3 main steps that are performed in algorithms based on eager encoding.

smt/0008_sol.tex

@@ -0,0 +1,12 @@
+The main idea of eager encoding is that the input formula is translated into a
+propositional formula with all relevant theory-specific information encoded into
+the formula.
+
+\begin{enumerate}[label=(\Roman*)]
+  \item Replace any unique $\Theory$-atom in the original formula $\varphi$ with a fresh propositional variable to get a propositional formula $\hat{\varphi}$. \label{item:varphi_prop}
+\item Generate a propositional formula $\varphi_{cons}$ that constrains the values of the introduced
+  propositional variables to preserve the information of the theory. \label{item:varphi_cons}
+
+\item Invoke a SAT solver on the propositional formula $\varphi_{prop} \coloneqq \hat{\varphi} \land \varphi_{cons}$
+that corresponds to an equisatisfiable propositional formula to $\varphi$.
+\end{enumerate}

smt/0009.tex

@@ -0,0 +1 @@
+\item \lect Explain the specific translations used in \emph{eager encoding} to decide formulas in the theory of equality and uninterpreted functions.

smt/0009_sol.tex

@@ -0,0 +1,5 @@
+The translations used in the eager approach for $\mathcal{T}_{EUF}$ are: 
+\begin{enumerate}
+    \item Ackermann Reduction: to remove all function instances, resulting in an equisatisfiable formula in $\mathcal{T}_{E}$.
+    \item Graph-Based Reduction: to remove all equality instances, resulting in an equisatisfiable formula in propositional logic.
+\end{enumerate}

smt/0010.tex

@@ -0,0 +1,5 @@
+\item \applyAckermann{
+    \begin{equation*}
+        \varphi_{EUF} \quad := \quad f(x)=f(y) \; \lor \; (z=y \land z \neq f(z))
+    \end{equation*}
+   }

smt/0010_sol.tex

@@ -0,0 +1,11 @@
+    \begin{align*}
+         \varphi_{FC} \quad := \quad & (x=y \rightarrow f_{x} = f_y) \wedge \\
+         &(x=z \rightarrow f_{x} = f_z) \wedge \\
+         &(y=z \rightarrow f_y = f_z)
+    \end{align*}
+    \begin{align*}
+         \hat{\varphi}_{EUF} \quad := \quad f_{x}=f_y \; \lor \; (z=y \land z \neq f_z)
+    \end{align*}
+    \begin{align*}
+         \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
+    \end{align*}

smt/0011.tex

@@ -0,0 +1,5 @@
+\item \applyAckermann{
+    \begin{equation*}
+        \varphi_{EUF} \quad := \quad f(g(x))=f(y) \; \lor \; (z=g(y) \land z \neq f(z))
+    \end{equation*}
+  }

smt/0011_sol.tex

@@ -0,0 +1,12 @@
+    \begin{align*}
+         \varphi_{FC} \quad := \quad &  (x=y \rightarrow g_x = g_y) \wedge \\
+        & (g_x=y \rightarrow f_{gx} = f_y) \wedge \\
+         &(g_x=z \rightarrow f_{gx} = f_z) \wedge \\
+         &(y=z \rightarrow f_y = f_z)
+    \end{align*}
+    \begin{align*}
+         \hat{\varphi}_{EUF} \quad := \quad f_{gx}=f_y \; \lor \; (z=g_y \land z \neq f_z)
+    \end{align*}
+    \begin{align*}
+         \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
+    \end{align*}

smt/0012.tex

@@ -0,0 +1,5 @@
+\item \applyAckermann{
+    \begin{equation*}
+        \varphi_{EUF} \quad := \quad f(x,y)=f(y,z) \; \lor \; (z=f(y,z) \land f(x,x) \neq f(x,y))
+    \end{equation*}
+  }

smt/0012_sol.tex

@@ -0,0 +1,12 @@
+    \begin{align*}
+         \varphi_{FC} \quad := \quad 
+         &(x=y \wedge y=z \rightarrow f_{xy} = f_{yz}) \wedge \\
+         &(x=x \wedge y=x \rightarrow f_{xy} = f_{xx}) \wedge \\
+         &(y=x \wedge z=x \rightarrow f_{yz} = f_{xx})
+    \end{align*}
+    \begin{align*}
+         \hat{\varphi}_{EUF} \quad := \quad f_{xy}=f_{yz} \; \lor \; (z=f_{yz} \land f_{xx} \neq f_{xy})
+    \end{align*}
+    \begin{align*}
+         \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
+    \end{align*}

smt/0013.tex

@@ -0,0 +1,6 @@
+\item \applyGB{
+    \begin{equation*}
+        \phi_E \;\; := \;\; (a=b \; \lor \; a=d) \imp (b=c \; \land \; c \neq d)
+    \end{equation*}
+  }
+

smt/0013_sol.tex

@@ -0,0 +1,22 @@
+ We choose: 
+ \begin{itemize}
+     \item Triangle 1: a-b-c
+     \item Triangle 2: a-c-d
+ \end{itemize}
+ \begin{align*}
+      \varphi_{TC} \coloneqq &
+                       (e_{a = b} \land e_{b = c} \rightarrow e_{a = c}) \land \\
+                       & (e_{a = b} \land e_{a = c} \rightarrow e_{b = c}) \land \\
+                       & (e_{b = c} \land e_{a = c} \rightarrow e_{a = b}) \land \\
+                       &\\
+                       & (e_{a = c} \land e_{c = d} \rightarrow e_{a = d}) \land \\
+                       & (e_{a = c} \land e_{a = d} \rightarrow e_{c = d}) \land \\
+                       & (e_{c = d} \land e_{a = d} \rightarrow e_{a = c}) 
+        \end{align*}
+    \begin{align*}
+      \hat\varphi_{E} \coloneqq
+                          (e_{a=b} \; \lor \; e_{a=d} \imp (e_{b=c} \; \land \; \neg e_{c = d})
+    \end{align*}
+    \begin{align*}
+     \varphi_{prop} \coloneqq \varphi_{TC} \land \hat\varphi_{E} 
+    \end{align*}

smt/0014.tex

@@ -0,0 +1,6 @@
+\item \applyGB{
+    \begin{equation*}
+        \phi_E \;\; := \;\; (a=b \; \lor \; a=d) \imp (b=c \; \land \; c \neq e \land \; e \neq d)
+    \end{equation*}
+  }
+

smt/0014_sol.tex

@@ -0,0 +1,27 @@
+ We choose: 
+ \begin{itemize}
+     \item Triangle 1: a-b-c
+     \item Triangle 2: a-c-d
+     \item Triangle 3: c-d-e
+ \end{itemize}
+ \begin{align*}
+      \varphi_{TC} \coloneqq &
+                       (e_{a = b} \land e_{b = c} \rightarrow e_{a = c}) \land \\
+                       & (e_{a = b} \land e_{a = c} \rightarrow e_{b = c}) \land \\
+                       & (e_{b = c} \land e_{a = c} \rightarrow e_{a = b}) \land \\
+                       &\\
+                       & (e_{a = c} \land e_{c = d} \rightarrow e_{a = d}) \land \\
+                       & (e_{a = c} \land e_{a = d} \rightarrow e_{c = d}) \land \\
+                       & (e_{c = d} \land e_{a = d} \rightarrow e_{a = c}) \land \\
+                       &\\
+                       & (e_{c = e} \land e_{c = d} \rightarrow e_{d = e}) \land \\
+                       & (e_{c = e} \land e_{d = e} \rightarrow e_{c = d}) \land \\
+                       & (e_{c = d} \land e_{d = e} \rightarrow e_{c = e}) 
+        \end{align*}
+    \begin{align*}
+      \hat\varphi_{E} \coloneqq
+                          (e_{a=b} \; \lor \; e_{a=d} \imp (e_{b=c} \; \land \; \neg e_{c = e}\; \land \; \neg e_{e = d})
+    \end{align*}
+    \begin{align*}
+     \varphi_{prop} \coloneqq \varphi_{TC} \land \hat\varphi_{E} 
+    \end{align*}

smt/0015.tex

@@ -0,0 +1 @@
+\item Explain the concept of lazy encoding to decide satisfiability of formulas in a first-order theory.

smt/0015_sol.tex

@@ -0,0 +1,8 @@
+The propositional skeleton of $\varphi$ is given to a SAT
+solver. If a satisfying assignment is found, it is checked by a theory
+solver. If the assignment is consistent with the theory, $\varphi$ is $\mathcal{T}$-satisfiable.
+Otherwise, a blocking clause is generated and the SAT solver searches for
+a new assignment. This is repeated until either a $\mathcal{T}$-consistent assignment
+is found, or the SAT solver cannot find any more assignments.
+
+See figure in lecture notes on page 11.

smt/0016.tex

@@ -0,0 +1,5 @@
+\item \applyCC{
+    \begin{align*}
+         \varphi_{EUF} \quad := \quad  x=f(y) \wedge x \neq y \wedge y \neq u \wedge y = f(u) \wedge z \neq f(u) \wedge \\ u = v  \wedge v= z \wedge v = f(y) \wedge v \neq f(z) \wedge f(x) \neq f(z)
+    \end{align*}
+  }

smt/0016_sol.tex

@@ -0,0 +1,10 @@
+ \begin{align*}
+             &\{x,f(y)\},\{y,f(u)\},\{u,\underline{v}\}, \{\underline{v},z\},  \{\underline{v},f(y)\}, \{f(x)\}, \{f(z)\}\\\
+             &\{x,\underline{f(y)}\},\{y,f(u)\},\{u,v,z,v,\underline{f(y)}, \{f(x)\}, \{f(z)\}\}\\
+             &\{\underline{x},f(y),u,v,\underline{z},v\},\{y,f(u)\}, \{\underline{f(x)}\}, \{\underline{f(z)}\}\\
+            &\{x,f(y),\underline{u},v,\underline{z},v\},\{y,\underline{f(u)}\}, \{f(x),\underline{f(z)}\}\\
+            &\{x,f(y),u,v,z,v\},\{y,f(u)\}, \{f(x),f(z)\}
+\end{align*}
+
+Checking the disequality $f(x) \neq f(z)$ leads to the result that the assignment is UNSAT, since  $f(x)$ and $f(z)$
+are in the same congruence class.

smt/0017.tex

@@ -0,0 +1,2 @@
+\item Give the definition of the propsitional skeleton of a formula $\varphi$ in a given theory $\Theory$.
+Give an example for a formula $\varphi$ in $\LIA$ and its corresponding propositional skeleton $\skel$.

smt/0017_sol.tex

@@ -0,0 +1,9 @@
+The propositional skeleton $\skel$ of a formula $\varphi$ is obtained by replacing each occurance of a $\Theory$-literal with a propositional variable.
+
+An example for a formula $\varphi$ in $\LIA$:
+
+$$ \varphi \coloneqq (x > y) \lor (x > z),$$
+and the corresponding skeleton $\skel$:
+
+$$ e_1 \lor e_2, $$
+where $e_1 \equiv x > y$ and $e_2 \equiv x > z$.

smt/1001.tex

@@ -0,0 +1 @@
+\item Explain the concept of a theory in first-order logic using the theory of Linear Integer Arithmetic $\mathcal{T}_{LIA}$ as example.

smt/1002.tex

@@ -0,0 +1,8 @@
+\item \self In the following list tick all formulas that are axioms of the theory of equalities and uninterpreted functions $\mathcal{T}_{EUF}$.
+
+\begin{itemize}
+    \item[$\square$] $\forall x\, (x=x)$
+    \item[$\square$] $\forall x\, \forall y\, (x=y \lor y=x)$
+    \item[$\square$] $\forall x\, \forall y\, \forall z\, (x=y \land y=z \imp x=z)$
+    \item[$\square$] $\forall x\, \forall y\, (f(x)=f(y) \imp x=y)$
+\end{itemize}

smt/1003.tex

@@ -0,0 +1 @@
+\item \self A first-order theory $\mathcal{T}$ is defined by a signature $\Sigma$ and a set of axioms $\mathcal{A}$. Consider the \textit{Theory of Equality} $\mathcal{T}_E$. Give its signature $\Sigma_E$ and its axioms $\mathcal{A}_E$.

smt/1004.tex

@@ -0,0 +1,2 @@
+\item What is an uninterpreted function? What is the difference between an
+uninterpreted and an interpreted function? What are the properties of an uninterpreted function?

smt/1005.tex

@@ -0,0 +1,6 @@
+\item Considering formulas $\varphi$ and $\psi$ regarding a theory $\Theory$.
+\begin{itemize}
+    \item When is a formula $\varphi$ $\mathcal{T}$-valid?
+    \item When is a formula $\varphi$ $\mathcal{T}$-satisfiable?
+    \item When does $\varphi$ $\mathcal{T}$-entail $\psi$?
+\end{itemize}

smt/1006.tex

@@ -0,0 +1,8 @@
+\item \self In the following list tick all statements that conform to the eager encoding approach for the implementation of SMT solver.
+
+\begin{itemize}
+    \item[$\square$] Eager encoding is based on the interaction between a SAT solver and a so-called theory solver.
+    \item[$\square$] Eager encoding involves translating the original formula to an equisatisfiable boolean formula in a single step.
+    \item[$\square$] Eager encoding is based on the direct encoding of axioms.
+    \item[$\square$] Eager encoding starts with no constraints at all and adds constraints only when needed.
+\end{itemize}

smt/1007.tex

@@ -0,0 +1,5 @@
+\item \self 
+\begin{itemize}
+    \item Explain the concept of \textit{Eager Encoding} to decide satisfiability of formulas in a first-order theory.
+    \item Explain how eager encoding works on the \textit{Theory of Equality} $\mathcal{T}_{E}$.
+\end{itemize} 

smt/1008.tex

@@ -0,0 +1,6 @@
+\item \self In the following text fill the blanks with the missing word(s).
+
+The Ackermann's reduction is used to reduce a formula $\phi_{in}$ in \rule{4cm}{.4pt} \rule{6cm}{.4pt} to a formula in \rule{5.5cm}{.4pt} \rule{4.5cm}{.4pt} that is equisatisfiable. Two formulas are equisatisfiable if \rule{10cm}{.4pt}.
+The algorithm adds explicit constraints to the formula $\phi_{in}$ to enforce \rule{7cm}{.4pt}. These constraints say, that $\forall \bar{x} \forall \bar{y} \; (\bigwedge_i x_i = y_i) \imp $ \rule{2.5cm}{.4pt} $ ) $.
+The resulting equisatisfiable formula consists of two parts and is of the form: $\phi_{out}  := \phi_C \wedge \hat{\phi_{in}}$.
+The right part of the formula $\hat{\phi_{in}}$ describes the flattening original formula in which we replace \rule{7cm}{.4pt} with \rule{5.5cm}{.4pt}.

smt/1009.tex

@@ -0,0 +1,3 @@
+\item \applyAckermann{
+    $$\phi_{EUF} \quad := \quad f(x,y)=g(x) \imp \left[f(g(y),z)=x \lor \lnot(g(z)=y)\right].$$
+}

smt/1010.tex

@@ -0,0 +1,5 @@
+\item \ifassignmentsheet \points{2} \fi \applyAckermann{
+    \begin{equation*}
+        \phi_{EUF} \quad := \quad f(g(x), h(y))=a \; \lor \; b=f(u, v) \; \imp \; k(a,b)=u \land v=k(x,y)
+    \end{equation*}
+  }

smt/1011.tex

@@ -0,0 +1 @@
+\item When applying eager encoding to decide the satisfiability of a formula in $\EUF$, explain how reflexivity, symmetry and transitivity are handled within the graph-based reduction.

smt/1012.tex

@@ -0,0 +1,9 @@
+\item \self In the following text fill the blanks with the missing word(s).
+
+The Graph Based Reduction is used to reduce a formula $\phi_{in}$ in \rule{4.5cm}{.4pt} \rule{5.5cm}{.4pt} to a formula in \rule{6cm}{.4pt} \rule{4cm}{.4pt} that is equisatisfiable.
+Two formulas are equisatisfiable if \rule{1cm}{.4pt} \rule{11cm}{.4pt}.
+In the first step of the algorithm, we create a Non-Polar Equality Graph and in the next step we make it chordal. The graph is chordal, if \rule{8.5cm}{.4pt} \rule{3.5cm}{.4pt}. 
+We introduce fresh propositional variables for each equation to ensure \rule{4cm}{.4pt}. 
+In order to ensure transitivity, the algorithm adds constraints of the form \rule{11cm}{.4pt} for all \rule{7cm}{.4pt} in the graph.
+The resulting equisatisfiable formula consists of two parts and is of the form: $\phi_{out}  := \phi_{TC} $ \rule{0.5cm}{.4pt} $\hat{\phi_{in}}$.
+The right part of the formula $\hat{\phi_{in}}$ describes the flattening original formula in which we replace \rule{4cm}{.4pt} with \rule{6cm}{.4pt}.

smt/1013.tex

@@ -0,0 +1,8 @@
+\item \self Consider the following formula from $\mathcal{T}_{E}$.
+    \begin{equation*}
+        \phi_{EUF}  :=    \big[ f_y = g_x \land f_y = y \big] \lor \big[ f_y = f_x \land y \neq f_{gy} \big] \lor \big[ f_x = f_y \land f_y = y \big] \lor \big[ f_x = f_{gy} \land f_y \neq y \big]
+    \end{equation*}
+    
+    Use the graph-based algorithm to construct an equisatisfiable propositional formula $\phi_{prop}$.
+
+    What would you have to change if you would want to check $\phi_E$ for \textit{validity} instead of satisfiability?

smt/1014.tex

@@ -0,0 +1,5 @@
+\item \ifassignmentsheet \points{2} \fi \applyGB{
+    \begin{equation*}
+        \phi_{EUF} \quad := \quad  x \neq y \land y = g_x \lor g_x = g_y \rightarrow \neg (g_y \neq z \lor z = f_x) \land \neg (f_x = f_y \land x \neq z)
+    \end{equation*}
+  }

smt/1015.tex

@@ -0,0 +1,5 @@
+\item \applyEagerEUF{
+    \begin{align*}
+       \phi_{EUF} \quad := \quad  f(x)=f(y) \land f(y)=y \lor f(g(x))=f(f(y)) \land g(x)=x \\ \lor f(x) \neq f(y) \land y \neq g(f(y)) \land x \neq g(x)
+    \end{align*}
+  }

smt/1016.tex

@@ -0,0 +1,9 @@
+\item \self In the following list tick all statements that conform to the lazy encoding approach
+for the implementation of SMT solver.
+
+\begin{itemize}
+    \item[$\square$] Lazy encoding is based on the interaction between a SAT solver and a so-called theory solver.
+    \item[$\square$] Lazy encoding involves translating the original formula to an equisatisfiable Boolean formula in a single step.
+    \item[$\square$] Lazy encoding is based on the direct encoding of axioms.
+    \item[$\square$] Lazy encoding starts with no constraints at all and adds constraints only when needed.
+\end{itemize}

smt/1018.tex

@@ -0,0 +1,4 @@
+\item \self 
+To decide SMT formulas, the lazy approach uses a theory solver in combination with a SAT solver.
+Explain what a theory solver is. Explain what the inputs and outputs of a theory solver are and how it is used within the lazy encoding approach.
+

smt/1019.tex

@@ -0,0 +1,3 @@
+\item \self In the following text fill the blanks with the missing word(s).
+
+One way to solve \textit{Satisfiability} \rule{3cm}{0.15mm} \textit{Theories} problems works as follows. First, the propositional skeleton of the formula in question is given to a \rule{1.5cm}{0.15mm} solver. If this solver returns \rule{2.5cm}{0.15mm}, we terminate with answer \rule{2.5cm}{0.15mm}. In the other case, the solver returns a \rule{5cm}{0.15mm}, which is a \rule{3.5cm}{0.15mm} of theory literals. This can be given to a \rule{3cm}{0.15mm} solver that can decide the \rule{3cm}{0.15mm} fragment of the theory in question. If this solver returns \rule{2.5cm}{0.15mm}, we terminate with answer \rule{3.5cm}{0.15mm}. Otherwise, we add a \rule{2.5cm}{0.15mm} \rule{2.5cm}{0.15mm} to the propositional skeleton, to prevent the same \rule{4cm}{0.15mm} from occurring again, and run the \rule{1.5cm}{0.15mm} solver on the augmented propositional skeleton. This loop is repeated until either the \rule{1.5cm}{0.15mm} solver returns \rule{3.5cm}{0.15mm} (in which case the answer is \rule{3.5cm}{0.15mm}), or the \rule{3cm}{0.15mm} solver returns \rule{3.5cm}{0.15mm} (in which case the answer is \rule{3cm}{0.15mm}). This entire procedure is called \rule{2cm}{0.15mm} encoding.

smt/1020.tex

@@ -0,0 +1,8 @@
+\item \self In the following list, mark all items that are true for an \textit{eager encoding} procedure for $\mathcal{T}_{UE}$ with \textbf{E}, mark all items that are true for a \textit{lazy encoding} procedure with \textbf{L}, and mark all items which neither belong to an eager nor a lazy encoding procedure with \textbf{N}.
+
+\begin{itemize}
+    \item[\Huge{$\square$}] Only one call to a propositional SAT solver is required.
+    \item[\Huge{$\square$}] A propositional formula that is equisatisfiable to the original theory formula is constructed before calling any solver.
+    \item[\Huge{$\square$}] A propositional SAT solver and a theory solver for the conjunctive fragment of the theory interact with each other.
+    \item[\Huge{$\square$}] For a theory-inconsistent assignment of literals, a blocking clause is created.
+\end{itemize}

smt/1021.tex

@@ -0,0 +1,5 @@
+
+\item \applyCC{
+$$\varphi_{EUF} \quad := \quad x=y \land y=f(y) \land y \neq f(x) \land z=f(z) \land f(z)=f(x) \land z=f(y)$$
+}
+

smt/1022.tex

@@ -0,0 +1,3 @@
+\item What does the congruence closure algorithm compute? State the inputs and output of the algorithm.
+
+In the context of deciding satisfiability of formulas in $\EUF$, what is the congruence closure algorithm used for?

smt/1023.tex

@@ -0,0 +1,5 @@
+\item \applyCC{
+    \begin{align*}
+        \varphi_{EUF} \quad := \quad f(a) = c \land f(c) \neq f(d) \land b = f(c) \land a \neq f(c) \land c = d \land b \neq d \land a = c
+    \end{align*}
+  }

smt/1024.tex

@@ -0,0 +1,5 @@
+\item \applyCC{
+    \begin{align*}
+        \varphi_{EUF} \quad := \quad a = b \land c \neq d \land f(a) = c \land f(b) \neq f(c) \land f(a) = f(d) \land f(b) = c \land f(d) = f(c)
+    \end{align*}
+  }

smt/1025.tex

@@ -0,0 +1,6 @@
+\item \applyCC{
+    \begin{align*}
+        f(b) = a \land c \neq d \land f(e) = b \land d \neq f(b) \land f(a) = f(e) \; \land \\
+         b \neq f(b) \land a \neq e \land f(a) = e \land a = c \land f(b) \neq e \land d = f(c)
+    \end{align*}
+  }

smt/1026.tex

@@ -0,0 +1,7 @@
+\item \applyAckermann{
+    \begin{equation*}
+    \varphi_{EUF}  :=   f(x)=y \land x=g(x) \lor \\
+    x \neq f(x) \land g(x)=f(g(x)) \lor \\
+    y \neq g(x) \land x=f(y) \land g(y)=f(g(x))
+    \end{equation*}
+  }

smt/1027.tex

@@ -0,0 +1,5 @@
+\item \applyAckermann{
+    \begin{equation*} \varphi_{EUF} \quad := \quad  x=f(x,y) \land x \neq y \leftrightarrow z=f(x,y) \lor \\
+    f(y,z) \neq z \land y \neq f(x,y) \lor y=f(x,z)
+    \end{equation*}
+  }

smt/1028.tex

@@ -0,0 +1,5 @@
+\item \applyGB{
+    \begin{equation*}
+        \varphi_{E}  :=   x \neq y \land y = c \lor c = d \rightarrow \neg (d \neq z \lor z = a) \land \neg (a = b \land x \neq z).
+    \end{equation*}
+  }

smt/1029.tex

@@ -0,0 +1,5 @@
+\item \applyEagerEUF{
+    \begin{equation*}
+           \varphi_{EUF} \quad := (y = z \lor f(x) = f(y)) \imp ( x = z \vee f(x) = x \wedge f(x) = y)
+    \end{equation*}
+  }

smt/1030.tex

@@ -0,0 +1,4 @@
+\item \applyCC{
+$$\varphi_{EUF} \quad := \quad f(b)=a \land e=b \land c=f(c) \land d \neq f(e)
+\land f(a)=f(d) \land a \neq f(c) \land d=f(a)$$
+}

smt/1031.tex

@@ -0,0 +1,5 @@
+\item \applyCC{
+    \begin{align*}
+         \varphi_{EUF} \quad := \quad  f(o)=k \land l \neq f(m) \land n \neq l \land f(k)=m \land f(o)=f(k) \land o \neq k \land \\ l \neq f(n) \land f(m) \neq k \land m \neq f(m) \land o=n \land f(m)=o
+    \end{align*}
+  }

smt/1032.tex

@@ -0,0 +1,4 @@
+\item \ifassignmentsheet \points{2} \fi \applyCC{
+$$\varphi_{EUF} \quad := \quad f(b)=a \land e=b \land c=f(c) \land d \neq f(e)
+\land f(a)=f(d) \land a \neq f(c) \land d=f(a)$$
+}

smt/1032_sol.tex

@@ -0,0 +1,8 @@
+\begin{align*}
+    & \{f(b),a\}, \{e,b\}, \{c,f(c)\}, \{f(e)\}, \{\underline{f(a)},f(d)\}, \{d,\underline{f(a)}\} \\
+    & \{\underline{f(b)},a\}, \{\underline{e,b}\}, \{c,f(c)\}, \{\underline{f(e)}\}, \{f(a),f(d),d\} \\
+    & \{f(b),a,f(e)\}, \{e,b\}, \{c,f(c)\}, \{f(a),f(d),d\} 
+\end{align*}
+
+Checking the disequalities $d \neq f(e)$ and $a \neq f(c)$ leads to the result that the assignment is SAT, since neither $d$ and $f(e)$ nor $a$ and $f(c)$
+are in the same congruence class.

smt/1033.tex

@@ -0,0 +1,5 @@
+\item \applyCC{
+    \begin{align*}
+         \varphi_{EUF} \quad := \quad  f(o)=k \land l \neq f(m) \land n \neq l \land f(k)=m \land f(o)=f(k) \land o \neq k \land \\ l \neq f(n) \land f(m) \neq k \land m \neq f(m) \land o=n \land f(m)=o
+    \end{align*}
+  }

smt/1033_sol.tex

@@ -0,0 +1,11 @@
+\begin{align*}
+    & \{k,\underline{f(o)}\}, \{l\}, \{m,f(k)\}, \{f(k),\underline{f(o)}\}, \{f(n)\}, \{n,o\}, \{o,f(m)\} \\
+    & \{k,f(k),f(o)\}, \{l\}, \{m,f(k)\}, \{f(n)\}, \{n,\underline{o}\}, \{\underline{o},f(m)\} \\
+    & \{k,\underline{f(k)},f(o)\}, \{l\}, \{m,\underline{f(k)}\}, \{f(n)\}, \{n,o,f(m)\} \\
+    & \{k,m,f(k),\underline{f(o)}\}, \{l\}, \{\underline{f(n)}\}, \{\underline{n,o},f(m)\} \\
+    & \{\underline{k,m},\underline{f(k)},f(n),f(o)\}, \{l\}, \{n,o,\underline{f(m)}\} \\
+    & \{k,m,n,o,f(k),f(m),f(n),f(o)\}, \{l\} \\
+\end{align*}
+
+Checking the disequalities $o \neq k$, $f(m) \neq k$, $m \neq f(m)$ leads to the result that the assignment is UNSAT, since $o$ and $k$, $f(m)$ and $k$, $m$ and $f(m)$
+are in the same congruence class.

smt/2001.tex

@@ -0,0 +1,3 @@
+\item \ifassignmentsheet \points{2} \fi \applyAckermann{
+        $$f(x)=g(x) \lor z=f(y) \imp f(z) \neq g(y) \land x=z$$
+}

smt/2002.tex

@@ -0,0 +1,7 @@
+\item \applyAckermann{
+    \begin{equation*}
+    \varphi_{EUF}  :=   f(x)=y \land x=g(x) \lor \\
+    x \neq f(x) \land g(x)=f(g(x)) \lor \\
+    y \neq g(x) \land x=f(y) \land g(y)=f(g(x))
+    \end{equation*}
+  }

smt/2002_sol.tex

@@ -0,0 +1,13 @@
+\begin{align*}
+  \hat{\varphi}_{EUF} \quad := \quad f_x=y \land x = g_x \lor x \neq f_x \land g_x = f_{g_x} \lor y \neq g_x \land x = f_y \land g_y = f_{g_x}
+\end{align*}
+
+\begin{align*}
+     \varphi_{FC} \quad := \quad & (x=y \rightarrow g_x = g_y)~\land \\
+                                 & (x=y \rightarrow f_x = f_y)~\land \\
+                                 & (x=g_x \rightarrow f_x = f_{g_x})~\land \\
+                                 & (y=g_x \rightarrow f_y = f_{g_x})
+\end{align*}
+\begin{align*}
+     \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
+\end{align*}

smt/2003.tex

@@ -0,0 +1,3 @@
+\item \ifassignmentsheet \points{2} \fi \applyGB{
+ $$a\neq b \land b=c \lor c=d \implies \neg(d\neq e \lor e=f) \land \neg(f=g \land a\neq e)$$
+}

smt/2003_sol.tex

@@ -0,0 +1,36 @@
+\begin{center}
+  \begin{egraph}
+    \node[base node] (a)                    {$a$};
+    \node[base node] (b) [above right of=a] {$b$};
+    \node[base node] (c) [below right of=b] {$c$};
+    \node[base node] (d) [below of=c]       {$d$};
+    \node[base node] (e) [below left of=d]  {$e$};
+    \node[base node] (f) [left of=e]        {$f$};
+    \node[base node] (g) [above left of=f]  {$g$};
+    \path[]
+        (a) edge [] node {} (b)
+        (b) edge [] node {} (c)
+        (c) edge [] node {} (d)
+        (d) edge [] node {} (e)
+        (e) edge [] node {} (a)
+        (f) edge [] node {} (e)
+        (g) edge [] node {} (f);
+
+     \chord{b}{e};
+     \chord{c}{e};
+  \end{egraph}
+\end{center}
+
+\begin{align*}
+  \varphi_{TC} =~\egraphFuncConstraint{a}{b}{e}~\land\\[0.75ex]
+                 \egraphFuncConstraint{b}{c}{e}~\land\\[0.75ex]
+                 \egraphFuncConstraint{c}{d}{e}
+\end{align*}
+
+\begin{align*}
+  \hat\varphi_{E} \coloneqq
+      \lnot e_{a=b} \land e_{b=c} \lor e_{c=d} \imp \lnot (\lnot e_{d=e} \lor e_{e=f}) \land \lnot(e_{f=g} \land \lnot e_{a=e})
+\end{align*}
+\begin{align*}
+ \varphi_{prop} \coloneqq \varphi_{TC} \land \hat\varphi_{E}
+\end{align*}

smt/2004.tex

@@ -0,0 +1,3 @@
+\item \ifassignmentsheet \points{2} \fi \applyAckermann{
+$$ \varphi_{EUF} := f(a,b)=x \land f(x,y)\neq g(a) \lor f(m,n)=b \lor f(g(a),y) \neq a$$
+}

smt/2004_sol.tex

@@ -0,0 +1,15 @@
+\begin{align*}
+  \hat{\varphi}_{EUF} \quad := \quad f_{ab} = x \land f_{xy} \neq g_a \lor f_{mn} = b \lor f_{g_{a}y} \neq a
+\end{align*}
+
+\begin{align*}
+     \varphi_{FC} \quad := \quad & (a=m  \land b=n \rightarrow f_{ab} = f_{mn}) \land \\
+                                 & (a=x  \land b=y \rightarrow f_{ab} = f_{xy}) \land \\
+                                 & (a=g_a\land b=y \rightarrow f_{ab} = f_{g_{a}y}) \land \\
+                                 & (m=g_a\land y=n \rightarrow f_{mn} = f_{g_{a}y}) \land \\
+                                 & (m=x  \land y=n \rightarrow f_{xy} = f_{mn}) \land \\
+                                 & (x=g_a\land y=y \rightarrow f_{xy} = f_{g_{a}y})
+\end{align*}
+\begin{align*}
+     \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
+\end{align*}

smt/3000.tex

@@ -0,0 +1,3 @@
+\item \ifassignmentsheet \points{5} \fi
+  Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  $$\varphi := (x = y) \land (y = f(y)) \land (y \neq f(x)) \land (z = f(z)) \land (f(z) = f(x)) $$

smt/3000_sol.tex

@@ -0,0 +1,35 @@
+We start by computing $\skel$:
+\begin{compactItemize}
+	\item $e_{0}\Leftrightarrow(x=y)$
+	\item $e_{1}\Leftrightarrow(y=f(y))$
+	\item $e_{2}\Leftrightarrow(y=f(x))$
+	\item $e_{3}\Leftrightarrow(z=f(z))$
+	\item $e_{4}\Leftrightarrow(f(z)=f(x))$
+\end{compactItemize}
+
+
+$$ \skel = e_{0} \land e_{1} \land \neg e_{2} \land e_{3} \land e_{4}$$
+
+\hspace{-0.09cm}\scalebox{0.85}{
+	\begin{dplltabular}{6}
+		\dpllStep{1|2|3|4|5|6}
+		\dpllDecL{0|0|0|0|0|0}
+		\dpllAssi{ - |$e_{0}$|$e_{0}, e_{1}$|$e_{0}, e_{1}, \lnot e_{2}$|\makecell{$e_{0}, e_{1}, \lnot e_{2}, $ \\ $e_{3}$}|\makecell{$e_{0}, e_{1}, \lnot e_{2}, $ \\ $e_{3}, e_{4}$}}
+		\dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done|\done}
+		\dpllClause{2}{$e_{1}$}{$e_{1}$|$e_{1}$|\done|\done|\done|\done}
+		\dpllClause{3}{$\lnot e_{2}$}{$\lnot e_{2}$|$\lnot e_{2}$|$\lnot e_{2}$|\done|\done|\done}
+		\dpllClause{4}{$e_{3}$}{$e_{3}$|$e_{3}$|$e_{3}$|$e_{3}$|\done|\done}
+		\dpllClause{5}{$e_{4}$}{$e_{4}$|$e_{4}$|$e_{4}$|$e_{4}$|$e_{4}$|\done}
+		\dpllBCP{$e_{0}$|$e_{1}$|$\lnot e_{2}$|$e_{3}$|$e_{4}$| - }
+		\dpllPL{ - | - | - | - | - | - }
+		\dpllDeci{ - | - | - | - | - |SAT}
+	\end{dplltabular}
+}
+
+\vspace{0.5em}
+The SAT solver has computed that $\skel$ is satisfiable, we are therefore going to check for consistency with the theory:
+\begin{align*}
+	&\{x, y\}, \{y, f(y)\}, \{z, f(z)\}, \{f(z), f(x)\}\\
+	&\{f(y), x, y\}, \{f(x), f(z), z\}
+\end{align*}
+The $\EUF$-Solver returned SAT, therefore $\varphi$ is satisfiable.

smt/3001.tex

@@ -0,0 +1,2 @@
+\item Use the lazy encoding approach to check whether the formula $\varphi$ in $\EUF$ is satisfiable.
+  $$\varphi := (g(a) = c) \land \big( (f(g(a)) \neq f(c)) \lor (g(a) = d)) \big) \land (c \neq d) $$

smt/3001_sol.tex

@@ -0,0 +1,171 @@
+  We start by computing $\skel$:
+  \begin{compactItemize}
+  	\item $e_{0}\Leftrightarrow(g(a)=c)$
+  	\item $e_{1}\Leftrightarrow(f(g(a))=f(c))$
+  	\item $e_{2}\Leftrightarrow(g(a)=d)$
+  	\item $e_{3}\Leftrightarrow(c=d)$
+  \end{compactItemize}
+  $$ \skel = e_{0} \land \neg e_{1} \land e_{2} \land \neg e_{3} $$
+
+
+  \hspace{-0.09cm}\scalebox{0.85}{
+  	\begin{dplltabular}{4}
+  		\dpllStep{1|2|3|4}
+  		\dpllDecL{0|0|0|0}
+  		\dpllAssi{ - |$e_{0}$|$e_{0}, \lnot e_{3}$|$e_{0}, \lnot e_{3}, \lnot e_{1}$}
+  		\dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done}
+  		\dpllClause{2}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|\done}
+  		\dpllClause{3}{$\lnot e_{3}$}{$\lnot e_{3}$|$\lnot e_{3}$|\done|\done}
+  		\dpllBCP{$e_{0}$|$\lnot e_{3}$| - | - }
+  		\dpllPL{ - | - |$\lnot e_{1}$| - }
+  		\dpllDeci{ - | - | - | - }
+  	\end{dplltabular}
+  }
+
+  A satisfying assignment $e_0 \land \neg e_1 \land \neg e_3$ has been found and
+  we have to check consistency of $(g(a) = c) \land (f(g(a)) \neq f(c)) \land (c \neq d) $:
+
+  \begin{align*}
+  	&\{g(a), c\}, \{f(g(a))\}, \{f(c)\}, \{d\}\\
+  	&\{g(a), c\}, \{d\}, \{f(c), f(g(a))\}
+  \end{align*}
+
+  Congruence Closure returns UNSAT because of: $(f(g(a)) \neq f(c)) $.
+  We therefore add $\neg e_0 \lor e_1 \lor e_3$ as a blocking clause and continue.
+  \hspace{-0.09cm}\scalebox{0.85}{
+  	\begin{dplltabular}{5}
+  		\dpllStep{5|6|7|8|9}
+  		\dpllDecL{0|0|0|0|0}
+  		\dpllAssi{ - |$e_{0}$|$e_{0}, \lnot e_{3}$|$e_{0}, \lnot e_{3}, e_{1}$|\makecell{$e_{0}, \lnot e_{3}, e_{1}, $ \\ $e_{2}$}}
+  		\dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done}
+  		\dpllClause{2}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\done}
+  		\dpllClause{3}{$\lnot e_{3}$}{$\lnot e_{3}$|$\lnot e_{3}$|\done|\done|\done}
+  		\dpllClause{4}{$\lnot e_{0}, e_{3}, e_{1}$}{$\lnot e_{0}, e_{3}, e_{1}$|$e_{3}, e_{1}$|$e_{1}$|\done|\done}
+  		\dpllBCP{$e_{0}$|$\lnot e_{3}$|$e_{1}$|$e_{2}$| - }
+  		\dpllPL{ - | - | - | - | - }
+  		\dpllDeci{ - | - | - | - | - }
+  	\end{dplltabular}
+  }
+
+  We have to check consistency for $(g(a) = c) \land (f(g(a)) = f(c)) \land (g(a) = d) \land (c \neq d) $:
+
+  \begin{align*}
+  	&\{g(a), c\}, \{f(g(a)), f(c)\}, \{g(a), d\}\\
+  	&\{f(g(a)), f(c)\}, \{c, d, g(a)\}
+  \end{align*}
+
+  Congruence Closure returns UNSAT  because of: $(c \neq d) $\\
+  We therefore add $\neg e_0 \lor e_3 \lor \neg e_1 \lor \neg e_2$ as a blocking clause and continue.
+  \hspace{-0.09cm}\scalebox{0.80}{
+  	\begin{dplltabular}{5}
+  		\dpllStep{10|11|12|13|14}
+  		\dpllDecL{0|0|0|0|0}
+  		\dpllAssi{ - |$e_{0}$|$e_{0}, \lnot e_{3}$|$e_{0}, \lnot e_{3}, e_{1}$|\makecell{$e_{0}, \lnot e_{3}, e_{1}, $ \\ $\lnot e_{2}$}}
+  		\dpllClause{1}{$e_{0}$}{$e_{0}$|\done|\done|\done|\done}
+  		\dpllClause{2}{$\lnot e_{1}, e_{2}$}{$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$\lnot e_{1}, e_{2}$|$e_{2}$|\conflict}
+  		\dpllClause{3}{$\lnot e_{3}$}{$\lnot e_{3}$|$\lnot e_{3}$|\done|\done|\done}
+  		\dpllClause{4}{$\lnot e_{0}, e_{3}, e_{1}$}{$\lnot e_{0}, e_{3}, e_{1}$|$e_{3}, e_{1}$|$e_{1}$|\done|\done}
+  		\dpllClause{5}{$\lnot e_{0}, e_{3}, \lnot e_{1}, \lnot e_{2}$}{\makecell{$\lnot e_{0}, e_{3}, \lnot e_{1}, $ \\ $\lnot e_{2}$}|$e_{3}, \lnot e_{1}, \lnot e_{2}$|$\lnot e_{1}, \lnot e_{2}$|$\lnot e_{2}$|\done}
+  		\dpllBCP{$e_{0}$|$\lnot e_{3}$|$e_{1}$|$\lnot e_{2}$| - }
+  		\dpllPL{ - | - | - | - | - }
+  		\dpllDeci{ - | - | - | - |UNSAT}
+  	\end{dplltabular}
+  }
+
+  Conflict in step 14\\
+  \scalebox{0.75}{
+
+  \begin{tikzpicture}[>=latex,line join=bevel,]
+    \pgfsetlinewidth{1bp}
+  %%
+  \pgfsetcolor{black}
+    % Edge: 0 -> 2
+    \draw [->] (1.0882bp,62.277bp) .. controls (1.964bp,62.779bp) and (9.2748bp,62.662bp)  .. (19.0bp,62.429bp) .. controls (30.239bp,62.537bp) and (43.981bp,61.976bp)  .. (65.01bp,63.663bp);
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (33.0bp,70.929bp) node {$$1$$};
+    % Edge: 0 -> 4
+    \draw [->] (1.0536bp,100.444bp) .. controls (2.5288bp,100.842bp) and (34.108bp,100.377bp)  .. (65.302bp,102.81bp);
+    \draw (33.0bp,107.93bp) node {$$3$$};
+    % Edge: 2 -> 5
+    \draw [->] (84.139bp,57.437bp) .. controls (89.42bp,51.96bp) and (97.049bp,44.903bp)  .. (105.0bp,40.429bp) .. controls (117.15bp,33.594bp) and (132.19bp,29.057bp)  .. (153.87bp,24.136bp);
+    \draw (119.0bp,47.929bp) node {$$4$$};
+    % Edge: 2 -> 6
+    \draw [->] (87.223bp,65.255bp) .. controls (115.41bp,64.774bp) and (194.66bp,63.424bp)  .. (242.75bp,62.604bp);
+    \draw (165.0bp,70.929bp) node {$$5$$};
+    % Edge: 3 -> 1
+    \draw [->] (264.67bp,18.652bp) .. controls (272.24bp,21.175bp) and (283.02bp,24.768bp)  .. (302.09bp,31.126bp);
+    % Edge: 4 -> 5
+    \draw [->] (85.379bp,99.325bp) .. controls (96.698bp,90.91bp) and (117.27bp,75.011bp)  .. (133.0bp,59.429bp) .. controls (139.39bp,53.105bp) and (145.86bp,45.585bp)  .. (157.76bp,30.745bp);
+    \draw (119.0bp,89.929bp) node {$$4$$};
+    % Edge: 4 -> 6
+    \draw [->] (87.393bp,105.29bp) .. controls (98.691bp,105.0bp) and (117.24bp,104.11bp)  .. (133.0bp,101.43bp) .. controls (174.77bp,94.331bp) and (185.41bp,91.533bp)  .. (225.0bp,76.429bp) .. controls (228.25bp,75.189bp) and (231.62bp,73.694bp)  .. (243.87bp,67.569bp);
+    \draw (165.0bp,104.93bp) node {$$5$$};
+    % Edge: 5 -> 3
+    \draw [->] (173.78bp,15.592bp) .. controls (179.69bp,10.872bp) and (188.28bp,4.9991bp)  .. (197.0bp,2.4291bp) .. controls (208.94bp,-1.0874bp) and (212.85bp,-0.25425bp)  .. (225.0bp,2.4291bp) .. controls (228.24bp,3.1456bp) and (231.56bp,4.2776bp)  .. (244.02bp,10.039bp);
+    \draw (211.0bp,9.9291bp) node {$$2$$};
+    % Edge: 5 -> 6
+    \draw [->] (176.04bp,24.306bp) .. controls (188.14bp,26.832bp) and (208.86bp,32.005bp)  .. (225.0bp,40.429bp) .. controls (229.31bp,42.678bp) and (233.61bp,45.621bp)  .. (245.22bp,55.023bp);
+    \draw (211.0bp,47.929bp) node {$$5$$};
+    % Edge: 6 -> 1
+    \draw [->] (264.16bp,57.93bp) .. controls (272.09bp,54.035bp) and (283.8bp,48.281bp)  .. (302.68bp,39.01bp);
+    % Node: 2
+  \begin{scope}
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (76.0bp,65.43bp) ellipse (11.0bp and 11.0bp);
+    \draw (76.0bp,65.429bp) node {$e_{0}$};
+  \end{scope}
+    % Node: 4
+  \begin{scope}
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (76.0bp,105.43bp) ellipse (11.0bp and 11.0bp);
+    \draw (76.0bp,105.43bp) node {$\lnot e_{3}$};
+  \end{scope}
+    % Node: 1
+  \begin{scope}
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (313.0bp,34.43bp) ellipse (11.0bp and 11.0bp);
+    \draw (313.0bp,34.429bp) node {$\bot$};
+  \end{scope}
+    % Node: 5
+  \begin{scope}
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (165.0bp,22.43bp) ellipse (11.0bp and 11.0bp);
+    \draw (165.0bp,22.429bp) node {$e_{1}$};
+  \end{scope}
+    % Node: 6
+  \begin{scope}
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (254.0bp,62.43bp) ellipse (11.0bp and 11.0bp);
+    \draw (254.0bp,62.429bp) node {$\lnot e_{2}$};
+  \end{scope}
+    % Node: 3
+  \begin{scope}
+    \definecolor{strokecol}{rgb}{0.0,0.0,0.0};
+    \pgfsetstrokecolor{strokecol}
+    \draw (254.0bp,15.43bp) ellipse (11.0bp and 11.0bp);
+    \draw (254.0bp,15.429bp) node {$e_{2}$};
+  \end{scope}
+  %
+  \end{tikzpicture}
+
+
+  }
+  \begin{prooftree}
+  	\AxiomC{$2. \; \lnot e_{1} \lor e_{2}$}
+  	\AxiomC{$5. \; \lnot e_{0} \lor e_{3} \lor \lnot e_{1} \lor \lnot e_{2}$}
+  	\BinaryInfC{$\lnot e_{1} \lor \lnot e_{0} \lor e_{3}$}
+  	\AxiomC{$4. \; \lnot e_{0} \lor e_{3} \lor e_{1}$}
+  	\BinaryInfC{$\lnot e_{0} \lor e_{3}$}
+  	\AxiomC{$1. \; e_{0}$}
+  	\BinaryInfC{$e_{3}$}
+  	\AxiomC{$3. \; \lnot e_{3}$}
+  	\BinaryInfC{$\bot$}
+  \end{prooftree}
+
+  Since the SAT solver cannot find a satisfying assignment we are done and conclude that $\varphi$ is UNSAT.

smt/multiple_choice/1_1_smt_lect.tex

@@ -0,0 +1,8 @@
+\item \lect In the following list, tick all statements that correctly describe the meaning of the term \textit{Satisfiability Modulo Theories}.
+
+\begin{itemize}
+\item[$\square$] A formula is \textit{satisfiable modulo a theory} if all models that satisfy the axioms of the theory also satisfy the formula.
+\item[$\square$] \textit{Satisfiability Modulo Theories} refers to the fact that in sufficiently complex theories, some statements can neither be proven nor disproven. Thus, they are satisfiable, but not valid.
+\item[$\square$] \textit{Satisfiability Modulo Theories} means that for a consistent theory there always exists a model which satisfies all the axioms of the theory. Thus, the theory is \textit{satisfiable}.
+\item[$\square$] It is possible to find axioms that characterize the intuitive meaning of the arithmetic \textit{modulo} operator. The resulting \textit{theory} is \textit{satisfiable}.
+\end{itemize}

smt/multiple_choice/2_1_smt_lect.tex

@@ -0,0 +1,8 @@
+\item \lect Consider the \textit{Theory of Uninterpreted Functions and Equality} $\mathcal{T}_{EUF}$ and tick all statements below, that are correct.
+
+\begin{itemize}
+    \item[$\square$] $\mathcal{T}_{EUF}$ is decidable.
+    \item[$\square$] $\mathcal{T}_{EUF}$ is not decidable.
+    \item[$\square$] The quantifier-free fragment of $\mathcal{T}_{EUF}$ is not decidable.
+    \item[$\square$] The quantifier-free fragment of $\mathcal{T}_{EUF}$ is decidable.
+\end{itemize}

smt/multiple_choice/2_1_smt_self.tex

@@ -0,0 +1,7 @@
+\item \self Consider the \textit{Theory of Uninterpreted Functions and Equality} $\mathcal{T}_{EUF}$. and tick all items that are decidable in the following list.
+
+\begin{itemize}
+    \item[$\square$] Quantifier-free fragment of $\mathcal{T}_{EUF}$
+    \item[$\square$] Conjunctive fragment of $\mathcal{T}_{EUF}$
+    \item[$\square$] Full $\mathcal{T}_{EUF}$
+\end{itemize}

smt/multiple_choice/2_2_smt_self.tex

@@ -0,0 +1,8 @@
+\item \self In the following list tick all formulas that are axioms of the theory of equalities and uninterpreted functions $\mathcal{T}_{EUF}$.
+
+\begin{itemize}
+    \item[$\square$] $\forall x\, (x=x)$
+    \item[$\square$] $\forall x\, \forall y\, (x=y \lor y=x)$
+    \item[$\square$] $\forall x\, \forall y\, \forall z\, (x=y \land y=z \imp x=z)$
+    \item[$\square$] $\forall x\, \forall y\, (f(x)=f(y) \imp x=y)$
+\end{itemize}

smt/multiple_choice/3_1_a_smt_self.tex

@@ -0,0 +1,8 @@
+\item \self In the following list tick all statements that conform to the eager encoding approach for the implementation of SMT solver.
+
+\begin{itemize}
+    \item[$\square$] Eager encoding is based on the interaction between a SAT solver and a so-called theory solver.
+    \item[$\square$] Eager encoding involves translating the original formula to an equisatisfiable boolean formula in a single step.
+    \item[$\square$] Eager encoding is based on the direct encoding of axioms.
+    \item[$\square$] Eager encoding starts with no constraints at all and adds constraints only when needed.
+\end{itemize}

smt/multiple_choice/3_1_b_smt_self.tex

@@ -0,0 +1,9 @@
+\item \self In the following list tick all statements that conform to the lazy encoding approach
+for the implementation of SMT solver.
+
+\begin{itemize}
+    \item[$\square$] Lazy encoding is based on the interaction between a SAT solver and a so-called theory solver.
+    \item[$\square$] Lazy encoding involves translating the original formula to an equisatisfiable Boolean formula in a single step.
+    \item[$\square$] Lazy encoding is based on the direct encoding of axioms.
+    \item[$\square$] Lazy encoding starts with no constraints at all and adds constraints only when needed.
+\end{itemize}

smt/multiple_choice/3_1_smt_self.tex

@@ -0,0 +1,8 @@
+\item \self In the following list tick all statements that are \texttt{true}.
+
+\begin{itemize}
+    \item[$\square$] An edge between two non-adjacent nodes $n_1$ and $n_2$ within a graph $G$ is called a chord.
+    \item[$\square$] A graph is called chordal, if it contains no chord-free cycles with size greater than 2.
+    \item[$\square$] A cycle is said to be chord-free, if in the cycle there exist no non-adjacent nodes that are connected by an edge.
+    \item[$\square$] An edge between two non-adjacent nodes $n_1$ and $n_2$ within a graph $G$ is called a cycle.
+\end{itemize}

smt/multiple_choice/3_2_smt_lect.tex

@@ -0,0 +1,11 @@
+\item \lect 
+We have not yet discussed DPLL(T)? Kick this question?
+We want to decide whether or not a formula in $\mathcal{T}_{E}$ is satisfiable in the theory. To do so, we will transform $\phi_E$ into an equisatisfiable propositional formula $\phi_{prop}$ and then use a SAT solver on $\phi_{prop}$ to get the answer we seek. The name of this method is ...?
+
+\begin{itemize}
+    \item[$\square$] DPLL(T)
+    \item[$\square$] Lazy Encoding
+    \item[$\square$] Eager Encoding
+    \item[$\square$] Tseitin's Encoding
+    \item[$\square$] Ackermann's Reduction
+\end{itemize}

smt/multiple_choice/4_1_smt_self.tex

@@ -0,0 +1,9 @@
+\item \self Consider the \textit{Theory of Equality} $\mathcal{T}_{E}$. We want to decide whether or not a formula $\phi$ in $\mathcal{T}_{E}$ is satisfiable with respect to the theory. To do so, we will first use a SAT solver on the propositional skeleton of $\phi$. If the SAT solver returns a satisfying model, we use a theory solver for the conjunctive fragment of the theory to check whether the truth assignment to literals is consistent with the theory. If not, we add a blocking clause to the propositional skeleton and use the SAT solver again. This is repeated until either the SAT solver reports \textit{unsatisfiable}, or the theory solver reports an assignment to be consistent with the theory. The name of this method for checking satisfiability of theory formulas is ... ?
+
+\begin{itemize}
+    \item[$\square$] DPLL(T)
+    \item[$\square$] Lazy Encoding
+    \item[$\square$] Eager Encoding
+    \item[$\square$] Tseitin's Encoding
+    \item[$\square$] Ackermann's Reduction
+\end{itemize}

smt/multiple_choice/5_1_smt_lect.tex

@@ -0,0 +1,8 @@
+\item \lect Considering the \textit{Congruence Closure} algorithm, tick all items that are \texttt{true}
+
+\begin{itemize}
+\item[$\square$] In the last step, all equalities from the conjunction of literals are checked against the merged congruence classes.
+\item[$\square$] Classes are merged, if they contain common terms.
+\item[$\square$] All terms for which there is a negative equality in the conjunction of literals are put into the same congruence class. 
+\item[$\square$] Classes are merged, if two classes both contain an instance of the same uninterpreted function.
+\end{itemize}

smt/practical_questions/0_1_a_smt_prac.tex

@@ -0,0 +1,7 @@
+\item \prac \textbf{[3 Points]} Given the formula: 
+    \begin{equation*}
+    \varphi_{EUF}  :=   f(x)=y \land x=g(x) \lor \\
+    x \neq f(x) \land g(x)=f(g(x)) \lor \\
+    y \neq g(x) \land x=f(y) \land g(y)=f(g(x))
+    \end{equation*}
+Apply the \emph{Ackermann} reduction algorithm to compute an equisatisfiable formula in $\mathcal{T}_{E}$.

smt/practical_questions/0_1_smt_prac.tex

@@ -0,0 +1,6 @@
+
+\item \prac \textbf{[3 Points]} Given the formula: 
+    \begin{equation*} \varphi_{EUF} \quad := \quad  x=f(x,y) \land x \neq y \leftrightarrow z=f(x,y) \lor \\
+    f(y,z) \neq z \land y \neq f(x,y) \lor y=f(x,z)
+    \end{equation*}
+Apply the \emph{Ackermann} reduction algorithm to compute an equisatisfiable formula in $\mathcal{T}_{E}$.

smt/practical_questions/0_2_a_smt_prac.tex

@@ -0,0 +1,8 @@
+\item \prac \textbf{[5 Points]} Consider the following formula in $\mathcal{T}_{EUF}$:
+    \begin{equation*}
+           \varphi_{EUF} \quad := (y = z \lor f(x) = f(y)) \imp ( x = z \vee f(x) = x \wedge f(x) = y)
+    \end{equation*}
+        
+    Use Ackermann's reduction to compute an equisatisfiable formula in $\mathcal{T}_{E}$.
+    
+    Then perform the graph-based reduction on the outcome of Ackermann's reduction to construct an equisatisfiable propositional formula.

smt/practical_questions/0_2_smt_prac.tex

@@ -0,0 +1,12 @@
+
+\item \prac \textbf{[3 Points]} Perform graph-based reduction to translate the following formula in $\mathcal{T}_{E}$ into an
+ equisatisfiable formula in propositional logic.
+ 
+    \begin{equation*}
+        \varphi_{E}  :=   x \neq y \land y = c \lor c = d \rightarrow \neg (d \neq z \lor z = a) \land \neg (a = b \land x \neq z).
+    \end{equation*}
+    
+
+ 
+ 
+

smt/practical_questions/0_3_a_smt_prac.tex

@@ -0,0 +1,4 @@
+\item \prac \textbf{[3 Points]} Use the Congruence-Closure algorithm to check if the following assignment for the equalities is satisfiable.
+    \begin{align*}
+         \varphi_{EUF} \quad := \quad  f(o)=k \land l \neq f(m) \land n \neq l \land f(k)=m \land f(o)=f(k) \land o \neq k \land \\ l \neq f(n) \land f(m) \neq k \land m \neq f(m) \land o=n \land f(m)=o
+    \end{align*}

smt/practical_questions/0_3_smt_prac.tex

@@ -0,0 +1,3 @@
+\item \prac \textbf{[3 Points]} Use the Congruence-Closure algorithm to check if the following assignment for the equalities is satisfiable.
+$$\varphi_{EUF} \quad := \quad f(b)=a \land e=b \land c=f(c) \land d \neq f(e) 
+\land f(a)=f(d) \land a \neq f(c) \land d=f(a)$$

smt/practical_questions/3_0_smt_lect.tex

@@ -0,0 +1,6 @@
+\item \lect 
+Given the formula 
+    \begin{equation*}
+        \varphi_{EUF} \quad := \quad f(x)=f(y) \; \lor \; (z=y \land z \neq f(z))
+    \end{equation*}
+Apply the \emph{Ackermann} reduction algorithm to compute an equisatisfiable formula in $\mathcal{T}_{E}$.

smt/practical_questions/3_0_smt_lect_sol.tex

@@ -0,0 +1,11 @@
+    \begin{align*}
+         \varphi_{FC} \quad := \quad & (x=y \rightarrow f_{x} = f_y) \wedge \\
+         &(x=z \rightarrow f_{x} = f_z) \wedge \\
+         &(y=z \rightarrow f_y = f_z)
+    \end{align*}
+    \begin{align*}
+         \hat{\varphi}_{EUF} \quad := \quad f_{x}=f_y \; \lor \; (z=y \land z \neq f_z)
+    \end{align*}
+    \begin{align*}
+         \varphi_{E} \quad := \hat{\varphi}_{EUF} \wedge \varphi_{FC}
+    \end{align*}

smt/practical_questions/3_1_a_smt_lect.tex

@@ -0,0 +1,8 @@
+\item \lect 
+Perform the graph-based reduction on the following formula to compute an equsatisfiable formula in propositional logic.
+
+Given the formula 
+    \begin{equation*}
+        \varphi_{EUF} \quad := \quad f(x,y)=f(y,z) \; \lor \; (z=f(y,z) \land f(x,x) \neq f(x,y))
+    \end{equation*}
+Apply the \emph{Ackermann} reduction algorithm to compute an equisatisfiable formula in $\mathcal{T}_{E}$.