removed old questions

smt/multiple_choice/1_1_smt_lect.tex

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1,8 +0,0 @@
-\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}$.

smt/practical_questions/3_1_a_smt_lect_sol.tex

@@ -1,12 +0,0 @@
-    \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/practical_questions/3_1_smt_lect.tex

@@ -1,6 +0,0 @@
-\item \lect 
-Given the formula 
-    \begin{equation*}
-        \varphi_{EUF} \quad := \quad f(g(x))=f(y) \; \lor \; (z=g(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_1_smt_lect_sol.tex

@@ -1,12 +0,0 @@
-    \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/practical_questions/3_1_smt_self.tex

@@ -1,2 +0,0 @@
-\item \self For the following $\mathcal{T}_{EUF}$-formula, compute an equisatisfiable formula $\phi_{E}$ in the \textit{Theory of Equality} $\mathcal{T}_{E}$, by applying \textit{Ackermann's Reduction}.
-    $$\phi_{EUF} \quad := \quad f(x,y)=g(x) \imp \left[f(g(y),z)=x \lor \lnot(g(z)=y)\right].$$

smt/practical_questions/3_2_a_smt_lect.tex

@@ -1,6 +0,0 @@
-\item \lect Perform graph-based reduction to translate the following formula in $\mathcal{T}_{E}$ into an
- equisatisfiable formula in propositional logic.
-    \begin{equation*}
-        \phi_E \;\; := \;\; (a=b \; \lor \; a=d) \imp (b=c \; \land \; c \neq e \land \; e \neq d)
-    \end{equation*}
-    

smt/practical_questions/3_2_a_smt_lect_sol.tex

@@ -1,27 +0,0 @@
- 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/practical_questions/3_2_smt_lect.tex

@@ -1,6 +0,0 @@
-\item \lect Perform graph-based reduction to translate the following formula in $\mathcal{T}_{E}$ into an
- equisatisfiable formula in propositional logic.
-    \begin{equation*}
-        \phi_E \;\; := \;\; (a=b \; \lor \; a=d) \imp (b=c \; \land \; c \neq d)
-    \end{equation*}
-    

smt/practical_questions/3_2_smt_lect_sol.tex

@@ -1,22 +0,0 @@
- 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/practical_questions/3_2_smt_self.tex

@@ -1,7 +0,0 @@
-\item \self Consider the following formula in $\mathcal{T}_{EUF}$.
-    \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*}
-    
-    Use Ackermann's reduction to compute an equisatisfiable formula in $\mathcal{T}_{E}$.
-    

smt/practical_questions/3_3_smt_self.tex

@@ -1,8 +0,0 @@
-\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/practical_questions/3_4_smt_self.tex

@@ -1,6 +0,0 @@
-\item \self Consider the following formula from $\mathcal{T}_{E}$.
-    \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*}
-
-    Use the graph-based algorithm to construct an equisatisfiable propositional formula $\phi_{prop}$.

smt/practical_questions/3_5_smt_self.tex

@@ -1,8 +0,0 @@
-\item \self Consider the following formula in $\mathcal{T}_{EUF}$. 
-    \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}
-    
-    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 $\phi_{prop}$.

smt/practical_questions/5_1_smt_lect.tex

@@ -1,5 +0,0 @@
-\item \lect Consider the following formula in the conjunctive fragment of $\mathcal{T}_{EUF}$.
-    \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*}
-    Use the \textit{Congruence Closure} algorithm to determine whether this formula is satisfiable.

smt/practical_questions/5_1_smt_lect_sol.tex

@@ -1,10 +0,0 @@
- \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/practical_questions/5_1_smt_self.tex

@@ -1,5 +0,0 @@
-\item \self Consider the following formula in the conjunctive fragment of $\mathcal{T}_{EUF}$.
-    \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*}
-    Use the \textit{Congruence Closure} algorithm to determine whether this formula is satisfiable.

smt/practical_questions/5_2_smt_lect.tex

@@ -1,5 +0,0 @@
-
-\item \self Use the Congruence-Closure algorithm to check if the following assignment for the equalities is satisfiable.
-
-$\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/practical_questions/5_2_smt_self.tex

@@ -1,5 +0,0 @@
-\item \self Consider the following formula in the conjunctive fragment of $\mathcal{T}_{EUF}$.
-    \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*}
-    Use the \textit{Congruence Closure} algorithm to determine whether  this formula is satisfiable.

smt/practical_questions/5_3_smt_self.tex

@@ -1,6 +0,0 @@
-\item \self Consider the following formula in the conjunctive fragment of $\mathcal{T}_{EUF}$. Let $a \neq b$ be a shorthand notation for $\lnot(a=b)$.
-    \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*}
-    Use the \textit{Congruence Closure} algorithm to determine whether this formula is satisfiable.

