From 7f19ef2b95e2a41e2a3f7dfa2cf99e9c3ced8198 Mon Sep 17 00:00:00 2001 From: sp Date: Thu, 13 Jun 2024 09:53:13 +0200 Subject: [PATCH] removed old questions --- smt/multiple_choice/1_1_smt_lect.tex | 8 ---- smt/multiple_choice/2_1_smt_lect.tex | 8 ---- smt/multiple_choice/2_1_smt_self.tex | 7 --- smt/multiple_choice/2_2_smt_self.tex | 8 ---- smt/multiple_choice/3_1_a_smt_self.tex | 8 ---- smt/multiple_choice/3_1_b_smt_self.tex | 9 ---- smt/multiple_choice/3_1_smt_self.tex | 8 ---- smt/multiple_choice/3_2_smt_lect.tex | 11 ----- smt/multiple_choice/4_1_smt_self.tex | 9 ---- smt/multiple_choice/5_1_smt_lect.tex | 8 ---- smt/practical_questions/0_1_a_smt_prac.tex | 7 --- smt/practical_questions/0_1_smt_prac.tex | 6 --- smt/practical_questions/0_2_a_smt_prac.tex | 8 ---- smt/practical_questions/0_2_smt_prac.tex | 12 ----- smt/practical_questions/0_3_a_smt_prac.tex | 4 -- smt/practical_questions/0_3_smt_prac.tex | 3 -- smt/practical_questions/3_0_smt_lect.tex | 6 --- smt/practical_questions/3_0_smt_lect_sol.tex | 11 ----- smt/practical_questions/3_1_a_smt_lect.tex | 8 ---- .../3_1_a_smt_lect_sol.tex | 12 ----- smt/practical_questions/3_1_smt_lect.tex | 6 --- smt/practical_questions/3_1_smt_lect_sol.tex | 12 ----- smt/practical_questions/3_1_smt_self.tex | 2 - smt/practical_questions/3_2_a_smt_lect.tex | 6 --- .../3_2_a_smt_lect_sol.tex | 27 ----------- smt/practical_questions/3_2_smt_lect.tex | 6 --- smt/practical_questions/3_2_smt_lect_sol.tex | 22 --------- smt/practical_questions/3_2_smt_self.tex | 7 --- smt/practical_questions/3_3_smt_lect.tex | 0 smt/practical_questions/3_3_smt_self.tex | 8 ---- smt/practical_questions/3_4_smt_self.tex | 6 --- smt/practical_questions/3_5_smt_self.tex | 8 ---- smt/practical_questions/5_1_smt_lect.tex | 5 -- smt/practical_questions/5_1_smt_lect_sol.tex | 10 ---- smt/practical_questions/5_1_smt_self.tex | 5 -- smt/practical_questions/5_2_smt_lect.tex | 5 -- smt/practical_questions/5_2_smt_self.tex | 5 -- smt/practical_questions/5_3_smt_self.tex | 6 --- smt/practical_questions/5_4_smt_self.tex | 26 ---------- smt/theory_questions/1_0_smt_self.tex | 1 - smt/theory_questions/1_1_a_smt_lect.tex | 1 - smt/theory_questions/1_1_a_smt_lect_sol.tex | 10 ---- smt/theory_questions/1_1_b_smt_lect.tex | 2 - smt/theory_questions/1_1_b_smt_lect_sol.tex | 4 -- smt/theory_questions/1_1_c_smt_lect.tex | 2 - smt/theory_questions/1_1_c_smt_lect_sol.tex | 6 --- smt/theory_questions/1_1_d_smt_lect.tex | 2 - smt/theory_questions/1_1_d_smt_lect_sol.tex | 4 -- smt/theory_questions/1_1_smt_lect.tex | 7 --- smt/theory_questions/1_1_smt_lect_sol.tex | 7 --- smt/theory_questions/1_1_smt_self.tex | 1 - smt/theory_questions/1_2_smt_lect.tex | 1 - smt/theory_questions/1_2_smt_lect_sol.tex | 6 --- smt/theory_questions/1_2_smt_self.tex | 1 - smt/theory_questions/1_3_smt_self.tex | 1 - smt/theory_questions/2_1_a_smt_self.tex | 3 -- smt/theory_questions/2_1_b_smt_self.tex | 6 --- smt/theory_questions/2_1_smt_lect.tex | 2 - smt/theory_questions/2_1_smt_lect_sol.tex | 9 ---- smt/theory_questions/2_1_smt_self.tex | 1 - smt/theory_questions/2_2_smt_lect.tex | 2 - smt/theory_questions/2_2_smt_lect_sol.tex | 10 ---- smt/theory_questions/3_1_smt_lect.tex | 2 - smt/theory_questions/3_1_smt_lect_sol.tex | 13 ----- smt/theory_questions/3_1_smt_self.tex | 5 -- smt/theory_questions/3_2_smt_lect.tex | 1 - smt/theory_questions/3_2_smt_lect_sol.tex | 5 -- smt/theory_questions/3_3_smt_self.tex | 6 --- smt/theory_questions/3_5_smt_self.tex | 1 - smt/theory_questions/3_6_smt_self.tex | 9 ---- smt/theory_questions/4_1_smt_lect.tex | 1 - smt/theory_questions/4_1_smt_lect_sol.tex | 8 ---- smt/theory_questions/4_1_smt_self.tex | 3 -- smt/theory_questions/4_2_smt_lect.tex | 8 ---- smt/theory_questions/4_2_smt_self.tex | 2 - smt/theory_questions/4_3_smt_self.tex | 1 - smt/theory_questions/5_1_smt_lect.tex | 4 -- smt/theory_questions/5_1_smt_self.tex | 3 -- .../multiple_choice/2_1_symbrep_lect.tex | 8 ---- .../multiple_choice/2_1_symbrep_self.tex | 8 ---- .../practical_questions/1_10_kripke_self.tex | 8 ---- .../practical_questions/1_1_kripke_lect.tex | 4 -- .../1_1_kripke_lect_sol.tex | 29 ----------- .../practical_questions/1_1_kripke_self.tex | 5 -- .../practical_questions/1_1_symbrep.tex | 1 - .../practical_questions/1_1_symbrep_self.tex | 1 - .../practical_questions/1_2_kripke_lect.tex | 38 --------------- .../1_2_kripke_lect_sol.tex | 44 ----------------- .../practical_questions/1_2_kripke_self.tex | 25 ---------- .../practical_questions/1_2_symbrep_self.tex | 2 - .../practical_questions/1_3_kripke_self.tex | 25 ---------- .../practical_questions/1_4_kripke_self.tex | 25 ---------- .../practical_questions/2_05_symbrep_self.tex | 32 ------------- .../practical_questions/2_10_symbrep_lect.tex | 39 --------------- .../2_10_symbrep_lect_sol.tex | 7 --- .../practical_questions/2_10_symbrep_self.tex | 1 - .../practical_questions/2_11_symbrep_lect.tex | 9 ---- .../2_11_symbrep_lect_sol.tex | 4 -- .../practical_questions/2_11_symbrep_self.tex | 21 -------- .../practical_questions/2_12_symbrep_lect.tex | 7 --- .../practical_questions/2_12_symbrep_self.tex | 15 ------ .../practical_questions/2_13_symbrep_lect.tex | 24 ---------- .../2_13_symbrep_lect_sol.tex | 15 ------ .../practical_questions/2_13_symbrep_self.tex | 15 ------ .../practical_questions/2_17_symbrep_self.tex | 33 ------------- .../practical_questions/2_18_symbrep_self.tex | 7 --- .../practical_questions/2_1_symbrep_lect.tex | 1 - .../2_1_symbrep_lect_sol.tex | 6 --- .../practical_questions/2_1_symbrep_self.tex | 7 --- .../practical_questions/2_20_symbrep_self.tex | 9 ---- .../practical_questions/2_2_symbrep_lect.tex | 2 - .../2_2_symbrep_lect_sol.tex | 6 --- .../practical_questions/2_2_symbrep_self.tex | 8 ---- .../practical_questions/2_3_symbrep_lect.tex | 40 ---------------- .../practical_questions/2_3_symbrep_self.tex | 48 ------------------- .../practical_questions/2_4_symbrep_lect.tex | 15 ------ .../practical_questions/2_4_symbrep_self.tex | 17 ------- .../practical_questions/2_5_symbrep_self.tex | 36 -------------- .../practical_questions/2_6_symbrep_lect.tex | 2 - .../practical_questions/2_6_symbrep_self.tex | 41 ---------------- .../practical_questions/2_7_symbrep_lect.tex | 14 ------ .../practical_questions/2_7_symbrep_self.tex | 37 -------------- .../practical_questions/2_8_symbrep_self.tex | 1 - .../practical_questions/2_9_symbrep_lect.tex | 24 ---------- .../2_9_symbrep_lect_sol.tex | 13 ----- .../practical_questions/2_9_symbrep_self.tex | 3 -- .../theory_questions/0_1_symb_lect.tex | 1 - .../theory_questions/0_1_symb_self.tex | 1 - .../theory_questions/1_0_kripke_self.tex | 2 - .../theory_questions/2_01_symbrep_self.tex | 3 -- .../theory_questions/2_1_symbrep_self.tex | 1 - .../theory_questions/2_2_symbrep_self.tex | 4 -- .../theory_questions/2_3_symbrep_lect.tex | 1 - .../theory_questions/2_3_symbrep_self.tex | 5 -- 134 files changed, 1294 deletions(-) delete mode 100644 smt/multiple_choice/1_1_smt_lect.tex delete mode 100644 smt/multiple_choice/2_1_smt_lect.tex delete mode 100644 smt/multiple_choice/2_1_smt_self.tex delete mode 100644 smt/multiple_choice/2_2_smt_self.tex delete mode 100644 smt/multiple_choice/3_1_a_smt_self.tex delete mode 100644 smt/multiple_choice/3_1_b_smt_self.tex delete mode 100644 smt/multiple_choice/3_1_smt_self.tex delete mode 100644 smt/multiple_choice/3_2_smt_lect.tex delete mode 100644 smt/multiple_choice/4_1_smt_self.tex delete mode 100644 smt/multiple_choice/5_1_smt_lect.tex delete mode 100644 smt/practical_questions/0_1_a_smt_prac.tex delete mode 100644 smt/practical_questions/0_1_smt_prac.tex delete mode 100644 smt/practical_questions/0_2_a_smt_prac.tex delete mode 100644 smt/practical_questions/0_2_smt_prac.tex delete mode 100644 smt/practical_questions/0_3_a_smt_prac.tex delete mode 100644 smt/practical_questions/0_3_smt_prac.tex delete mode 100644 smt/practical_questions/3_0_smt_lect.tex delete mode 100644 smt/practical_questions/3_0_smt_lect_sol.tex delete mode 100644 smt/practical_questions/3_1_a_smt_lect.tex delete mode 100644 smt/practical_questions/3_1_a_smt_lect_sol.tex delete mode 100644 smt/practical_questions/3_1_smt_lect.tex delete mode 100644 smt/practical_questions/3_1_smt_lect_sol.tex delete mode 100644 smt/practical_questions/3_1_smt_self.tex delete mode 100644 smt/practical_questions/3_2_a_smt_lect.tex delete mode 100644 smt/practical_questions/3_2_a_smt_lect_sol.tex delete mode 100644 smt/practical_questions/3_2_smt_lect.tex delete mode 100644 smt/practical_questions/3_2_smt_lect_sol.tex delete mode 100644 smt/practical_questions/3_2_smt_self.tex delete mode 100644 smt/practical_questions/3_3_smt_lect.tex delete mode 100644 smt/practical_questions/3_3_smt_self.tex delete mode 100644 smt/practical_questions/3_4_smt_self.tex delete mode 100644 smt/practical_questions/3_5_smt_self.tex delete mode 100644 smt/practical_questions/5_1_smt_lect.tex delete mode 100644 smt/practical_questions/5_1_smt_lect_sol.tex delete mode 100644 smt/practical_questions/5_1_smt_self.tex delete mode 100644 smt/practical_questions/5_2_smt_lect.tex delete mode 100644 smt/practical_questions/5_2_smt_self.tex delete mode 100644 smt/practical_questions/5_3_smt_self.tex delete mode 100644 smt/practical_questions/5_4_smt_self.tex delete mode 100644 smt/theory_questions/1_0_smt_self.tex delete mode 100644 smt/theory_questions/1_1_a_smt_lect.tex delete mode 100644 smt/theory_questions/1_1_a_smt_lect_sol.tex delete mode 100644 smt/theory_questions/1_1_b_smt_lect.tex delete mode 100644 smt/theory_questions/1_1_b_smt_lect_sol.tex delete mode 100644 smt/theory_questions/1_1_c_smt_lect.tex delete mode 100644 smt/theory_questions/1_1_c_smt_lect_sol.tex delete mode 100644 smt/theory_questions/1_1_d_smt_lect.tex delete mode 100644 smt/theory_questions/1_1_d_smt_lect_sol.tex delete mode 100644 smt/theory_questions/1_1_smt_lect.tex delete mode 100644 smt/theory_questions/1_1_smt_lect_sol.tex delete mode 100644 smt/theory_questions/1_1_smt_self.tex delete mode 100644 smt/theory_questions/1_2_smt_lect.tex delete mode 100644 smt/theory_questions/1_2_smt_lect_sol.tex delete mode 100644 smt/theory_questions/1_2_smt_self.tex delete mode 100644 smt/theory_questions/1_3_smt_self.tex delete mode 100644 smt/theory_questions/2_1_a_smt_self.tex delete mode 100644 smt/theory_questions/2_1_b_smt_self.tex delete mode 100644 smt/theory_questions/2_1_smt_lect.tex delete mode 100644 smt/theory_questions/2_1_smt_lect_sol.tex delete mode 100644 smt/theory_questions/2_1_smt_self.tex delete mode 100644 smt/theory_questions/2_2_smt_lect.tex delete mode 100644 smt/theory_questions/2_2_smt_lect_sol.tex delete mode 100644 smt/theory_questions/3_1_smt_lect.tex delete mode 100644 smt/theory_questions/3_1_smt_lect_sol.tex delete mode 100644 smt/theory_questions/3_1_smt_self.tex delete mode 100644 smt/theory_questions/3_2_smt_lect.tex delete mode 100644 smt/theory_questions/3_2_smt_lect_sol.tex delete mode 100644 smt/theory_questions/3_3_smt_self.tex delete mode 100644 smt/theory_questions/3_5_smt_self.tex delete mode 100644 smt/theory_questions/3_6_smt_self.tex delete mode 100644 smt/theory_questions/4_1_smt_lect.tex delete mode 100644 smt/theory_questions/4_1_smt_lect_sol.tex delete mode 100644 smt/theory_questions/4_1_smt_self.tex delete mode 100644 smt/theory_questions/4_2_smt_lect.tex delete mode 100644 smt/theory_questions/4_2_smt_self.tex delete mode 100644 smt/theory_questions/4_3_smt_self.tex delete mode 100644 smt/theory_questions/5_1_smt_lect.tex delete mode 100644 smt/theory_questions/5_1_smt_self.tex delete mode 100644 symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex delete mode 100644 symbolic_encoding/multiple_choice/2_1_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_10_kripke_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_1_kripke_lect.tex delete mode 100644 symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/1_1_kripke_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_1_symbrep.tex delete mode 100644 symbolic_encoding/practical_questions/1_1_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_2_kripke_lect.tex delete mode 100644 symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/1_2_kripke_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_2_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_3_kripke_self.tex delete mode 100644 symbolic_encoding/practical_questions/1_4_kripke_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_05_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_10_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/2_10_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_11_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/2_11_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_12_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_12_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_13_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/2_13_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_17_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_18_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_1_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/2_1_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_20_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_2_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/2_2_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_3_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_3_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_4_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_4_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_5_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_6_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_6_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_7_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_7_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_8_symbrep_self.tex delete mode 100644 symbolic_encoding/practical_questions/2_9_symbrep_lect.tex delete mode 100644 symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex delete mode 100644 symbolic_encoding/practical_questions/2_9_symbrep_self.tex delete mode 100644 symbolic_encoding/theory_questions/0_1_symb_lect.tex delete mode 100644 symbolic_encoding/theory_questions/0_1_symb_self.tex delete mode 100644 symbolic_encoding/theory_questions/1_0_kripke_self.tex delete mode 100644 symbolic_encoding/theory_questions/2_01_symbrep_self.tex delete mode 100644 symbolic_encoding/theory_questions/2_1_symbrep_self.tex delete mode 100644 symbolic_encoding/theory_questions/2_2_symbrep_self.tex delete mode 100644 symbolic_encoding/theory_questions/2_3_symbrep_lect.tex delete mode 100644 symbolic_encoding/theory_questions/2_3_symbrep_self.tex diff --git a/smt/multiple_choice/1_1_smt_lect.tex b/smt/multiple_choice/1_1_smt_lect.tex deleted file mode 100644 index d03cafe..0000000 --- a/smt/multiple_choice/1_1_smt_lect.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/2_1_smt_lect.tex b/smt/multiple_choice/2_1_smt_lect.tex deleted file mode 100644 index 05fe5ef..0000000 --- a/smt/multiple_choice/2_1_smt_lect.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/2_1_smt_self.tex b/smt/multiple_choice/2_1_smt_self.tex deleted file mode 100644 index 378b7ad..0000000 --- a/smt/multiple_choice/2_1_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/2_2_smt_self.tex b/smt/multiple_choice/2_2_smt_self.tex deleted file mode 100644 index a76f330..0000000 --- a/smt/multiple_choice/2_2_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/3_1_a_smt_self.tex b/smt/multiple_choice/3_1_a_smt_self.tex deleted file mode 100644 index eefd34b..0000000 --- a/smt/multiple_choice/3_1_a_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/3_1_b_smt_self.tex b/smt/multiple_choice/3_1_b_smt_self.tex deleted file mode 100644 index a60205c..0000000 --- a/smt/multiple_choice/3_1_b_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/3_1_smt_self.tex b/smt/multiple_choice/3_1_smt_self.tex deleted file mode 100644 index 75045cc..0000000 --- a/smt/multiple_choice/3_1_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/3_2_smt_lect.tex b/smt/multiple_choice/3_2_smt_lect.tex deleted file mode 100644 index f05a957..0000000 --- a/smt/multiple_choice/3_2_smt_lect.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/multiple_choice/4_1_smt_self.tex b/smt/multiple_choice/4_1_smt_self.tex deleted file mode 100644 index 67edc94..0000000 --- a/smt/multiple_choice/4_1_smt_self.tex +++ /dev/null @@ -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} diff --git a/smt/multiple_choice/5_1_smt_lect.tex b/smt/multiple_choice/5_1_smt_lect.tex deleted file mode 100644 index 911aaaa..0000000 --- a/smt/multiple_choice/5_1_smt_lect.tex +++ /dev/null @@ -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} diff --git a/smt/practical_questions/0_1_a_smt_prac.tex b/smt/practical_questions/0_1_a_smt_prac.tex deleted file mode 100644 index 84a90a2..0000000 --- a/smt/practical_questions/0_1_a_smt_prac.tex +++ /dev/null @@ -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}$. diff --git a/smt/practical_questions/0_1_smt_prac.tex b/smt/practical_questions/0_1_smt_prac.tex deleted file mode 100644 index 5fa0e04..0000000 --- a/smt/practical_questions/0_1_smt_prac.tex +++ /dev/null @@ -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}$. \ No newline at end of file diff --git a/smt/practical_questions/0_2_a_smt_prac.tex b/smt/practical_questions/0_2_a_smt_prac.tex deleted file mode 100644 index a9b5e23..0000000 --- a/smt/practical_questions/0_2_a_smt_prac.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/practical_questions/0_2_smt_prac.tex b/smt/practical_questions/0_2_smt_prac.tex deleted file mode 100644 index ebf8b59..0000000 --- a/smt/practical_questions/0_2_smt_prac.tex +++ /dev/null @@ -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*} - - - - - diff --git a/smt/practical_questions/0_3_a_smt_prac.tex b/smt/practical_questions/0_3_a_smt_prac.tex deleted file mode 100644 index 2baca7b..0000000 --- a/smt/practical_questions/0_3_a_smt_prac.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/smt/practical_questions/0_3_smt_prac.tex b/smt/practical_questions/0_3_smt_prac.tex deleted file mode 100644 index ecf548c..0000000 --- a/smt/practical_questions/0_3_smt_prac.tex +++ /dev/null @@ -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)$$ \ No newline at end of file diff --git a/smt/practical_questions/3_0_smt_lect.tex b/smt/practical_questions/3_0_smt_lect.tex deleted file mode 100644 index 9bdafe1..0000000 --- a/smt/practical_questions/3_0_smt_lect.tex +++ /dev/null @@ -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}$. diff --git a/smt/practical_questions/3_0_smt_lect_sol.tex b/smt/practical_questions/3_0_smt_lect_sol.tex deleted file mode 100644 index 062eb72..0000000 --- a/smt/practical_questions/3_0_smt_lect_sol.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/smt/practical_questions/3_1_a_smt_lect.tex b/smt/practical_questions/3_1_a_smt_lect.tex deleted file mode 100644 index ba56994..0000000 --- a/smt/practical_questions/3_1_a_smt_lect.tex +++ /dev/null @@ -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}$. diff --git a/smt/practical_questions/3_1_a_smt_lect_sol.tex b/smt/practical_questions/3_1_a_smt_lect_sol.tex deleted file mode 100644 index 59a1b24..0000000 --- a/smt/practical_questions/3_1_a_smt_lect_sol.tex +++ /dev/null @@ -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*} diff --git a/smt/practical_questions/3_1_smt_lect.tex b/smt/practical_questions/3_1_smt_lect.tex deleted file mode 100644 index 1cac3cd..0000000 --- a/smt/practical_questions/3_1_smt_lect.tex +++ /dev/null @@ -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}$. diff --git a/smt/practical_questions/3_1_smt_lect_sol.tex b/smt/practical_questions/3_1_smt_lect_sol.tex deleted file mode 100644 index 9e171ce..0000000 --- a/smt/practical_questions/3_1_smt_lect_sol.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/smt/practical_questions/3_1_smt_self.tex b/smt/practical_questions/3_1_smt_self.tex deleted file mode 100644 index ed0930e..0000000 --- a/smt/practical_questions/3_1_smt_self.tex +++ /dev/null @@ -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].$$ diff --git a/smt/practical_questions/3_2_a_smt_lect.tex b/smt/practical_questions/3_2_a_smt_lect.tex deleted file mode 100644 index 6d51ac6..0000000 --- a/smt/practical_questions/3_2_a_smt_lect.tex +++ /dev/null @@ -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*} - \ No newline at end of file diff --git a/smt/practical_questions/3_2_a_smt_lect_sol.tex b/smt/practical_questions/3_2_a_smt_lect_sol.tex deleted file mode 100644 index 8843ad4..0000000 --- a/smt/practical_questions/3_2_a_smt_lect_sol.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/smt/practical_questions/3_2_smt_lect.tex b/smt/practical_questions/3_2_smt_lect.tex deleted file mode 100644 index 7d54a3f..0000000 --- a/smt/practical_questions/3_2_smt_lect.tex +++ /dev/null @@ -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*} - diff --git a/smt/practical_questions/3_2_smt_lect_sol.tex b/smt/practical_questions/3_2_smt_lect_sol.tex deleted file mode 100644 index 969e71f..0000000 --- a/smt/practical_questions/3_2_smt_lect_sol.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/smt/practical_questions/3_2_smt_self.tex b/smt/practical_questions/3_2_smt_self.tex deleted file mode 100644 index 0ff2d3e..0000000 --- a/smt/practical_questions/3_2_smt_self.tex +++ /dev/null @@ -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}$. - diff --git a/smt/practical_questions/3_3_smt_lect.tex b/smt/practical_questions/3_3_smt_lect.tex deleted file mode 100644 index e69de29..0000000 diff --git a/smt/practical_questions/3_3_smt_self.tex b/smt/practical_questions/3_3_smt_self.tex deleted file mode 100644 index 5facd9c..0000000 --- a/smt/practical_questions/3_3_smt_self.tex +++ /dev/null @@ -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? \ No newline at end of file diff --git a/smt/practical_questions/3_4_smt_self.tex b/smt/practical_questions/3_4_smt_self.tex deleted file mode 100644 index 7f54c53..0000000 --- a/smt/practical_questions/3_4_smt_self.tex +++ /dev/null @@ -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}$. diff --git a/smt/practical_questions/3_5_smt_self.tex b/smt/practical_questions/3_5_smt_self.tex deleted file mode 100644 index 543d113..0000000 --- a/smt/practical_questions/3_5_smt_self.tex +++ /dev/null @@ -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}$. \ No newline at end of file diff --git a/smt/practical_questions/5_1_smt_lect.tex b/smt/practical_questions/5_1_smt_lect.tex deleted file mode 100644 index 362b1f0..0000000 --- a/smt/practical_questions/5_1_smt_lect.tex +++ /dev/null @@ -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. diff --git a/smt/practical_questions/5_1_smt_lect_sol.tex b/smt/practical_questions/5_1_smt_lect_sol.tex deleted file mode 100644 index 3899f63..0000000 --- a/smt/practical_questions/5_1_smt_lect_sol.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/practical_questions/5_1_smt_self.tex b/smt/practical_questions/5_1_smt_self.tex deleted file mode 100644 index a263e10..0000000 --- a/smt/practical_questions/5_1_smt_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/practical_questions/5_2_smt_lect.tex b/smt/practical_questions/5_2_smt_lect.tex deleted file mode 100644 index fc27a28..0000000 --- a/smt/practical_questions/5_2_smt_lect.tex +++ /dev/null @@ -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)$ - diff --git a/smt/practical_questions/5_2_smt_self.tex b/smt/practical_questions/5_2_smt_self.tex deleted file mode 100644 index b4a0d5e..0000000 --- a/smt/practical_questions/5_2_smt_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/practical_questions/5_3_smt_self.tex b/smt/practical_questions/5_3_smt_self.tex deleted file mode 100644 index 112ee20..0000000 --- a/smt/practical_questions/5_3_smt_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/practical_questions/5_4_smt_self.tex b/smt/practical_questions/5_4_smt_self.tex deleted file mode 100644 index d1bcf83..0000000 --- a/smt/practical_questions/5_4_smt_self.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/smt/theory_questions/1_0_smt_self.tex b/smt/theory_questions/1_0_smt_self.tex deleted file mode 100644 index 5b40a19..0000000 --- a/smt/theory_questions/1_0_smt_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/1_1_a_smt_lect.tex b/smt/theory_questions/1_1_a_smt_lect.tex deleted file mode 100644 index d487102..0000000 --- a/smt/theory_questions/1_1_a_smt_lect.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/1_1_a_smt_lect_sol.tex b/smt/theory_questions/1_1_a_smt_lect_sol.tex deleted file mode 100644 index 15f4ef6..0000000 --- a/smt/theory_questions/1_1_a_smt_lect_sol.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/theory_questions/1_1_b_smt_lect.tex b/smt/theory_questions/1_1_b_smt_lect.tex deleted file mode 100644 index 7bfa74c..0000000 --- a/smt/theory_questions/1_1_b_smt_lect.tex +++ /dev/null @@ -1,2 +0,0 @@ - -\item \lect Give the definition of a theory of formulas in first-order logic. diff --git a/smt/theory_questions/1_1_b_smt_lect_sol.tex b/smt/theory_questions/1_1_b_smt_lect_sol.tex deleted file mode 100644 index b4d3ce4..0000000 --- a/smt/theory_questions/1_1_b_smt_lect_sol.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/1_1_c_smt_lect.tex b/smt/theory_questions/1_1_c_smt_lect.tex deleted file mode 100644 index 9f51cb5..0000000 --- a/smt/theory_questions/1_1_c_smt_lect.tex +++ /dev/null @@ -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. diff --git a/smt/theory_questions/1_1_c_smt_lect_sol.tex b/smt/theory_questions/1_1_c_smt_lect_sol.tex deleted file mode 100644 index 3597f23..0000000 --- a/smt/theory_questions/1_1_c_smt_lect_sol.tex +++ /dev/null @@ -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} diff --git a/smt/theory_questions/1_1_d_smt_lect.tex b/smt/theory_questions/1_1_d_smt_lect.tex deleted file mode 100644 index 5fbced3..0000000 --- a/smt/theory_questions/1_1_d_smt_lect.tex +++ /dev/null @@ -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? \ No newline at end of file diff --git a/smt/theory_questions/1_1_d_smt_lect_sol.tex b/smt/theory_questions/1_1_d_smt_lect_sol.tex deleted file mode 100644 index 960043b..0000000 --- a/smt/theory_questions/1_1_d_smt_lect_sol.tex +++ /dev/null @@ -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. diff --git a/smt/theory_questions/1_1_smt_lect.tex b/smt/theory_questions/1_1_smt_lect.tex deleted file mode 100644 index 06374da..0000000 --- a/smt/theory_questions/1_1_smt_lect.tex +++ /dev/null @@ -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}. - - - - - - diff --git a/smt/theory_questions/1_1_smt_lect_sol.tex b/smt/theory_questions/1_1_smt_lect_sol.tex deleted file mode 100644 index 376b194..0000000 --- a/smt/theory_questions/1_1_smt_lect_sol.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/1_1_smt_self.tex b/smt/theory_questions/1_1_smt_self.tex deleted file mode 100644 index 2dfe4f2..0000000 --- a/smt/theory_questions/1_1_smt_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/1_2_smt_lect.tex b/smt/theory_questions/1_2_smt_lect.tex deleted file mode 100644 index 702eb05..0000000 --- a/smt/theory_questions/1_2_smt_lect.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/1_2_smt_lect_sol.tex b/smt/theory_questions/1_2_smt_lect_sol.tex deleted file mode 100644 index 823439c..0000000 --- a/smt/theory_questions/1_2_smt_lect_sol.tex +++ /dev/null @@ -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$. \ No newline at end of file diff --git a/smt/theory_questions/1_2_smt_self.tex b/smt/theory_questions/1_2_smt_self.tex deleted file mode 100644 index 549839f..0000000 --- a/smt/theory_questions/1_2_smt_self.tex +++ /dev/null @@ -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? \ No newline at end of file diff --git a/smt/theory_questions/1_3_smt_self.tex b/smt/theory_questions/1_3_smt_self.tex deleted file mode 100644 index 9a1d304..0000000 --- a/smt/theory_questions/1_3_smt_self.tex +++ /dev/null @@ -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. diff --git a/smt/theory_questions/2_1_a_smt_self.tex b/smt/theory_questions/2_1_a_smt_self.tex deleted file mode 100644 index 5e5d5d3..0000000 --- a/smt/theory_questions/2_1_a_smt_self.tex +++ /dev/null @@ -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? \ No newline at end of file diff --git a/smt/theory_questions/2_1_b_smt_self.tex b/smt/theory_questions/2_1_b_smt_self.tex deleted file mode 100644 index 25168f1..0000000 --- a/smt/theory_questions/2_1_b_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/theory_questions/2_1_smt_lect.tex b/smt/theory_questions/2_1_smt_lect.tex deleted file mode 100644 index 73c901d..0000000 --- a/smt/theory_questions/2_1_smt_lect.tex +++ /dev/null @@ -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}$. \ No newline at end of file diff --git a/smt/theory_questions/2_1_smt_lect_sol.tex b/smt/theory_questions/2_1_smt_lect_sol.tex deleted file mode 100644 index 0ac4d7d..0000000 --- a/smt/theory_questions/2_1_smt_lect_sol.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/theory_questions/2_1_smt_self.tex b/smt/theory_questions/2_1_smt_self.tex deleted file mode 100644 index 02ac565..0000000 --- a/smt/theory_questions/2_1_smt_self.tex +++ /dev/null @@ -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$. diff --git a/smt/theory_questions/2_2_smt_lect.tex b/smt/theory_questions/2_2_smt_lect.tex deleted file mode 100644 index 679e46b..0000000 --- a/smt/theory_questions/2_2_smt_lect.tex +++ /dev/null @@ -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. diff --git a/smt/theory_questions/2_2_smt_lect_sol.tex b/smt/theory_questions/2_2_smt_lect_sol.tex deleted file mode 100644 index 67d21e7..0000000 --- a/smt/theory_questions/2_2_smt_lect_sol.tex +++ /dev/null @@ -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} - - diff --git a/smt/theory_questions/3_1_smt_lect.tex b/smt/theory_questions/3_1_smt_lect.tex deleted file mode 100644 index f68d1d2..0000000 --- a/smt/theory_questions/3_1_smt_lect.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/3_1_smt_lect_sol.tex b/smt/theory_questions/3_1_smt_lect_sol.tex deleted file mode 100644 index 724f9f1..0000000 --- a/smt/theory_questions/3_1_smt_lect_sol.tex +++ /dev/null @@ -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} diff --git a/smt/theory_questions/3_1_smt_self.tex b/smt/theory_questions/3_1_smt_self.tex deleted file mode 100644 index f9a1f37..0000000 --- a/smt/theory_questions/3_1_smt_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/theory_questions/3_2_smt_lect.tex b/smt/theory_questions/3_2_smt_lect.tex deleted file mode 100644 index a778692..0000000 --- a/smt/theory_questions/3_2_smt_lect.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/3_2_smt_lect_sol.tex b/smt/theory_questions/3_2_smt_lect_sol.tex deleted file mode 100644 index b583ad3..0000000 --- a/smt/theory_questions/3_2_smt_lect_sol.tex +++ /dev/null @@ -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} diff --git a/smt/theory_questions/3_3_smt_self.tex b/smt/theory_questions/3_3_smt_self.tex deleted file mode 100644 index 51f7efd..0000000 --- a/smt/theory_questions/3_3_smt_self.tex +++ /dev/null @@ -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}. \ No newline at end of file diff --git a/smt/theory_questions/3_5_smt_self.tex b/smt/theory_questions/3_5_smt_self.tex deleted file mode 100644 index cede4cb..0000000 --- a/smt/theory_questions/3_5_smt_self.tex +++ /dev/null @@ -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}. \ No newline at end of file diff --git a/smt/theory_questions/3_6_smt_self.tex b/smt/theory_questions/3_6_smt_self.tex deleted file mode 100644 index e1698b3..0000000 --- a/smt/theory_questions/3_6_smt_self.tex +++ /dev/null @@ -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}. \ No newline at end of file diff --git a/smt/theory_questions/4_1_smt_lect.tex b/smt/theory_questions/4_1_smt_lect.tex deleted file mode 100644 index 44c1a36..0000000 --- a/smt/theory_questions/4_1_smt_lect.tex +++ /dev/null @@ -1 +0,0 @@ -\item \lect Explain the concept of \textit{Lazy Encoding} to decide satisfiability of formulas in a first-order theory. \ No newline at end of file diff --git a/smt/theory_questions/4_1_smt_lect_sol.tex b/smt/theory_questions/4_1_smt_lect_sol.tex deleted file mode 100644 index cba7b1e..0000000 --- a/smt/theory_questions/4_1_smt_lect_sol.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/4_1_smt_self.tex b/smt/theory_questions/4_1_smt_self.tex deleted file mode 100644 index 701e772..0000000 --- a/smt/theory_questions/4_1_smt_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/smt/theory_questions/4_2_smt_lect.tex b/smt/theory_questions/4_2_smt_lect.tex deleted file mode 100644 index b111f1a..0000000 --- a/smt/theory_questions/4_2_smt_lect.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/smt/theory_questions/4_2_smt_self.tex b/smt/theory_questions/4_2_smt_self.tex deleted file mode 100644 index 5deb213..0000000 --- a/smt/theory_questions/4_2_smt_self.tex +++ /dev/null @@ -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. diff --git a/smt/theory_questions/4_3_smt_self.tex b/smt/theory_questions/4_3_smt_self.tex deleted file mode 100644 index 9a2b981..0000000 --- a/smt/theory_questions/4_3_smt_self.tex +++ /dev/null @@ -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? diff --git a/smt/theory_questions/5_1_smt_lect.tex b/smt/theory_questions/5_1_smt_lect.tex deleted file mode 100644 index 9a21857..0000000 --- a/smt/theory_questions/5_1_smt_lect.tex +++ /dev/null @@ -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. - diff --git a/smt/theory_questions/5_1_smt_self.tex b/smt/theory_questions/5_1_smt_self.tex deleted file mode 100644 index ae56c3f..0000000 --- a/smt/theory_questions/5_1_smt_self.tex +++ /dev/null @@ -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. diff --git a/symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex b/symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex deleted file mode 100644 index 3af6ca1..0000000 --- a/symbolic_encoding/multiple_choice/2_1_symbrep_lect.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/symbolic_encoding/multiple_choice/2_1_symbrep_self.tex b/symbolic_encoding/multiple_choice/2_1_symbrep_self.tex deleted file mode 100644 index e924dbf..0000000 --- a/symbolic_encoding/multiple_choice/2_1_symbrep_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_10_kripke_self.tex b/symbolic_encoding/practical_questions/1_10_kripke_self.tex deleted file mode 100644 index 4f8f219..0000000 --- a/symbolic_encoding/practical_questions/1_10_kripke_self.tex +++ /dev/null @@ -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}. diff --git a/symbolic_encoding/practical_questions/1_1_kripke_lect.tex b/symbolic_encoding/practical_questions/1_1_kripke_lect.tex deleted file mode 100644 index a199b5d..0000000 --- a/symbolic_encoding/practical_questions/1_1_kripke_lect.tex +++ /dev/null @@ -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\}\}, $ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex b/symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex deleted file mode 100644 index 11f08e8..0000000 --- a/symbolic_encoding/practical_questions/1_1_kripke_lect_sol.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_1_kripke_self.tex b/symbolic_encoding/practical_questions/1_1_kripke_self.tex deleted file mode 100644 index 7771977..0000000 --- a/symbolic_encoding/practical_questions/1_1_kripke_self.tex +++ /dev/null @@ -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\}\}$. diff --git a/symbolic_encoding/practical_questions/1_1_symbrep.tex b/symbolic_encoding/practical_questions/1_1_symbrep.tex deleted file mode 100644 index 2ac3f2b..0000000 --- a/symbolic_encoding/practical_questions/1_1_symbrep.tex +++ /dev/null @@ -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}$. diff --git a/symbolic_encoding/practical_questions/1_1_symbrep_self.tex b/symbolic_encoding/practical_questions/1_1_symbrep_self.tex deleted file mode 100644 index 2ac3f2b..0000000 --- a/symbolic_encoding/practical_questions/1_1_symbrep_self.tex +++ /dev/null @@ -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}$. diff --git a/symbolic_encoding/practical_questions/1_2_kripke_lect.tex b/symbolic_encoding/practical_questions/1_2_kripke_lect.tex deleted file mode 100644 index 1d33b8b..0000000 --- a/symbolic_encoding/practical_questions/1_2_kripke_lect.tex +++ /dev/null @@ -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 \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex b/symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex deleted file mode 100644 index 87eeeb8..0000000 --- a/symbolic_encoding/practical_questions/1_2_kripke_lect_sol.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/1_2_kripke_self.tex b/symbolic_encoding/practical_questions/1_2_kripke_self.tex deleted file mode 100644 index 194a30a..0000000 --- a/symbolic_encoding/practical_questions/1_2_kripke_self.tex +++ /dev/null @@ -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} diff --git a/symbolic_encoding/practical_questions/1_2_symbrep_self.tex b/symbolic_encoding/practical_questions/1_2_symbrep_self.tex deleted file mode 100644 index 65d9ca2..0000000 --- a/symbolic_encoding/practical_questions/1_2_symbrep_self.tex +++ /dev/null @@ -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\}$. diff --git a/symbolic_encoding/practical_questions/1_3_kripke_self.tex b/symbolic_encoding/practical_questions/1_3_kripke_self.tex deleted file mode 100644 index 818e444..0000000 --- a/symbolic_encoding/practical_questions/1_3_kripke_self.tex +++ /dev/null @@ -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} diff --git a/symbolic_encoding/practical_questions/1_4_kripke_self.tex b/symbolic_encoding/practical_questions/1_4_kripke_self.tex deleted file mode 100644 index 6bc3ff4..0000000 --- a/symbolic_encoding/practical_questions/1_4_kripke_self.tex +++ /dev/null @@ -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} diff --git a/symbolic_encoding/practical_questions/2_05_symbrep_self.tex b/symbolic_encoding/practical_questions/2_05_symbrep_self.tex deleted file mode 100644 index b9b1458..0000000 --- a/symbolic_encoding/practical_questions/2_05_symbrep_self.tex +++ /dev/null @@ -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} diff --git a/symbolic_encoding/practical_questions/2_10_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_10_symbrep_lect.tex deleted file mode 100644 index a9ea243..0000000 --- a/symbolic_encoding/practical_questions/2_10_symbrep_lect.tex +++ /dev/null @@ -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} - - \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex deleted file mode 100644 index d6b73f7..0000000 --- a/symbolic_encoding/practical_questions/2_10_symbrep_lect_sol.tex +++ /dev/null @@ -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\}$. diff --git a/symbolic_encoding/practical_questions/2_10_symbrep_self.tex b/symbolic_encoding/practical_questions/2_10_symbrep_self.tex deleted file mode 100644 index b9d0410..0000000 --- a/symbolic_encoding/practical_questions/2_10_symbrep_self.tex +++ /dev/null @@ -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. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_11_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_11_symbrep_lect.tex deleted file mode 100644 index 0f137e4..0000000 --- a/symbolic_encoding/practical_questions/2_11_symbrep_lect.tex +++ /dev/null @@ -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$. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex deleted file mode 100644 index db46cc5..0000000 --- a/symbolic_encoding/practical_questions/2_11_symbrep_lect_sol.tex +++ /dev/null @@ -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$ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_11_symbrep_self.tex b/symbolic_encoding/practical_questions/2_11_symbrep_self.tex deleted file mode 100644 index 6438172..0000000 --- a/symbolic_encoding/practical_questions/2_11_symbrep_self.tex +++ /dev/null @@ -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} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_12_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_12_symbrep_lect.tex deleted file mode 100644 index e79edba..0000000 --- a/symbolic_encoding/practical_questions/2_12_symbrep_lect.tex +++ /dev/null @@ -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*} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_12_symbrep_self.tex b/symbolic_encoding/practical_questions/2_12_symbrep_self.tex deleted file mode 100644 index 81e580d..0000000 --- a/symbolic_encoding/practical_questions/2_12_symbrep_self.tex +++ /dev/null @@ -1,15 +0,0 @@ -\item \self Find a symbolic binary encoding for -$X = \{ 0,1, \ldots, 31 \}$. -Use it to compute formulas in propositional logic that symbolically represent the following sets. - -\begin{itemize} - \item $B =\{8, 9, 10, 11, 12, 13, 14, 15\}$ - \item $C =\{x \in X \mid 0 \leq x \leq 15\}$ -\end{itemize} - -Compute the characteristic functions of the following sets by symbolic operations, using your results from before. -\begin{enumerate} - \item $D = B \cup C$ - \item $E = B \cap C$ - \item $F = C \setminus B$ -\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_13_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_13_symbrep_lect.tex deleted file mode 100644 index 7c4e8d5..0000000 --- a/symbolic_encoding/practical_questions/2_13_symbrep_lect.tex +++ /dev/null @@ -1,24 +0,0 @@ -\item \lect Find a \textit{symbolic encoding} for 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} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex deleted file mode 100644 index bd9c552..0000000 --- a/symbolic_encoding/practical_questions/2_13_symbrep_lect_sol.tex +++ /dev/null @@ -1,15 +0,0 @@ -Using the variables $v_1$ and $v_0$, we can define the transition relation using the following formula:\\ -\begin{center} - $\lnot v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0) \ \lor$\\ - $\lnot v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0) \ \lor$\\ - $v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land v'_0) \ \lor$\\ - $v_1 \land v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor \lnot v'_1 \land v'_0 \lor v'_1 \land \lnot v'_0 \lor v'_1 \land v'_0)$ -\end{center} - -We can further simplify the formula to: -\begin{center} - $\lnot v_1 \land \lnot v_0 \lor$\\ - $\lnot v_1 \land v_0 \land (v'_0 \lor v'_1 \land \lnot v'_0) \ \lor$\\ - $v_1 \land \lnot v_0 \land (\lnot v'_1 \lor v'_1 \land v'_0) \ \lor$\\ - $v_1 \land v_0$ -\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_13_symbrep_self.tex b/symbolic_encoding/practical_questions/2_13_symbrep_self.tex deleted file mode 100644 index 7b8fe3c..0000000 --- a/symbolic_encoding/practical_questions/2_13_symbrep_self.tex +++ /dev/null @@ -1,15 +0,0 @@ -\item \self Find a symbolic binary encoding for -$X = \{ 0,1, \ldots, 31 \}$. -Use it to compute formulas in propositional logic that symbolically represent the following sets. -\begin{itemize} - \item $B =\{x \in X \mid \text{x is even}\}$ - \item $C =\{x \in X \mid \text{x is odd}\}$ - \item $D =\{0,1,2,3,4,5,6,7\}$ -\end{itemize} - -Compute the characteristic functions of the following sets by symbolic operations, using your results from before. -\begin{enumerate} - \item $E = B \cup D$ - \item $F = C \cap E$ - \item $G = E \setminus F$ -\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_17_symbrep_self.tex b/symbolic_encoding/practical_questions/2_17_symbrep_self.tex deleted file mode 100644 index 48dd31b..0000000 --- a/symbolic_encoding/practical_questions/2_17_symbrep_self.tex +++ /dev/null @@ -1,33 +0,0 @@ -\item \self Find a \textit{symbolic encoding} for the \textit{transition relation} of the following \textit{Kripke structure} and -simplify your formulas. The labels of the states symbolize their symbolic encoding. -E.g. "110" = "$x_2 \land x_1 \land \lnot x_0$", i.e. the least significant bit corresponds to $x_0$, -the second-least significant bit to $x_1$, and so forth. - -\begin{center} -\vspace{-2em} -\begin{tikzpicture}[auto, node distance=2cm,shorten >=1pt, -thick,node/.style={circle,draw,minimum size=25pt}] - \node[node] (s0) {$000$}; - \node[node] (s1) [above right of=s0] {$001$}; - \node[node] (s2) [right of=s1] {$010$}; - \node[node] (s3) [below right of=s2] {$011$}; - \node[node] (s4) [below of=s3] {$100$}; - \node[node] (s5) [below left of=s4] {$101$}; - \node[node] (s6) [left of=s5] {$110$}; - \node[node] (s7) [above left of=s6] {$111$}; - - - - \path[->] (s0) edge (s1); - \path[->] (s1) edge (s2); - \path[<->] (s2) edge (s3); - \path[->] (s3) edge (s4); - \path[->] (s4) edge (s7); - \path[->] (s7) edge (s6); - \path[<->] (s6) edge (s5); - \path[->] (s3) edge (s6); - \path[->] (s5) edge (s0); - \path[->] (s1.30) edge[bend right=90, looseness=15, out=240, in=300] (s1.60); - \path[->] (s4.30) edge[bend right=90, looseness=15, out=240, in=300] (s4.60); -\end{tikzpicture} -\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_18_symbrep_self.tex b/symbolic_encoding/practical_questions/2_18_symbrep_self.tex deleted file mode 100644 index e9ab01b..0000000 --- a/symbolic_encoding/practical_questions/2_18_symbrep_self.tex +++ /dev/null @@ -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*} - (v_1 \land v_0 \land \lnot v'_1 \land \neg v'_0) & \enspace \lor \\ - (\neg v_1 \land v_0 \land \lnot v'_1 \land v'_0) & \enspace \lor \\ - (v_1 \land v_0 \land v'_1 \land v'_0) & - \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_1_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_1_symbrep_lect.tex deleted file mode 100644 index 7d625ca..0000000 --- a/symbolic_encoding/practical_questions/2_1_symbrep_lect.tex +++ /dev/null @@ -1 +0,0 @@ -\item \lect Given a state space of size $|S| = 2^4 = 16$, give the symbolic encoding for the following states: (a) $s_{7}$, (b) $s_{15}$, and (c) $s_{10}$. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex deleted file mode 100644 index e574485..0000000 --- a/symbolic_encoding/practical_questions/2_1_symbrep_lect_sol.tex +++ /dev/null @@ -1,6 +0,0 @@ -For the symbolic encoding we need 4 Boolean variables, \{$v_3$, . . . , $v_0$\}. -Let $v_3$ be the most significant bit, and $v_0$ the least significant bit.\\ - -(a) $s_{7}$ = $\lnot v_3 \land v_2 \land v_1 \land v_0$\\ -(b) $s_{15}$ = $v_3 \land v_2 \land v_1 \land v_0$\\ -(c) $s_{10}$ = $v_3 \land \lnot v_2 \land v_1 \land \lnot v_0$ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_1_symbrep_self.tex b/symbolic_encoding/practical_questions/2_1_symbrep_self.tex deleted file mode 100644 index a6507b4..0000000 --- a/symbolic_encoding/practical_questions/2_1_symbrep_self.tex +++ /dev/null @@ -1,7 +0,0 @@ -\item \self Given a state space of the size $|S| = 2^{11} = 2048$, give the symbolic encoding for the following states: - -\begin{enumerate} - \item $s_{435}$ - \item $s_{1467}$ - \item $s_{2022}$ -\end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_20_symbrep_self.tex b/symbolic_encoding/practical_questions/2_20_symbrep_self.tex deleted file mode 100644 index a735070..0000000 --- a/symbolic_encoding/practical_questions/2_20_symbrep_self.tex +++ /dev/null @@ -1,9 +0,0 @@ -\item \self Build a \textit{Kripke structure} from the following symbolically encoded transition relations and draw the - corresponding graph: - - \begin{align*} - (\lnot x_2 \land \lnot x_1 \land \lnot x_0) \land (\lnot x_2' \land x_0') & \enspace \lor \\ - (\lnot x_2 \land x_1) \land ((x_2' \oplus x_1') \land x_0') & \enspace \lor \\ - (x_2 \land (x_1 \leftrightarrow x_0)) \land (x_2' \land (x_1' \oplus x_0')) & \enspace \lor \\ - (x_2 \land x_1 \land \lnot x_0) \land (x_2' \land (x_1' \lor x_0')) & - \end{align*} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_2_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_2_symbrep_lect.tex deleted file mode 100644 index 549492f..0000000 --- a/symbolic_encoding/practical_questions/2_2_symbrep_lect.tex +++ /dev/null @@ -1,2 +0,0 @@ -\item \lect Given is the set of states $S=\{s_0,\dots,s_7\}$. -Find formulas in propositional logic that symbolically represent the sets $A = \{s_7, s_6,s_3, s_2 \}$, $B=\{s_1, s_3,s_5, s_7\}$, and $C=\{s_7, s_6,s_0, s_1\}$. diff --git a/symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex deleted file mode 100644 index 02c3d2c..0000000 --- a/symbolic_encoding/practical_questions/2_2_symbrep_lect_sol.tex +++ /dev/null @@ -1,6 +0,0 @@ -$A = \{s_7, s_6,s_3, s_2 \}$ = $(v_2 \land v_1 \land v_0) \lor (v_2 \land v_1 \land \lnot v_0) \lor (\lnot v_2 \land v_1 \land v_0) \lor (\lnot v_2 \land v_1 \land \lnot v_0)$\\ -\hspace*{0,34cm} = $v_1$\\\\ -$B=\{s_1, s_3,s_5, s_7\}$ = $(\lnot v_2 \land \lnot v_1 \land v_0) \lor (\lnot v_2 \land v_1 \land v_0) \lor (v_2 \land \lnot v_1 \land v_0) \lor (v_2 \land v_1 \land v_0)$\\ -\hspace*{0,34cm} = $v_0$\\\\ -$C=\{s_7, s_6,s_0, s_1\}$ = $(v_2 \land v_1 \land v_0) \lor (v_2 \land v_1 \land \lnot v_0) \lor (\lnot v_2 \land \lnot v_1 \land \lnot v_0) \lor (\lnot v_2 \land \lnot v_1 \land v_0)$ \\ -\hspace*{0,34cm} = $(v_2 \land v_1) \lor (\lnot v_2 \land \lnot v_1)$ \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_2_symbrep_self.tex b/symbolic_encoding/practical_questions/2_2_symbrep_self.tex deleted file mode 100644 index 5841294..0000000 --- a/symbolic_encoding/practical_questions/2_2_symbrep_self.tex +++ /dev/null @@ -1,8 +0,0 @@ -\item \self Consider the following set of states defined by the valuations: -\begin{align*} - (v_0 \imp \top, v_1 \imp \top, v_2 \imp \top, v_3 \imp \bot), - (v_0 \imp \top, v_1 \imp \bot, v_2 \imp \top, v_3 \imp \bot),\\ - (v_0 \imp \top, v_1 \imp \bot, v_2 \imp \bot, v_3 \imp \bot), - (v_0 \imp \top, v_1 \imp \top, v_2 \imp \bot, v_3 \imp \bot), -\end{align*} -Represent this set of states symbolically using a propositional formula and simplify this formula as best as possible. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_3_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_3_symbrep_lect.tex deleted file mode 100644 index 0720fb4..0000000 --- a/symbolic_encoding/practical_questions/2_3_symbrep_lect.tex +++ /dev/null @@ -1,40 +0,0 @@ -\item \lect Consider the domain $A=\{Maths, \;English, \;Biology, \;Physical \; Education\}$ and - the two different symbolic encodings for $A$ given below. - Which one gives a shorter characteristic function for the following sets? - \begin{enumerate} - \item $B = \{Maths, \; Biology\}$ - \item $C = \{English, \; Biology\}$ - \item $D = \{Maths, \;Physical \; Education\}$ - \end{enumerate} - Illustrate your answer by giving the - characteristic function for $B$, $C$ and $D$ in both encodings. - -\vspace{.5cm} - -%\begin{minipage} - \begin{tabular}{l|l|l} - \hline - \multicolumn{3}{c}{\textbf{Encoding 1}} \\ - \hline - Element & x & y \\ - \hline - Maths & $0$ & $0$ \\ - English & $1$ & $0$ \\ - Biology & $0$ & $1$ \\ - Physical Education & $1$ & $1$ - \end{tabular} -%\end{minipage} -%\begin{minipage} -\hspace{3cm} - \begin{tabular}{l|l|l} - \hline - \multicolumn{3}{c}{\textbf{Encoding 2}} \\ - \hline - Element & x & y \\ - \hline - Maths & $0$ & $0$ \\ - English & $1$ & $0$ \\ - Biology & $1$ & $1$ \\ - Physical Education & $0$ & $1$ - \end{tabular} -%\end{minipage} diff --git a/symbolic_encoding/practical_questions/2_3_symbrep_self.tex b/symbolic_encoding/practical_questions/2_3_symbrep_self.tex deleted file mode 100644 index e52ce46..0000000 --- a/symbolic_encoding/practical_questions/2_3_symbrep_self.tex +++ /dev/null @@ -1,48 +0,0 @@ -\item \self Consider the domain $A=\{Asparagus, \;Bell \; Pepper, \;Cabbage, \;Tomato, \\ \; Onion, \;Zucchini, \;Eggplant, \; Mushroom\}$ and - the two different symbolic encodings for $A$ given below. - Which one gives a shorter characteristic function for the following sets? - \begin{enumerate} - \item $B = \{Asparagus, \; Mushroom\}$ - \item $C = \{Bell \; Pepper, \; Onion, \; Zucchini, \; Eggplant\}$ - \item $D = \{Cabbage, \; Tomato\}$ - \end{enumerate} - Illustrate your answer by giving the - characteristic function for $B$, $C$ and $D$ in both encodings. - -\vspace{.5cm} - -%\begin{minipage} - \begin{tabular}{l|l|l|l} - \hline - \multicolumn{3}{c}{\textbf{Encoding 1}} \\ - \hline - Element & x & y & z\\ - \hline - Asparagus & $0$ & $0$ & $0$ \\ - Bell Pepper & $0$ & $0$ & $1$ \\ - Cabbage & $0$ & $1$ & $0$ \\ - Tomato & $0$ & $1$ & $1$ \\ - Onion & $1$ & $0$ & $0$ \\ - Zucchini & $1$ & $0$ & $1$ \\ - Eggplant & $1$ & $1$ & $0$ \\ - Mushroom & $1$ & $1$ & $1$ - \end{tabular} -%\end{minipage} -%\begin{minipage} -\hspace{3cm} - \begin{tabular}{l|l|l|l} - \hline - \multicolumn{3}{c}{\textbf{Encoding 2}} \\ - \hline - Element & x & y & z \\ - \hline - Asparagus & $1$ & $1$ & $0$ \\ - Bell Pepper & $1$ & $0$ & $1$ \\ - Cabbage & $0$ & $1$ & $0$ \\ - Tomato & $1$ & $1$ & $1$ \\ - Onion & $0$ & $0$ & $0$ \\ - Zucchini & $0$ & $0$ & $1$ \\ - Eggplant & $1$ & $0$ & $0$ \\ - Mushroom & $0$ & $1$ & $1$ - \end{tabular} -%\end{minipage} diff --git a/symbolic_encoding/practical_questions/2_4_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_4_symbrep_lect.tex deleted file mode 100644 index 58c4515..0000000 --- a/symbolic_encoding/practical_questions/2_4_symbrep_lect.tex +++ /dev/null @@ -1,15 +0,0 @@ -\item \self The following table shows eight students and their means of transportation. Find a symbolic encodings representing the list of students. -For this encoding, give the symbolic representation of the set $B$ of all students that go by \emph{bike}, and the set $C$ of all students that go by \emph{car}. - - \begin{tabular}{l|l} - Name & Transportation \\ - \hline - Alice & Car \\ - Bob & Bike \\ - Carl & Tram \\ - David & Bike \\ - Eve & Tram \\ - Frank & Bike \\ - Greg & Tram \\ - Hank & Bike \\ - \end{tabular} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_4_symbrep_self.tex b/symbolic_encoding/practical_questions/2_4_symbrep_self.tex deleted file mode 100644 index ea247e3..0000000 --- a/symbolic_encoding/practical_questions/2_4_symbrep_self.tex +++ /dev/null @@ -1,17 +0,0 @@ -\item \self -Listed are the participants of a seminar as well as their choice of snacks. Find a symbolic encodings for the participants. -For for this encoding, give the symbolic representation of the set $B$ of all participants that ordered \emph{bananas}, and the set $C$ of all participants that ordered cake. - - \begin{tabular}{l|l} - Name & Snack \\ - \hline - Alice & banana \\ - Bob & cake \\ - Carl & banana \\ - David & banana \\ - Eve & cake \\ - Frank & cake \\ - Greg & orange \\ - Hank & cake \\ - \end{tabular} - diff --git a/symbolic_encoding/practical_questions/2_5_symbrep_self.tex b/symbolic_encoding/practical_questions/2_5_symbrep_self.tex deleted file mode 100644 index e84fc59..0000000 --- a/symbolic_encoding/practical_questions/2_5_symbrep_self.tex +++ /dev/null @@ -1,36 +0,0 @@ -\item \self -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, Italy\}$? 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} diff --git a/symbolic_encoding/practical_questions/2_6_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_6_symbrep_lect.tex deleted file mode 100644 index a654fb9..0000000 --- a/symbolic_encoding/practical_questions/2_6_symbrep_lect.tex +++ /dev/null @@ -1,2 +0,0 @@ -\item \self - Given a state space of size $|S| = 64$, find a symbolic binary encoding for this state space and compute the formulas that symbolically represent the sets of states $$B = \{s_{16}, s_{17}, s_{18}, ..., s_{32}\} \enspace \text{and} \enspace C = \{s_{24}, s_{25},, s_{26}, ..., s_{64}.\}$$ Then compute the formulas that symbolically represent the sets $D = B \cap C$ and $E = B \cup C$. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_6_symbrep_self.tex b/symbolic_encoding/practical_questions/2_6_symbrep_self.tex deleted file mode 100644 index 97cdec2..0000000 --- a/symbolic_encoding/practical_questions/2_6_symbrep_self.tex +++ /dev/null @@ -1,41 +0,0 @@ -\item \self Consider the following set operations and relations between - two sets $X$ and $Y$, and an element $a$: -\begin{enumerate} -\item Union: $X \cup Y$ -\item Intersection: $X \cap Y$ -\item Set Difference: $X \setminus Y$ -\item Containment: $a \in X$? -\item Subset: $X \subseteq Y$? -\item Strict Subset: $X \subset Y$? -\item Emptiness: $X=\emptyset$? -\item Equality: $X=Y$? -\end{enumerate} -Let $x$ and $y$ be the symbolic representations of $X$ and $Y$ -respectively, and let $\alpha$ be the symbolic encoding of element -$a$. For each of the following items, state which of the above -operations is performed, or which of the above questions is answered. -Write the letters of the corresponding operation/question into the -boxes of the items below. Note that some of the items below do not -perform any of the above operations or answer any of the above -questions. Put a ``--'' in the box of these items. Also note that -some of the items below might do the same computation or answer the -same question. -\begin{itemize} -\item[\Huge{$\square$}] $\neg x \vee y$ -\item[\Huge{$\square$}] $x \wedge y$ -\item[\Huge{$\square$}] $x\equiv \top$? -\item[\Huge{$\square$}] $x\equiv y$? -\item[\Huge{$\square$}] $(x \rightarrow y) \wedge (y \rightarrow - x)$? -\item[\Huge{$\square$}] $x\equiv \bot$? -\item[\Huge{$\square$}] $y \wedge \neg x$ -\item[\Huge{$\square$}] $x \rightarrow \bot$? -\item[\Huge{$\square$}] $\alpha \models x$? -\item[\Huge{$\square$}] $\alpha \models \neg x$? -\item[\Huge{$\square$}] $\neg \alpha \models x$? -\item[\Huge{$\square$}] $x \rightarrow \alpha$? -\item[\Huge{$\square$}] $y \rightarrow x$? -\item[\Huge{$\square$}] $x \rightarrow y$? -\item[\Huge{$\square$}] $(x \rightarrow y) \wedge (x\not \equiv - y)$? -\end{itemize} diff --git a/symbolic_encoding/practical_questions/2_7_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_7_symbrep_lect.tex deleted file mode 100644 index e61733e..0000000 --- a/symbolic_encoding/practical_questions/2_7_symbrep_lect.tex +++ /dev/null @@ -1,14 +0,0 @@ -\item \self Find a symbolic binary encoding for -$X = \{ 0,1, \ldots, 31 \}$. -Use it to compute formulas in propositional logic that symbolically represent the following sets. - - \begin{itemize} - \item $B =\{4, 5, 12, 13, 20, 21, 28, 29 \}$ - \item $C =\{1, 2, 13, 14 \}$ - \end{itemize} - - Compute the characteristic functions of the following sets by symbolic operations, using your results from before. - \begin{enumerate} - \item $D = B \cup C$ - \item $E = X \setminus D$ - \end{enumerate} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_7_symbrep_self.tex b/symbolic_encoding/practical_questions/2_7_symbrep_self.tex deleted file mode 100644 index c01c81d..0000000 --- a/symbolic_encoding/practical_questions/2_7_symbrep_self.tex +++ /dev/null @@ -1,37 +0,0 @@ -\item \self Consider the set $\mathbb{N}_{16} = \{0,1,2,3,\dots,14,15\}$. - Let $x_0$, $x_1$, $x_2$, and $x_3$ be propositional variables, - used for symbolic encoding of the elements of $\mathbb{N}_{16}$, - using standard binary encoding, with $x_0$ being the least - significant ($2^0$) bit, and $x_3$ being the most significant - ($2^3$) bit. - - Now, consider the following subsets of $\mathbb{N}_{16}$. - -\begin{itemize} -\item $A = \{0, 1, 2, 3\}$ -\item $B = \{0, 1, 2, 3, 4, 5, 6, 7\}$ -\item $C = \{0, 2, 4, 6, 8, 10, 12, 14\}$ -\item $D = \{8, 10, 12, 14\}$ -\item $E = \{3, 10\}$ -\item $F = \{ \}$ -\end{itemize} - -In the following list of formulas, write the letter of the set that -the formula encodes into the adjacent box. Note that some sets might -be encoded by more than one formula. Also note that some formulas -might not encode any of the above sets; write a ``--'' in the box of -such formulas. - -\begin{itemize} -\item[\Huge{$\square$}] $\bot$ -\item[\Huge{$\square$}] $\top$ -\item[\Huge{$\square$}] $(\neg x_3 \wedge \neg x_2 \wedge x_1 - \wedge x_0) \vee (x_3 \wedge \neg x_2 \wedge x_1 \wedge \neg - x_0)$ -\item[\Huge{$\square$}] $x_0$ -\item[\Huge{$\square$}] $\neg x_0$ -\item[\Huge{$\square$}] $x_3$ -\item[\Huge{$\square$}] $\neg x_3$ -\item[\Huge{$\square$}] $\neg x_3 \vee \neg x_2$ -\item[\Huge{$\square$}] $\neg x_3 \wedge \neg x_2$ -\end{itemize} diff --git a/symbolic_encoding/practical_questions/2_8_symbrep_self.tex b/symbolic_encoding/practical_questions/2_8_symbrep_self.tex deleted file mode 100644 index 2b8ff64..0000000 --- a/symbolic_encoding/practical_questions/2_8_symbrep_self.tex +++ /dev/null @@ -1 +0,0 @@ -\item \self Given a state space of size $|S| = 2048$, find a symbolic binary encoding for this state space and compute the characteristic function for the sets of states $$B = \{s_0, s_1, s_2, ..., s_{1023}\} \enspace \text{and} \enspace C = \{s_{512}, s_{513},, s_{514}, ..., s_{1535}.\}$$ Then compute the characteristic function for the sets $D = B \cup C$ and $E = B \setminus C$. If possible, simplify the formulas. \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_9_symbrep_lect.tex b/symbolic_encoding/practical_questions/2_9_symbrep_lect.tex deleted file mode 100644 index 465e531..0000000 --- a/symbolic_encoding/practical_questions/2_9_symbrep_lect.tex +++ /dev/null @@ -1,24 +0,0 @@ -\item \lect Find a \textit{symbolic encoding} for 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} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex b/symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex deleted file mode 100644 index d8af7cc..0000000 --- a/symbolic_encoding/practical_questions/2_9_symbrep_lect_sol.tex +++ /dev/null @@ -1,13 +0,0 @@ -Using the variables $v_1$ and $v_0$, we can define the transition relation using the following formula:\\ -\begin{center} - $\lnot v_1 \land \lnot v_0 \land (\lnot v'_1 \land \lnot v'_0 \lor v'_1 \land \lnot v'_0) \ \lor$\\ - $\lnot v_1 \land v_0 \land v'_1 \land v'_0 \ \lor$\\ - $v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor \lnot v'_1 \land \lnot v'_0 \lor v'_1 \land \lnot v'_0)$\\ -\end{center} - -We can further simplify the formula to: -\begin{center} - $\lnot v_1 \land \lnot v_0 \land \lnot v'_0 \ \lor$\\ - $\lnot v_1 \land v_0 \land v'_1 \land v'_0 \ \lor$\\ - $v_1 \land v_0 \land (\lnot v'_1 \land v'_0 \lor \lnot v'_0)$\\ -\end{center} \ No newline at end of file diff --git a/symbolic_encoding/practical_questions/2_9_symbrep_self.tex b/symbolic_encoding/practical_questions/2_9_symbrep_self.tex deleted file mode 100644 index 84a036d..0000000 --- a/symbolic_encoding/practical_questions/2_9_symbrep_self.tex +++ /dev/null @@ -1,3 +0,0 @@ -\item \self Given a state space of size $|S| = 64$. Find a symbolic binary encoding for this state space and compute the formulas that symbolically represent the sets $$B = \{s_{32}, s_{33}, s_{34}, ..., s_{63}\} \enspace \text{and} \enspace C = \{s_{16}, s_{17},, s_{18}, ..., s_{40}\}.$$ - -Following, compute the formulas that represent the sets $D = B \cap C$, $E = B \cup C$, $F = B \setminus C$ and $G = C \setminus B$. \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/0_1_symb_lect.tex b/symbolic_encoding/theory_questions/0_1_symb_lect.tex deleted file mode 100644 index 68acaa3..0000000 --- a/symbolic_encoding/theory_questions/0_1_symb_lect.tex +++ /dev/null @@ -1 +0,0 @@ -\item \lect Given the term \textit{state} within a reactive system, what does a \textit{state} do? \underline{rausnehmen?} \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/0_1_symb_self.tex b/symbolic_encoding/theory_questions/0_1_symb_self.tex deleted file mode 100644 index 40bc701..0000000 --- a/symbolic_encoding/theory_questions/0_1_symb_self.tex +++ /dev/null @@ -1 +0,0 @@ -\item \self Given the term \textit{transition} within a reactive system, what does the term \textit{transition} mean? How can a \textit{transition} be determined? \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/1_0_kripke_self.tex b/symbolic_encoding/theory_questions/1_0_kripke_self.tex deleted file mode 100644 index 64df842..0000000 --- a/symbolic_encoding/theory_questions/1_0_kripke_self.tex +++ /dev/null @@ -1,2 +0,0 @@ -\item \self - Give the definition of a \emph{transition system} $\mathcal{T}$ and an example. diff --git a/symbolic_encoding/theory_questions/2_01_symbrep_self.tex b/symbolic_encoding/theory_questions/2_01_symbrep_self.tex deleted file mode 100644 index ce68361..0000000 --- a/symbolic_encoding/theory_questions/2_01_symbrep_self.tex +++ /dev/null @@ -1,3 +0,0 @@ -\item \self What is the main advantage of symbolic set operations over - non-symbolic operations that enumerate all set elements - explicitly? diff --git a/symbolic_encoding/theory_questions/2_1_symbrep_self.tex b/symbolic_encoding/theory_questions/2_1_symbrep_self.tex deleted file mode 100644 index 27de2fb..0000000 --- a/symbolic_encoding/theory_questions/2_1_symbrep_self.tex +++ /dev/null @@ -1 +0,0 @@ -\item \self Considering the \textit{representation of a single state}, for a given valuation, we can write a formula that is true for exactly that evaluation. How can in contrast the \textit{representation of sets of states} be defined? Give a small example of such a representation. \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/2_2_symbrep_self.tex b/symbolic_encoding/theory_questions/2_2_symbrep_self.tex deleted file mode 100644 index 054efd0..0000000 --- a/symbolic_encoding/theory_questions/2_2_symbrep_self.tex +++ /dev/null @@ -1,4 +0,0 @@ -\item \self Assume you are given the formulas $a$ and - $b$, which symbolically represent the sets $A$ and $B$, - respectively. Give the formula - $c$, which symbolically represents the set $C= A \setminus B$. diff --git a/symbolic_encoding/theory_questions/2_3_symbrep_lect.tex b/symbolic_encoding/theory_questions/2_3_symbrep_lect.tex deleted file mode 100644 index debc912..0000000 --- a/symbolic_encoding/theory_questions/2_3_symbrep_lect.tex +++ /dev/null @@ -1 +0,0 @@ -\item \lect Given a \textit{set of ordered pairs of states}, how can a transition relation of a \textit{transition system} be symbolically represented? Explain which sets of variables you need and give an example of such a representation. \ No newline at end of file diff --git a/symbolic_encoding/theory_questions/2_3_symbrep_self.tex b/symbolic_encoding/theory_questions/2_3_symbrep_self.tex deleted file mode 100644 index 115d9de..0000000 --- a/symbolic_encoding/theory_questions/2_3_symbrep_self.tex +++ /dev/null @@ -1,5 +0,0 @@ -\item \self Assume you are given the formulas $a$ and - $b$, which symbolically represent the sets $A$ and $B$, - respectively. What would you have to check on $a, b$ to test - whether or not $A$ is a strict subset of $B$, i.e., $A \subset - B$?