smt/practical_questions/5_4_smt_self.tex

@@ -1,26 +0,0 @@
-\item \self Use lazy encoding to check if the following formula from $\mathcal{T}_{EUF}$ is satisfiable. Perform DPLL to obtain a \textbf{full assignment} for the equalities which you can then check with the \textbf{Congruence-Closure} algorithm. If you find a theory conflict, obtain a \textbf{blocking clause} from the Congruence-Closure algorithm, restart the DPLL algorithm at decision level $0$ with the new blocking clause added. For simplicity, do not use conflict-driven clause learning. I.e., the only clauses you are supposed to add are blocking clauses coming from Congruence Closure.
-
-In each step of the DPLL algorithm, first try to perform Boolean Constraint Propagation (BCP), if applicable, then try to set Pure Literals (if applicable). If neither BCP nor Pure Literals are applicable, make a decision. \textbf{When backtracking, always undo exactly one decision}. (Note that undoing one decision implies undoing all BCP- and Pure-Literal-based assignments that were done because of this decision.)
-
-  \textbf{Important:} 
-  \begin{itemize}
-    \item 
-      Always assign \emph{false} to the literal first, and \emph{true} second.
-    \item 
-      If you have to make a decision in DPLL, use the following order of literals to select a 
-      theory literal to assign a truth value to.
-        \begin{enumerate}
-          \item x = y
-          \item x = z
-          \item y = z
-          \item f(x) = f(y) 
-        \end{enumerate}
-  \end{itemize}
-  
-  Formula to check:
-  \begin{align*}
-    \mathcal{T}_{EUF} :=    & (x = y \lor f(x) = f(y))        ~\land \\
-                            & (x = y \lor f(x) \neq f(y))     ~\land \\
-                            & (x \neq y \lor  y = z)          ~\land \\
-                            & (x \neq z \lor y \neq z)  
-  \end{align*}

smt/theory_questions/1_0_smt_self.tex

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

smt/theory_questions/1_1_a_smt_lect.tex

@@ -1 +0,0 @@
-\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/theory_questions/1_1_a_smt_lect_sol.tex

@@ -1,10 +0,0 @@
-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 = \{ ... ..., -3,-2,-1,0,1,2,3...,=,+,-,\neq, <, >, \leq,\geq\} $
-\item $\mathcal{A}$ defines the usual meaning to all symbols. (Constant number symbols are mapped to the corresponding value in $\mathbb{Z}$,  $+$ is interpreted as the function $0+0\rightarrow 0$, $0+1\rightarrow 1$, etc.).
-\end{itemize}

smt/theory_questions/1_1_b_smt_lect.tex

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

smt/theory_questions/1_1_b_smt_lect_sol.tex

@@ -1,4 +0,0 @@
-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/theory_questions/1_1_c_smt_lect.tex

@@ -1,2 +0,0 @@
-
-\item \lect Explain the terms \emph{$\mathcal{T}$-terms}, \emph{$\mathcal{T}$-atoms} and \emph{$\mathcal{T}$-literals} for SMT formulas.

smt/theory_questions/1_1_c_smt_lect_sol.tex

@@ -1,6 +0,0 @@
-\begin{itemize}
-    \item \emph{Constants} in $\Sigma$, \emph{variables}, and
-    applications of function symbols in $\Sigma$ where all inputs are $\mathcal{T}$-terms are $\mathcal{T}$-terms.
-    \item A $\mathcal{T}$-atom is the application of a predicate symbol in $\Sigma$ where all inputs are $\mathcal{T}$-terms.
-    \item A $\mathcal{T}$-literal is a $\mathcal{T}$-atoms or its negation.
-\end{itemize}

smt/theory_questions/1_1_d_smt_lect.tex

@@ -1,2 +0,0 @@
-\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/theory_questions/1_1_d_smt_lect_sol.tex

@@ -1,4 +0,0 @@
-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/theory_questions/1_1_smt_lect.tex

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

smt/theory_questions/1_1_smt_lect_sol.tex

@@ -1,7 +0,0 @@
-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/theory_questions/1_1_smt_self.tex

@@ -1 +0,0 @@
-\item \self Explain what a \textit{Theory} in \textit{Predicate Logic} is and give an example of such a theory. For your example, provide all the details necessary to make it a theory in predicate logic.

smt/theory_questions/1_2_smt_lect.tex

@@ -1 +0,0 @@
-\item \lect In the context of \textit{Satisfiability Modulo Theories (SMT)}, give a definition of $\mathcal{T}$-satisfiability and $\mathcal{T}$-validity.

smt/theory_questions/1_2_smt_lect_sol.tex

@@ -1,6 +0,0 @@
-\textbf{$\mathcal{T}$-satisfiablility.} A \emph{formula $\varphi$ is satisfiable in a theory $\mathcal{T}$}, or $\mathcal{T}$-satisfiable, if and only if there is a
-model $\mathcal{M}$ within  $\mathcal{T}$ that satisfies $\varphi$ (i.e., $\mathcal{M} \models A$ for every $A \in \mathcal{A}$
-and $\mathcal{M} \models\varphi$).
-
-\textbf{$\mathcal{T}$-valid.} A \emph{formula $\varphi$ is valid in a theory $\mathcal{T}$}, or $\mathcal{T}$-valid, if and only if all
-models within  $\mathcal{T}$ satisfy $\varphi$.

smt/theory_questions/1_2_smt_self.tex

@@ -1 +0,0 @@
-\item \self Consider the following statement: \textit{Every model of $\mathcal{T}$ satisfies all formulas $\phi_1, ..., \phi_n$ and satisfies $\psi$ as well.} To which definition does this statement refer to?

smt/theory_questions/1_3_smt_self.tex

@@ -1 +0,0 @@
-\item \self A first-order theory, or a fragment of a first-order theory can either be decidable or not decidable. Give one example for each case.

smt/theory_questions/2_1_a_smt_self.tex

@@ -1,3 +0,0 @@
-\item \self 
-What is an \emph{uninterpreted function}? What is the difference between an 
-uninterpreted and an interpreted function? What are the properties of an uninterpreted function?

smt/theory_questions/2_1_b_smt_self.tex

@@ -1,6 +0,0 @@
-\item \self Provide the answers to the following questions:
-\begin{itemize}
-    \item When is a formula $\mathcal{T}$-valid?
-    \item When is a formula $\mathcal{T}$-satisfiable?
-    \item When do we have $\mathcal{T}$-entailment of two formulas?
-\end{itemize}

smt/theory_questions/2_1_smt_lect.tex

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

smt/theory_questions/2_1_smt_lect_sol.tex

@@ -1,9 +0,0 @@
-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/theory_questions/2_1_smt_self.tex

@@ -1 +0,0 @@
-\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/theory_questions/2_2_smt_lect.tex

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

smt/theory_questions/2_2_smt_lect_sol.tex

@@ -1,10 +0,0 @@
-\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/theory_questions/3_1_smt_lect.tex

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

smt/theory_questions/3_1_smt_lect_sol.tex

@@ -1,13 +0,0 @@
-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. 
-
-Given a formula $\varphi$, algorithms based on eager encoding operate in three steps:
-\begin{enumerate}
-\item Replace any unique $\mathcal{T}$-atom in the original formula $\varphi$ with
-a fresh Boolean variable to get a Boolean formula $\hat{\varphi}$.
-\item Generate a Boolean formula $\varphi_{cons}$ that constrains the values of the introduced
-Boolean variables to preserve the information of the theory.
-\item Invoke a SAT solver on the Boolean formula $\varphi_{prop} \coloneqq \hat{\varphi} \wedge \varphi_{cons}$
-that corresponds to an equisatisfiable propositional formula to $\varphi$.
-\end{enumerate}

smt/theory_questions/3_1_smt_self.tex

@@ -1,5 +0,0 @@
-\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/theory_questions/3_2_smt_lect.tex

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

smt/theory_questions/3_2_smt_lect_sol.tex

@@ -1,5 +0,0 @@
-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/theory_questions/3_3_smt_self.tex

@@ -1,6 +0,0 @@
-\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/theory_questions/3_5_smt_self.tex

@@ -1 +0,0 @@
-\item \self In the context of \textit{Eager Encoding} within the \textit{Satisfiability Modulo Theories (SMT)}, explain how instances of \textit{reflexivity, symmetry} and \textit{transitivity} are handled within the \textit{Graph-based Reduction}.

smt/theory_questions/3_6_smt_self.tex

@@ -1,9 +0,0 @@
-\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/theory_questions/4_1_smt_lect.tex

@@ -1 +0,0 @@
-\item \lect Explain the concept of \textit{Lazy Encoding} to decide satisfiability of formulas in a first-order theory. 

smt/theory_questions/4_1_smt_lect_sol.tex

@@ -1,8 +0,0 @@
-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/theory_questions/4_1_smt_self.tex

@@ -1,3 +0,0 @@
-\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/theory_questions/4_2_smt_lect.tex

@@ -1,8 +0,0 @@
-\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/theory_questions/4_2_smt_self.tex

@@ -1,2 +0,0 @@
-\item \self 
-\textit{Satisfiability Modulo Theories (SMT)} solvers can be implemented via lazy encoding or via eager encoding. Give a short explanation about both approaches and point out their main differences.

smt/theory_questions/4_3_smt_self.tex

@@ -1 +0,0 @@
-\item \self Consider the problem of deciding satisfiability of quantifier-free theory formulas. What are the main advantages of the DPLL(T) algorithm over eager encoding and lazy encoding?

smt/theory_questions/5_1_smt_lect.tex

@@ -1,4 +0,0 @@
-\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/theory_questions/5_1_smt_self.tex

@@ -1,3 +0,0 @@
-\item \self Explain for what the \textit{Congruence Closure} algorithm is used.
-What are the inputs and outputs of the algorithm? What does the algorithm compute?
-Explain the individual steps of the algorithm. 

symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex

@@ -1,8 +0,0 @@
-\item \lect Given a state space of the size $|S| = 2^5 = 32$ and assuming $v_4$ is the most significant bit and $v_0$ is the least significant bit, which of the following symbolic representations or the given states is correct?
-
-\begin{enumerate}
-    \item[$\square$] State $s_{15}$ is represented by: $\lnot v_4 \land v_3 \land v_3, \land v_1 \land \lnot v_0$
-    \item[$\square$] State $s_{31}$ is represented by: $v_4 \land v_3 \land v_3 \land v_1 \land v_0$
-    \item[$\square$] State $s_{4}$ is represented by: $\lnot v_4 \land \lnot v_3 \land \lnot v_2, \land v_1 \land \lnot v_0$
-    \item[$\square$] State $s_{10}$ is represented by: $v_4 \land v_3 \land \lnot v_3 \land \lnot v_1 \land v_0$
-\end{enumerate}

symbolic_encoding/multiple_choice/2_1_symbrep_self.tex

@@ -1,8 +0,0 @@
-\item \self Given a state space of the size $|S| = 2^9 = 512$ and assuming $v_8$ is the most significant bit and $v_0$ is the least significant bit, which of the following symbolic representations or the given states is correct?
-
-\begin{enumerate}
-    \item[$\square$] State $s_{214}$ is represented by: $\lnot v_8 \land v_7 \land v_6 \land \lnot v_5 \land v_4 \land \lnot v_3 \land v_2 \land v_1 \land \lnot v_0$
-    \item[$\square$] State $s_{501}$ is represented by: $v_8 \land v_7 \land v_6 \land v_5 \land v_4 \land \lnot v_3 \land v_2 \land \lnot v_1 \land v_0$
-    \item[$\square$] State $s_{0}$ is represented by: $\lnot v_8 \land \lnot v_7 \land \lnot v_6 \land \lnot v_5 \land \lnot v_4 \land \lnot v_3 \land \lnot v_2 \land \lnot v_1 \land \lnot v_0$
-    \item[$\square$] State $s_{448}$ is represented by: $v_8 \land v_7 \land v_6 \land \lnot v_5 \land \lnot v_4 \land \lnot v_3 \land \lnot v_2 \land  v_1 \land \lnot v_0$
-\end{enumerate}

symbolic_encoding/practical_questions/1_10_kripke_self.tex

@@ -1,8 +0,0 @@
-\item \self
-
-Consider the example of a controller for a lamp.
-
-Initially the light is off. Pressing the button once turns on the light and the light glows white. From this state, any short-lasting pressure of the button causes the light to switch its color randomly between white, red, green, blue, and yellow.
-At any state, pressing the button for a longer time turns the light off.
-
-Model the lamp controller as \emph{transition system}.

symbolic_encoding/practical_questions/1_1_kripke_lect.tex

@@ -1,4 +0,0 @@
-\item \lect Draw the graph for a \emph{transition system} $\mathcal{T}$ with: 
-$S = \{s_1, s_2, s_3, s_4\}, $\\
-$S_0 = \{s_2\}, $\\
-$R = \{\{s_1, s_2\}, \{s_1, s_1\}, \{s_2, s_4\}, \{s_2, s_3\}, \{s_3, s_1\}, \{s_4, s_2\}, \{s_4, s_3\}\}, $

symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex

@@ -1,29 +0,0 @@
-\begin{center}
-\begin{tikzpicture}[scale=0.2]
-\tikzstyle{every node}+=[inner sep=0pt]
-\draw [black] (11,-26.9) circle (3);
-\draw (11,-26.9) node {$s_2$};
-\draw [black] (23.6,-15) circle (3);
-\draw (23.6,-15) node {$s_1$};
-\draw [black] (23.6,-38) circle (3);
-\draw (23.6,-38) node {$s_4$};
-\draw [black] (36.7,-26.9) circle (3);
-\draw (36.7,-26.9) node {$s_3$};
-\draw [black] (21.42,-17.06) -- (13.18,-24.84);
-\fill [black] (13.18,-24.84) -- (14.11,-24.65) -- (13.42,-23.93);
-\draw [black] (3.7,-26.9) -- (8,-26.9);
-\fill [black] (8,-26.9) -- (7.2,-26.4) -- (7.2,-27.4);
-\draw [black] (25.89,-36.06) -- (34.41,-28.84);
-\fill [black] (34.41,-28.84) -- (33.48,-28.98) -- (34.12,-29.74);
-\draw [black] (34.48,-24.88) -- (25.82,-17.02);
-\fill [black] (25.82,-17.02) -- (26.08,-17.93) -- (26.75,-17.18);
-\draw [black] (14,-26.9) -- (33.7,-26.9);
-\fill [black] (33.7,-26.9) -- (32.9,-26.4) -- (32.9,-27.4);
-\draw [black] (21.35,-36.02) -- (13.25,-28.88);
-\fill [black] (13.25,-28.88) -- (13.52,-29.79) -- (14.18,-29.04);
-\draw [black] (13.25,-28.88) -- (21.35,-36.02);
-\fill [black] (21.35,-36.02) -- (21.08,-35.11) -- (20.42,-35.86);
-\draw [black] (25.456,-12.658) arc (169.34618:-118.65382:2.25);
-\fill [black] (26.59,-15.05) -- (27.28,-15.69) -- (27.47,-14.7);
-\end{tikzpicture}
-\end{center}

symbolic_encoding/practical_questions/1_1_kripke_self.tex

@@ -1,5 +0,0 @@
-\item \self Draw the graph for a \emph{transition system} $\mathcal{T}$ with:
-
-$S = \{s_0, s_1, s_2\}, $\\
-$S_0 = \{s_0, s_1\}, $\\
-$R = \{\{s_0, s_0\}, \{s_0, s_1\}, \{s_0, s_2\}, \{s_1, s_0\}, \{s_1, s_1\}, \{s_1, s_2\}, \{s_2, s_0\}, \{s_2, s_1\}, \{s_2, s_2\}\}$.

symbolic_encoding/practical_questions/1_1_symbrep.tex

@@ -1 +0,0 @@
-\item \self Given a state space of size $|S| = 2^4 = 16$. Give the symbolic encoding for the following states: (a) $s_{4}$, (b) $s_{9}$, and (c) $s_{13}$.

symbolic_encoding/practical_questions/1_1_symbrep_self.tex

@@ -1 +0,0 @@
-\item \self Given a state space of size $|S| = 2^4 = 16$. Give the symbolic encoding for the following states: (a) $s_{4}$, (b) $s_{9}$, and (c) $s_{13}$.

symbolic_encoding/practical_questions/1_2_kripke_lect.tex

@@ -1,38 +0,0 @@
-
-\item \lect 
-Consider the example of an elevator.
-Initially, the elevator is in the ground floor. 
-From the ground floor, it can either go basement, stay there for a while,
-and then go back to the ground floor, or it can go from the ground floor 
-to the second floor, stay there for a while, and go back to the ground floor.
-While traveling between ground floor to second floor, the elevator passes the first floor, but it cannot stop there.
-
-Model this elevator as \emph{transition system}.
-
-
-
-
-\iffalse
-\item \lect 
-  Given the following graph representation of a \textit{transition system}, state the contents of the sets $S, S_0 and R$
-
-\begin{center}
-\vspace{-2em}
-\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt,
-thick,node/.style={circle,draw,minimum size=20pt}]
-    \node[node] (s0) {$s0$};
-    \node (s0s2) [below= 1cm of s0] {};
-    \node[node] (s1) [right of=s0s2] {$s1$};
-    \node[node] (s2) [below of=s0]   {$s2$};
-    \node (start1) [left=1cm of s0] {};
-    
-    \path[->] (start1) edge (s0);
-    \path[->] (s1) edge (s0);
-    \path[->] (s0) edge [bend left] (s2);
-    \path[->] (s2) edge (s1);
-    \path[->] (s2) edge [bend left] (s0);
-    \path[->] (s0.30) edge[bend right=90, looseness=15, out=240, in=300] (s0.60);
-    \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60);
-\end{tikzpicture}
-\end{center}
-\fi

symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex

@@ -1,44 +0,0 @@
-We use the following states:
-%ground floor, basement,second floor, passing ground floor
-\begin{itemize}
-\item $s_g$ indicates that the elevator is on the ground floor.
-\item $s_b$ indicates that the elevator is in the basement.
-\item $s_s$ indicates that the elevator is on the second floor.
-\item $s_f$ indicates that the elevator is passing the first floor.
-\end{itemize}
-The transition system is then given by: $\mathcal{T}$  = ($S$, $S_0$, $R$) with $S$ = $\{s_g, s_b, s_s, s_f\}$, $S_0$ = $\{s_g\}$, $R$ = $\{(s_g, s_g), (s_g, s_b), (s_b, s_b), (s_b, s_g), (s_g, s_f), (s_f, s_s), (s_s, s_s), (s_s, s_f), (s_f, s_g)\}$\\
-
-
-\begin{center}
-\begin{tikzpicture}[scale=0.2]
-\tikzstyle{every node}+=[inner sep=0pt]
-\draw [black] (13.9,-26) circle (3);
-\draw (13.9,-26) node {$s_g$};
-\draw [black] (27.8,-35.6) circle (3);
-\draw (27.8,-35.6) node {$s_b$};
-\draw [black] (27.8,-26) circle (3);
-\draw (27.8,-26) node {$s_f$};
-\draw [black] (27.8,-15.8) circle (3);
-\draw (27.8,-15.8) node {$s_s$};
-\draw [black] (4.8,-26) -- (10.9,-26);
-\fill [black] (10.9,-26) -- (10.1,-25.5) -- (10.1,-26.5);
-\draw [black] (11.501,-24.218) arc (261.13116:-26.86884:2.25);
-\fill [black] (13.85,-23.01) -- (14.47,-22.3) -- (13.48,-22.14);
-\draw [black] (16.37,-27.7) -- (25.33,-33.9);
-\fill [black] (25.33,-33.9) -- (24.96,-33.03) -- (24.39,-33.85);
-\draw [black] (26.957,-38.467) arc (11.34364:-276.65636:2.25);
-\fill [black] (25.01,-36.67) -- (24.13,-36.34) -- (24.33,-37.32);
-\draw [black] (25.33,-33.9) -- (16.37,-27.7);
-\fill [black] (16.37,-27.7) -- (16.74,-28.57) -- (17.31,-27.75);
-\draw [black] (16.9,-26) -- (24.8,-26);
-\fill [black] (24.8,-26) -- (24,-25.5) -- (24,-26.5);
-\draw [black] (27.8,-23) -- (27.8,-18.8);
-\fill [black] (27.8,-18.8) -- (27.3,-19.6) -- (28.3,-19.6);
-\draw [black] (28.483,-12.891) arc (194.52895:-93.47105:2.25);
-\fill [black] (30.52,-14.57) -- (31.42,-14.86) -- (31.17,-13.89);
-\draw [black] (27.8,-18.8) -- (27.8,-23);
-\fill [black] (27.8,-23) -- (28.3,-22.2) -- (27.3,-22.2);
-\draw [black] (24.8,-26) -- (16.9,-26);
-\fill [black] (16.9,-26) -- (17.7,-26.5) -- (17.7,-25.5);
-\end{tikzpicture}
-\end{center}

symbolic_encoding/practical_questions/1_2_kripke_self.tex

@@ -1,25 +0,0 @@
-\item \self
-  Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and
-simplify your formulas. Use a binary encoding to encode the states, e.g.,
-encode the state $s_2$ with the formula $v1 \wedge \neg v_0$.
-
-\begin{center}
-\vspace{-2em}
-\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt,
-thick,node/.style={circle,draw,minimum size=25pt}]
-    \node[node] (s0) {$s_0$};
-    \node[node] (s1) [right of=s0] {$s_1$};
-    \node[node] (s2) [below of=s1] {$s_2$};
-    \node[node] (s3) [below of=s0] {$s_3$};
-    %\path[->] (s0) edge (s1);
-    \path[->] (s0) edge (s2);
-    \path[->] (s0) edge (s3);
-    \path[->] (s1) edge (s2);
-    \path[->] (s1) edge (s3);
-    %\path[->] (s2) edge (s3);
-    \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150);
-    %\path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60);
-    %\path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60);
-    %\path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150);
-\end{tikzpicture}
-\end{center}

symbolic_encoding/practical_questions/1_2_symbrep_self.tex

@@ -1,2 +0,0 @@
-\item \self Given is the  set of states $S=\{s_0,\dots,s_7\}$.
-Find formulas in propositional logic that symbolically represent the sets $A = \{s_0, s_2,s_4, s_6 \}$, $B=\{s_0, s_1,s_2, s_3\}$, and $C=\{s_7, s_1\}$.

symbolic_encoding/practical_questions/1_3_kripke_self.tex

@@ -1,25 +0,0 @@
-\item \self
-  Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and
-simplify your formulas. Use a binary encoding to encode the states, e.g.,
-encode the state $s_2$ with the formula $v1 \wedge \neg v_0$.
-
-\begin{center}
-\vspace{-2em}
-\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt,
-thick,node/.style={circle,draw,minimum size=25pt}]
-    \node[node] (s0) {$s_0$};
-    \node[node] (s1) [right of=s0] {$s_1$};
-    \node[node] (s2) [below of=s1] {$s_2$};
-    \node[node] (s3) [below of=s0] {$s_3$};
-    \path[<->] (s0) edge (s1);
-    \path[<->] (s0) edge (s2);
-    \path[<->] (s0) edge (s3);
-    \path[<->] (s1) edge (s2);
-    \path[<->] (s1) edge (s3);
-    %\path[<->] (s2) edge (s3);
-    \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150);
-    \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60);
-    \path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60);
-    \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150);
-\end{tikzpicture}
-\end{center}

symbolic_encoding/practical_questions/1_4_kripke_self.tex

@@ -1,25 +0,0 @@
-\item \self
-Find a \textit{symbolic encoding} for the set of initial states and the \textit{transition relation} of the following \emph{transition system} and
-simplify your formulas. Use a binary encoding to encode the states, e.g.,
-encode the state $s_2$ with the formula $v1 \wedge \neg v_0$.
-
-\begin{center}
-\vspace{-2em}
-\begin{tikzpicture}[auto, node distance=3cm,shorten >=1pt,
-thick,node/.style={circle,draw,minimum size=25pt}]
-    \node[node] (s0) {$s_0$};
-    \node[node] (s1) [right of=s0] {$s_1$};
-    \node[node] (s2) [below of=s1] {$s_2$};
-    \node[node] (s3) [below of=s0] {$s_3$};
-    \path[<->] (s0) edge (s2);
-    %\path[<->] (s0) edge (s2);
-    %\path[<->] (s0) edge (s3);
-    %\path[<->] (s1) edge (s2);
-    \path[<->] (s1) edge (s3);
-    %\path[<->] (s2) edge (s3);
-    \path[->] (s0.120) edge[bend right=90, looseness=15, out=240, in=300] (s0.150);
-    \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60);
-    \path[->] (s2.30) edge[bend right=90, looseness=15, out=240, in=300] (s2.60);
-    \path[->] (s3.120) edge[bend right=90, looseness=15, out=240, in=300] (s3.150);
-\end{tikzpicture}
-\end{center}

symbolic_encoding/practical_questions/2_05_symbrep_self.tex

@@ -1,32 +0,0 @@
-\item \self Let $x$ and $y$ be the symbolic representations of the sets $X$ and
-    $Y$ respectively, and let $\alpha$ be the symbolic encoding of an
-    element $a$. Consider the following operations and relations
-    between $x$, $y$, and $\alpha$:
-
-\begin{enumerate}[A.]
-\item $x \rightarrow y$
-\item $\alpha \models x$ ?
-\item $x \wedge \neg y$
-\item $\alpha \nvDash y$ ?
-\item $x \equiv \bot$ ?
-\item $x \vee y$
-\end{enumerate}
-
-For each of the following items, state which of the above operations
-symbolically performs the respective set operation or answers the
-respective set-specific question. Write the letters of the
-corresponding operation/question into the boxes of the items below.
-Note that some of the items below do not correspond to any of the
-above operations or questions. Put a ``--'' in the box of these
-items.
-
-\begin{itemize}
-\item[\Huge{$\square$}] Union: $X \cup Y$
-\item[\Huge{$\square$}] Intersection: $X \cap Y$
-\item[\Huge{$\square$}] Set Difference: $X \setminus Y$
-\item[\Huge{$\square$}] Containment: $a \in X$?
-\item[\Huge{$\square$}] Subset: $X \subseteq Y$?
-\item[\Huge{$\square$}] Strict Subset: $X \subset Y$?
-\item[\Huge{$\square$}] Emptiness: $X=\emptyset$?
-\item[\Huge{$\square$}] Equality: $X=Y$?
-\end{itemize}

symbolic_encoding/practical_questions/2_10_symbrep_lect.tex

@@ -1,39 +0,0 @@
-
-\item \lect
-Consider the domain $A=\{Spain, France, Italy, Germany\}$ and
-    the two different symbolic encodings for $A$ given below.
-    Which one gives a shorter symbolic representation for the set
-    $B=\{France, Germany\}$? Illustrate your answer by giving the
-    representing formulas for $B$ in both encodings.
-
-\vspace{.5cm}
-
-%  \begin{minipage}
-    \begin{tabular}{l|l|l}
-    \hline
-    \multicolumn{3}{c}{\textbf{Encoding 1}} \\
-    \hline
-    Element & $v_1$ & $v_0$ \\
-    \hline
-    Spain & $0$ & $0$ \\
-    France & $1$ & $0$ \\
-    Italy & $0$ & $1$ \\
-    Germany & $1$ & $1$
-   \end{tabular}
-%\end{minipage}
-%\begin{minipage}
-\hspace{3cm}
-   \begin{tabular}{l|l|l}
-    \hline
-    \multicolumn{3}{c}{\textbf{Encoding 2}} \\
-    \hline
-    Element & $v_1$ & $v_0$ \\
-    \hline
-    Spain & $0$ & $0$ \\
-    France & $1$ & $0$ \\
-    Italy & $1$ & $1$ \\
-    Germany & $0$ & $1$
-   \end{tabular}
-%\end{minipage}
-  
-  

symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex

@@ -1,7 +0,0 @@
-Using encoding 1, we end up in the following formula:\\
-$b = v_1$\\\\
-Using encoding 2, we end up in the following formula:\\
-$b = (v_1 \land \lnot v_0) \lor (\lnot v_1 \land v_0)$\\
-
-Encoding 1 gives a shorter symbolic representation
-for the set $B=\{France, Germany\}$.

symbolic_encoding/practical_questions/2_10_symbrep_self.tex

@@ -1 +0,0 @@
-\item \self Given a state space of size $|S| = 16$, find a symbolic binary encoding for this state space and compute the characteristic function for the sets of states $$C = \{s_{0}, s_{2}, s_{8}, s_{10}\} \enspace \text{and} \enspace C = \{s_{0}, s_{2}, s_{8}, s_{10}\}$$ Then compute the characteristic function for the sets $D = C \subseteq B$, $E = B \setminus C$ and $F = S \setminus E$. If possible, simplify the formulas.

symbolic_encoding/practical_questions/2_11_symbrep_lect.tex

@@ -1,9 +0,0 @@
-\item  \lect 
-Find a symbolic binary encoding for $X = \{ 0,1, \ldots, 31 \}$.
-  Use it to find formulas that symbolically represent the sets $A$ and $B$ and simplify the formulas:
-  \begin{itemize}
-    \item $A =\{ 12, 13, 14, 15, 28, 29, 30, 31 \}$
-    \item $B =\{x \in X \mid 0 \leq x \leq 15\}$
-  \end{itemize}
-  Furthermore, give the formulas representing the sets
-  $C=A\cap B$ and $D = A \cup B$.

symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex

@@ -1,4 +0,0 @@
-We use 5 Boolean variables, \{$v_4$, . . . , $v_0$\}, for the encoding.\\
-
-$A = (v_2 \land v_3)$\\
-$B = \lnot v_4$

symbolic_encoding/practical_questions/2_11_symbrep_self.tex

@@ -1,21 +0,0 @@
-\item \self Find a symbolic binary encoding for
-$X = \{ 0,1, \ldots, 31 \}$.
-Use it to find characteristic functions for the following sets. If possible, simplify the formulas.
-
-  \begin{enumerate}
-    \item $B =\{x \in X \mid 24 \leq x < 32\}$
-    \item 
-      $C = \left\{ x \in X \middle| \enspace
-      \begin{array}{lll}
-      4 & \leq \enspace x & < 8 \\
-      12  & \leq \enspace x & < 16  \\
-      20 & \leq \enspace x & < 24
-      \end{array}
-      \right\}$
-  \end{enumerate}
-  
-  Compute the characteristic functions of the following sets by symbolic operations, using your results from before and simplify your formulas.
-  \begin{enumerate}
-    \item $D = B \cup C$
-    \item $E = B \cap C$
-  \end{enumerate}

symbolic_encoding/practical_questions/2_12_symbrep_lect.tex

@@ -1,7 +0,0 @@
-\item \self Define the \textit{transition system} from the following symbolically encoded transition relations and draw the
-  corresponding graph:
-  \begin{align*}
-    (\lnot v_1 \land \lnot v_0 \land  v'_1 \land v'_0)  & \enspace \lor  \\
-    (\neg v_1 \land v_0 \land \lnot v'_1 \land  \lnot v'_0) & \enspace \lor  \\
-     (\lnot v_1 \land \lnot v_0 \land  \lnot v'_1 \land \lnot v'_0)    &
-  \end{align*}