Browse Source

added chapter three and four to the questionnaire

main
Stefan Pranger 2 months ago
parent
commit
e082dc41d4
  1. 4
      .drone.yml
  2. 10
      3_sat_solvers_dpll/0001.tex
  3. 35
      3_sat_solvers_dpll/0001_sol.tex
  4. 2
      3_sat_solvers_dpll/0002.tex
  5. 14
      3_sat_solvers_dpll/0002_sol.tex
  6. 9
      3_sat_solvers_dpll/0003.tex
  7. 21
      3_sat_solvers_dpll/0003_sol.tex
  8. 2
      3_sat_solvers_dpll/0004.tex
  9. 1
      3_sat_solvers_dpll/0004_sol.tex
  10. 1
      3_sat_solvers_dpll/0005.tex
  11. 2
      3_sat_solvers_dpll/0005_sol.tex
  12. 10
      3_sat_solvers_dpll/0006.tex
  13. 20
      3_sat_solvers_dpll/0006_sol.tex
  14. 1
      3_sat_solvers_dpll/0007.tex
  15. 7
      3_sat_solvers_dpll/0007_sol.tex
  16. 34
      3_sat_solvers_dpll/0008.tex
  17. 11
      3_sat_solvers_dpll/0008_sol.tex
  18. 10
      3_sat_solvers_dpll/0009.tex
  19. 89
      3_sat_solvers_dpll/0009_sol.tex
  20. 11
      3_sat_solvers_dpll/0010.tex
  21. 71
      3_sat_solvers_dpll/0010_sol.tex
  22. 12
      3_sat_solvers_dpll/0011.tex
  23. 92
      3_sat_solvers_dpll/0011_graphs.tex
  24. 107
      3_sat_solvers_dpll/0011_sol.tex
  25. 1
      3_sat_solvers_dpll/1001.tex
  26. 1
      3_sat_solvers_dpll/1002.tex
  27. 5
      3_sat_solvers_dpll/1003.tex
  28. 10
      3_sat_solvers_dpll/1004.tex
  29. 2
      3_sat_solvers_dpll/1005.tex
  30. 9
      3_sat_solvers_dpll/1006.tex
  31. 2
      3_sat_solvers_dpll/1007.tex
  32. 9
      3_sat_solvers_dpll/1008.tex
  33. 15
      3_sat_solvers_dpll/1009.tex
  34. 2
      3_sat_solvers_dpll/1010.tex
  35. 11
      3_sat_solvers_dpll/1011.tex
  36. 2
      3_sat_solvers_dpll/1012.tex
  37. 3
      3_sat_solvers_dpll/1013.tex
  38. 11
      3_sat_solvers_dpll/1014.tex
  39. 3
      3_sat_solvers_dpll/1015.tex
  40. 1
      3_sat_solvers_dpll/1016.tex
  41. 33
      3_sat_solvers_dpll/1017.tex
  42. 16
      3_sat_solvers_dpll/1018.tex
  43. 11
      3_sat_solvers_dpll/1019.tex
  44. 12
      3_sat_solvers_dpll/1020.tex
  45. 13
      3_sat_solvers_dpll/1021.tex
  46. 12
      3_sat_solvers_dpll/1022.tex
  47. 12
      3_sat_solvers_dpll/1023.tex
  48. 11
      3_sat_solvers_dpll/1024.tex
  49. 13
      3_sat_solvers_dpll/1025.tex
  50. 12
      3_sat_solvers_dpll/1026.tex
  51. 12
      3_sat_solvers_dpll/1027.tex
  52. 10
      3_sat_solvers_dpll/1028.tex
  53. 10
      3_sat_solvers_dpll/1029.tex
  54. 2
      3_sat_solvers_dpll/1030.tex
  55. 3
      3_sat_solvers_dpll/1030_sol.tex
  56. 1
      3_sat_solvers_dpll/1031.tex
  57. 1
      3_sat_solvers_dpll/1031_sol.tex
  58. 2
      3_sat_solvers_dpll/2002.tex
  59. 9
      3_sat_solvers_dpll/2002_sol.tex
  60. 2
      3_sat_solvers_dpll/2003.tex
  61. 31
      3_sat_solvers_dpll/2003_sol.tex
  62. 1
      3_sat_solvers_dpll/2004.tex
  63. 31
      3_sat_solvers_dpll/2004_sol.tex
  64. 3
      3_sat_solvers_dpll/3001.tex
  65. 4
      3_sat_solvers_dpll/3002.tex
  66. 7
      3_sat_solvers_dpll/3003.tex
  67. 7
      3_sat_solvers_dpll/3004.tex
  68. 8
      3_sat_solvers_dpll/3005.tex
  69. 8
      3_sat_solvers_dpll/3006.tex
  70. 15
      3_sat_solvers_dpll/3007.tex
  71. 15
      3_sat_solvers_dpll/3008.tex
  72. 11
      3_sat_solvers_dpll/3009.tex
  73. 11
      3_sat_solvers_dpll/3011.tex
  74. 11
      3_sat_solvers_dpll/3012.tex
  75. 11
      3_sat_solvers_dpll/3013.tex
  76. 17
      3_sat_solvers_dpll/3014.tex
  77. 17
      3_sat_solvers_dpll/3015.tex
  78. 16
      3_sat_solvers_dpll/3016.tex
  79. 16
      3_sat_solvers_dpll/3017.tex
  80. 1
      3_sat_solvers_dpll/3018.tex
  81. 6
      3_sat_solvers_dpll/3019.tex
  82. 1
      3_sat_solvers_dpll/3021.tex
  83. 1
      3_sat_solvers_dpll/3022.tex
  84. 26
      3_sat_solvers_dpll/3023.tex
  85. 1
      3_sat_solvers_dpll/3024.tex
  86. 27
      3_sat_solvers_dpll/3025.tex
  87. 13
      3_sat_solvers_dpll/4001.tex
  88. 16
      3_sat_solvers_dpll/4002.tex
  89. 16
      3_sat_solvers_dpll/4003.tex
  90. 14
      3_sat_solvers_dpll/4004.tex
  91. 15
      3_sat_solvers_dpll/4005.tex
  92. 244
      3_sat_solvers_dpll/sat_solvers_dpll.tex
  93. 1
      4_tseitin/0001.tex
  94. 3
      4_tseitin/0001_sol.tex
  95. 1
      4_tseitin/0002.tex
  96. 12
      4_tseitin/0002_sol.tex
  97. 4
      4_tseitin/0003.tex
  98. 4
      4_tseitin/0003_sol.tex
  99. 2
      4_tseitin/0004.tex
  100. 27
      4_tseitin/0004_sol.tex

4
.drone.yml

@ -51,7 +51,9 @@ steps:
api_key:
from_secret: gitea_token
files:
- questionnaire_three.pdf
- questionnaire_with_solutions_three.pdf
- questionnaire_with_spacing_three.pdf
when:
ref:
include:
@ -64,7 +66,9 @@ steps:
api_key:
from_secret: gitea_token
files:
- questionnaire_four.pdf
- questionnaire_with_solutions_four.pdf
- questionnaire_with_spacing_four.pdf
when:
ref:
include:

10
3_sat_solvers_dpll/0001.tex

@ -0,0 +1,10 @@
\item \lect Use the DPLL algorithm (\emph{without} BCP, PL and clause learning) to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor b)$
\item $(\lnot b \lor c)$
\item $(\lnot c \lor d)$
\item $(\lnot d \lor e)$
\item $(\lnot e \lor \lnot a)$
\end{enumerate}

35
3_sat_solvers_dpll/0001_sol.tex

@ -0,0 +1,35 @@
DPLL algorithm:
\scalebox{0.97}{
\setlength\tabcolsep{3pt}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|c|}
\hline
Step & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 \\ \hline \hline
Decision Level & 0 & 1 & 2 & 3 & 4 & 5 & 5 & 4 & 3 & 2 \\ \hline
Assignment & - & $a$ & $a,b$ & $a,b,c$ & $a,b,c,d$ & $a,b,c,d,e$ & $a,b,c,d, \lnot e$ & $a,b,c,\lnot d$ & $a,b,\lnot c$ & $a,\lnot b$ \\ \hline
Cl. 1: $\lnot a, b$ & 1 & $b$ & \cmark & \cmark & \cmark & \cmark & \cmark & \cmark & \cmark & $\{\}$ \xmark \\ \hline
Cl. 2: $\lnot b, c$ & 2 & 2 & $c$ & \cmark & \cmark & \cmark & \cmark & \cmark & $\{\}$ \xmark & \cmark \\ \hline
Cl. 3: $\lnot c, d$ & 3 & 3 & 3 & $d$ & \cmark & \cmark & \cmark & $\{\}$ \xmark & \cmark & 3 \\ \hline
Cl. 4: $\lnot d, e$ & 4 & 4 & 4 & 4 & $e$ & \cmark & $\{\}$ \xmark & \cmark & 4 & 4 \\ \hline
Cl. 5: $\lnot e, \lnot a$ & 5 &$\lnot e$&$\lnot e$ & $\lnot e$ & $\lnot e$ & $\{\}$ \xmark & \cmark & $\lnot e$ & $\lnot e$ & $\lnot e$ \\ \hline \hline
Decision &$a$&$b$ & $c$ & $d$ & $e$ & $\lnot e$ & $\lnot d$ & $\lnot c$ & $\lnot b$ & $\lnot a$ \\ \hline
\end{tabular}}
\scalebox{0.97}{
\setlength\tabcolsep{3pt}
\begin{tabular}{|l|c|c|c|c|c|}
\hline
Step & 11 & 12 & 13 & 14 & 15 \\ \hline \hline
Decision Level & 1 & 2 & 3 & 4 & 5 \\ \hline
Assignment & $\lnot a$ & $\lnot a, b$ & $\lnot a, b, c$ & $\lnot a, b, c, d$ & $\lnot a, b, c, d, e$ \\ \hline
Cl. 1: $\lnot a, b$ & \cmark & \cmark & \cmark & \cmark & \cmark \\ \hline
Cl. 2: $\lnot b, c$ & 2 & $c$ & \cmark & \cmark & \cmark \\ \hline
Cl. 3: $\lnot c, d$ & 3 & 3 & $d$ & \cmark & \cmark \\ \hline
Cl. 4: $\lnot d, e$ & 4 & 4 & 4 & $e$ & \cmark \\ \hline
Cl. 5: $\lnot e, \lnot a$ & \cmark & \cmark & \cmark & \cmark & \cmark \\ \hline \hline
Decision & $b$ & $c$ & $d$ & $e$ & SAT \\ \hline
\end{tabular}}
Model:
$a$ = F, $b$ = T, $c$ = T, $d$ = T, $e$ = T

2
3_sat_solvers_dpll/0002.tex

@ -0,0 +1,2 @@
\item \lect In the context of the DPLL algorithm, explain what a
\emph{Unit Clause} is. Give an example.

14
3_sat_solvers_dpll/0002_sol.tex

@ -0,0 +1,14 @@
\textbf{Definition - Unit Clause.} A clause $c$ is said to be a unit clause
under some assignment $A$ if the following two conditions hold:
\begin{enumerate}
\item The clause $c$ is not satisfied by $A$.
\item All but one of the variables in $c$ are given a value by $A$.
\end{enumerate}
Therefore, there is a single literal left in the set representing the clause under the assignment.
An example would be:
\begin{itemize}
\item $c = \lnot a, b, c$
\item $A = \{\lnot a, c\}$
\end{itemize}

9
3_sat_solvers_dpll/0003.tex

@ -0,0 +1,9 @@
\item \lect Use the DPLL algorithm with \textit{Boolean Constrain Propagation} (\emph{without} PL and clause learning) to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor b)$
\item $(\lnot b \lor c)$
\item $(\lnot c \lor d)$
\item $(\lnot d \lor e)$
\item $(\lnot e \lor \lnot a)$
\end{enumerate}

21
3_sat_solvers_dpll/0003_sol.tex

@ -0,0 +1,21 @@
DPLL algorithm:
\scalebox{0.9}{
\setlength\tabcolsep{3pt}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|c|c|}
\hline
Step & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 11 \\ \hline \hline
Decision Level & 0 & 1 & 1 & 1 & 1 & 1 & 1 & 2 & 2 & 2 & 2 \\ \hline
Assignment & - & $a$ & $a,b$ & $a,b,c$ & $a,b,c,d$ & $a,b,c,d,e$ & $\lnot a$ & $\lnot a, b$ & $\lnot a,b,c$ & $\lnot a,b,c,d$ & $\lnot a,b,c,d,e$ \\ \hline
Cl. 1: $\lnot a, b$ & 1 & $b$ & \cmark & \cmark & \cmark & \cmark & \cmark & \cmark & \cmark & \cmark & \cmark \\ \hline
Cl. 2: $\lnot b, c$ & 2 & 2 & $c$ & \cmark & \cmark & \cmark & 2 & $c$ & \cmark & \cmark & \cmark \\ \hline
Cl. 3: $\lnot c, d$ & 3 & 3 & 3 & $d$ & \cmark & \cmark & 3 & 3 & $d$ & \cmark & \cmark \\ \hline
Cl. 4: $\lnot d, e$ & 4 & 4 & 4 & 4 & $e$ & \cmark & 4 & 4 & 4 & $e$ & \cmark \\ \hline
Cl. 5: $\lnot e, \lnot a$ & 5 &$\lnot e$& $\lnot e$ & $\lnot e$ & $\lnot e$ & $\{\}$ \xmark & \cmark & \cmark & \cmark & \cmark & \cmark \\ \hline \hline
BCP & - & $b$ & $c$ & $d$ & $e$ & - & - & $c$ & $d$ & $e$ & \cmark \\ \hline
Decision &$a$& - & - & - & - & $\lnot a$ & $b$ & - & - & - & SAT \\ \hline
\end{tabular}}
Model:
$a$ = F, $b$ = T, $c$ = T, $d$ = T, $e$ = T

2
3_sat_solvers_dpll/0004.tex

@ -0,0 +1,2 @@
\item \lect In the context of the DPLL algorithm, explain what a
\emph{Pure Literal} is. Give an example.

1
3_sat_solvers_dpll/0004_sol.tex

@ -0,0 +1 @@
\textbf{Definition - Pure Literal.} A literal is \emph{pure} if its negation does not appear in the formula.

1
3_sat_solvers_dpll/0005.tex

@ -0,0 +1 @@
\item \lect In the context of the DPLL algorithm, explain why it is advantageous to apply \textit{Boolean Constrain Propagation (BCP)} and \textit{Pure Literals (PL)} before making a decision.

2
3_sat_solvers_dpll/0005_sol.tex

@ -0,0 +1,2 @@
Boolean Constraint Propagation and Pure Literals are so-called heuristics. BCP and PL capture when the choices we can make are restricted in two different ways.
It is advantageous to apply these heuristics before making a decision, since it reduces the amount of different assignments we have to check.

10
3_sat_solvers_dpll/0006.tex

@ -0,0 +1,10 @@
\item \lect Use the DPLL algorithm with \textit{Boolean Constrain Propagation} and \textit{Pure Literals} (\emph{without} clause learning) to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor b)$
\item $(\lnot b \lor c)$
\item $(\lnot c \lor d)$
\item $(\lnot d \lor e)$
\item $(\lnot e \lor \lnot a)$
\end{enumerate}

20
3_sat_solvers_dpll/0006_sol.tex

@ -0,0 +1,20 @@
DPLL algorithm:
\begin{tabular}{|l|c|c|c|c|c|}
\hline
Step & 1 & 2 & 3 & 4 & 5 \\ \hline \hline
Decision Level & 0 & 0 & 0 & 0 & 0 \\ \hline
Assignment & - & $\lnot a$ & $\lnot a,\lnot b$ & $\lnot a,\lnot b,\lnot c$ & $\lnot a,\lnot b,\lnot c,\lnot d$ \\ \hline
Cl. 1: $\lnot a, b$ & 1 & \cmark & \cmark & \cmark & \cmark \\ \hline
Cl. 2: $\lnot b, c$ & 2 & 2 & \cmark & \cmark & \cmark \\ \hline
Cl. 3: $\lnot c, d$ & 3 & 3 & 3 & \cmark & \cmark \\ \hline
Cl. 4: $\lnot d, e$ & 4 & 4 & 4 & 4 & \cmark \\ \hline
Cl. 5: $\lnot e, \lnot a$ & 5 &\cmark& \cmark & \cmark& \cmark\\ \hline \hline
BCP & - & - & - & - & - \\ \hline
PL & $\lnot a$ & $\lnot b$ & $\lnot c$ & $\lnot d$ & - \\ \hline
Decision & - & - & - & - & SAT \\ \hline
\end{tabular}
Model:
$a$ = F, $b$ = F, $c$ = F, $d$ = F, $e$ = F

1
3_sat_solvers_dpll/0007.tex

@ -0,0 +1 @@
\item \lect In the context of the DPLL algorithm, explain what \emph{Conflict-Driven Clause Learning} is and why most modern SAT solvers use this technique.

7
3_sat_solvers_dpll/0007_sol.tex

@ -0,0 +1,7 @@
\emph{The idea of conflict-driven clause learning is not to repeat steps that lead to a conflict}. % this is a quote from the lecture notes
\vspace{0.5cm}
When executing the DPLL algorithm we can maintain a so-called conflict graph. We can use this graph to deduce which variables lead to a conflict.
In Conflict-Driven Clause Learning different SAT solvers apply different techniques to extract new \emph{learned} clauses from this graph.
The learned clauses help the SAT solver to no repeat mistakes in different execution branches.

34
3_sat_solvers_dpll/0008.tex

@ -0,0 +1,34 @@
\item \lect Consider the following conflict graph with the following set of clauses:
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node[base node] (1) {$a$};
\node[base node] (2) [below of=1]{$\lnot b$};
\node[base node] (3) [right of=1] {$\lnot c$};
\node[base node] (4) [right of=2] {$d$};
\node[base node] (5) [right of=3] {$\lnot e$};
\node[base node] (6) [right of=4] {$e$};
\node[base node] (7) [right of=5] {$\bot$};
\path[]
(1) edge [] node {$1$} (3)
(2) edge [] node {$3$} (4)
(4) edge [] node {$1$} (3)
(3) edge [] node {$6$} (5)
edge [] node {$7$} (6)
(5) edge [] node {} (7)
(6) edge [] node {} (7);
\end{tikzpicture}
\begin{enumerate}[{Clause} 1:]
\item $\{\lnot a, \lnot c, \lnot d\}$
\item $\{a, \lnot d\}$
\item $\{b, d\}$
\item $\{\lnot b, d, e\}$
\item $\{\lnot b, \lnot e\}$
\item $\{c, \lnot e\}$
\item $\{c, e\}$
\end{enumerate}
Give the resolution proof for the given conflict graph and clauses and state the clause to be learned from the conflict.

11
3_sat_solvers_dpll/0008_sol.tex

@ -0,0 +1,11 @@
\begin{prooftree}
\AxiomC{$ \circled{6} \; c \lor \lnot e$}
\AxiomC{$ \circled{7} \; c \lor e$}
\BinaryInfC{$c$}
\AxiomC{$\circled{1} \; \lnot a \lor \lnot c \lor \lnot d$}
\BinaryInfC{$\lnot a \lor \lnot d$}
\AxiomC{$\circled{3} \; b \lor d$}
\BinaryInfC{$\lnot a \lor b$}
\end{prooftree}
The new learned clause is therefore Cl. 8: $\lnot a \lor b$

10
3_sat_solvers_dpll/0009.tex

@ -0,0 +1,10 @@
\item \lect \dpllDescription{negative}
\begin{enumerate}[{Clause} 1:]
\item $\{\lnot a,\lnot b\}$
\item $\{a,c\}$
\item $\{b,\lnot c\}$
\item $\{\lnot b,d\}$
\item $\{\lnot c,\lnot d\}$
\item $\{c,e\}$
\item $\{c,\lnot e\}$
\end{enumerate}

89
3_sat_solvers_dpll/0009_sol.tex

@ -0,0 +1,89 @@
DPLL algorithm:
\scalebox{1}{
\setlength\tabcolsep{3pt}
\begin{tabular}{|l|c|c|c|c|c|c|c|c|c|c|}
\hline
Step & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 \\ \hline \hline
Decision Level & 0 & 1 & 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 \\ \hline
Assignment & - & $\lnot a$& $\lnot a,c$ & $\lnot a,b,c$ & $\lnot a,b,c,\lnot d$& - & $a$ &$a,\lnot b$ &$a,\lnot b,\lnot c$& $a,\lnot b,\lnot c,\lnot e$ \\ \hline
Cl. 1: $\lnot a,\lnot b$ & 1 & \cmark & \cmark & \cmark & \cmark & 1 & $\lnot b$ & \cmark & \cmark & \cmark \\ \hline
Cl. 2: $ a,c$ & 2 & $c$ & \cmark & \cmark & \cmark & 2 & \cmark & \cmark & \cmark & \cmark \\ \hline
Cl. 3: $b,\lnot c$ & 3 & 3 & $b$ & \cmark & \cmark & 3 & 3 & $\lnot c$ & \cmark & \cmark \\ \hline
Cl. 4: $\lnot b,d$ & 4 & 4 & 4 & $d$ & $\{\}$ \xmark & 4 & 4 & \cmark & \cmark & \cmark \\ \hline
Cl. 5: $\lnot c,\lnot d$ & 5 & 5 & $\lnot d$ & $\lnot d$ & \cmark & 5 & 5 & 5 & \cmark & \cmark \\ \hline
Cl. 6: $c,e$ & 6 & 6 & \cmark & \cmark & \cmark & 6 & 6 & 6 & $e$ & $\{\}$ \xmark \\ \hline
Cl. 7: $c,\lnot e$ & 7 & 7 & \cmark & \cmark & \cmark & 7 & 7 & 7 & $\lnot e$ & \cmark \\ \hline
\textcolor{gray}{Cl. 8: $a$}& - & - & - & - & learned $a$ & 8 & \cmark & \cmark & \cmark & \cmark \\ \hline \hline
BCP & - & $c$ & $b$ & $\lnot d$ & - & $a$ & $\lnot b$ & $\lnot c$ & $\lnot e$ & - \\ \hline
PL & - & - & - & - & - & - & - & - & - & - \\ \hline
Decision & $\lnot a$& - & - & - & - & - & - & - & - & UNSAT \\ \hline
\end{tabular}}
Ad 5:
\begin{center}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node[base node] (1) {$\lnot a$};
\node[base node] (2) [right of=1]{$c$};
\node[base node] (3) [below right of=2] {$\lnot d$};
\node[base node] (4) [above right of=2] {$b$};
\node[base node] (5) [right of=4] {$d$};
\node[base node] (6) [below right of=5] {$\bot$};
\path[]
(1) edge [] node {$2$} (2)
(2) edge [] node {$5$} (3)
edge [] node {$3$} (4)
(4) edge [] node {$4$} (5)
(5) edge [] node {} (6)
(3) edge [] node {} (6);
\end{tikzpicture}
\end{center}
\begin{prooftree}
\AxiomC{$4. \; \lnot b \lor d$}
\AxiomC{$5. \; \lnot c \lor \lnot d$}
\BinaryInfC{$\lnot b \lor \lnot c$}
\AxiomC{$3. \; b \lor \lnot c$}
\BinaryInfC{$\lnot c$}
\AxiomC{$2. \; a \lor c$}
\BinaryInfC{$a$}
\end{prooftree}
Ad 10:
\begin{center}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node (0) {};
\node[base node] (1) [right of=0]{$a$};
\node[base node] (2) [right of=1]{$\lnot b$};
\node[base node] (3) [right of=2] {$\lnot c$};
\node[base node] (4) [above right of=3] {$\lnot e$};
\node[base node] (5) [below right of=3] {$e$};
\node[base node] (6) [above right of=5] {$\bot$};
\path[]
(0) edge [] node {$8$} (1)
(1) edge [] node {$1$} (2)
(2) edge [] node {$3$} (3)
(3) edge [] node {$7$} (4)
edge [] node {$6$} (5)
(4) edge [] node {} (6)
(5) edge [] node {} (6);
\end{tikzpicture}
\end{center}
\begin{prooftree}
\AxiomC{$6. \; c \lor e$}
\AxiomC{$7. \; c \lor \lnot e$}
\BinaryInfC{$c$}
\AxiomC{$3. \; b \lor \lnot c$}
\BinaryInfC{$b$}
\AxiomC{$1. \; \lnot a \lor \lnot b$}
\BinaryInfC{$\lnot a$}
\AxiomC{$8. \; a$}
\BinaryInfC{$\bot$}
\end{prooftree}

11
3_sat_solvers_dpll/0010.tex

@ -0,0 +1,11 @@
\item \lect Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor d)$
\item $(\lnot d \lor c)$
\item $(\lnot b \lor e)$
\item $(\lnot b \lor \lnot e)$
\item $(b \lor f)$
\item $(b \lor \lnot f)$
\end{enumerate}

71
3_sat_solvers_dpll/0010_sol.tex

@ -0,0 +1,71 @@
DPLL algorithm:
\scalebox{1}{
\begin{tabular}{|l|c|c|c|c|c|c|c|c|}
\hline
Step & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ \hline \hline
Decision Level & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 0 \\ \hline
Assignment & - & $\lnot a$ & $\lnot a,c$ & $\lnot a,b,c$ & $\lnot a,b,c,e$ & - & $\lnot b$ & $\lnot b, f$ \\ \hline
Cl. 1: $\lnot a,d$ & 1 & \cmark & \cmark & \cmark & \cmark & 1 & 1 & 1 \\ \hline
Cl. 2: $\lnot d,c$ & 2 & 2 & \cmark & \cmark & \cmark & 2 & 2 & 2 \\ \hline
Cl. 3: $\lnot b,e$ & 3 & 3 & 3 & $e$ & \cmark & 3 & \cmark & \cmark \\ \hline
Cl. 4: $\lnot b,\lnot e$ & 4 & 4 & 4 & $\lnot e$ & $\{\}$ \xmark & 4 & \cmark & \cmark \\ \hline
Cl. 5: $b,f$ & 5 & 5 & 5 & \cmark & \cmark & 5 & $f$ & \cmark \\ \hline
Cl. 6: $b,\lnot f$ & 6 & 6 & 6 & \cmark & \cmark & 6 & $\lnot f$ & $\{\}$ \xmark \\ \hline
\textcolor{gray}{Cl. 7: $\lnot b$} & - & - & - & - & learned $\lnot b$ & 7 & \cmark & \cmark \\ \hline \hline
BCP & - & - & - & $e$ & - & $\lnot b$ & $f$ & - \\ \hline
PL & $\lnot a$ & $c$ & - & - & - & - & - & - \\ \hline
Decision & - & - & $b$ & - & - & - & - & UNSAT \\ \hline
\end{tabular}}
Ad 5:
\begin{center}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node[base node] (1) {$b$};
\node[base node] (2) [above right of=1] {$e$};
\node[base node] (3) [below right of=1] {$\lnot e$};
\node[base node] (4) [above right of=3] {$\bot$};
\path[]
(1) edge [] node {$3$} (2)
edge [] node {$4$} (3)
(2) edge [] node {} (4)
(3) edge [] node {} (4);
\end{tikzpicture}
\end{center}
\begin{prooftree}
\AxiomC{$3. \; \lnot b \lor e$}
\AxiomC{$4. \; \lnot b \lor \lnot e$}
\BinaryInfC{$\lnot b$}
\end{prooftree}
Ad 8:
\begin{center}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node (0) {};
\node[base node] (1) [right of=0] {$\lnot b$};
\node[base node] (2) [above right of=1] {$f$};
\node[base node] (3) [below right of=1] {$\lnot f$};
\node[base node] (4) [above right of=3] {$\bot$};
\path[]
(0) edge [] node {$7$} (1)
(1) edge [] node {$5$} (2)
edge [] node {$6$} (3)
(2) edge [] node {} (4)
(3) edge [] node {} (4);
\end{tikzpicture}
\end{center}
\begin{prooftree}
\AxiomC{$5. \; b \lor f$}
\AxiomC{$6. \; b \lor \lnot f$}
\BinaryInfC{$b$}
\AxiomC{$7. \; \lnot b$}
\BinaryInfC{$\bot$}
\end{prooftree}

12
3_sat_solvers_dpll/0011.tex

@ -0,0 +1,12 @@
\item \lect Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor \lnot c)$
\item $(b \lor c)$
\item $(\lnot b \lor \lnot d)$
\item $(\lnot d \lor e)$
\item $(d \lor e)$
\item $(a \lor \lnot c \lor \lnot e)$
\item $(\lnot b \lor c \lor d)$
\end{enumerate}

92
3_sat_solvers_dpll/0011_graphs.tex

@ -0,0 +1,92 @@
First Conflict in Step 6: \\
\begin{conflictgraph}
\node[base node] (notA) {$\lnot a$};
\node[base node] (notB) [below of=notA] {$\lnot b$};
\node[base node] (C) [right of=notB] {$c$};
\node[base node] (notE) [above right of=C] {$\lnot e$};
\node[base node] (D) [above right of=notE] {$d$};
\node[base node] (notD) [below right of=notE] {$\lnot d$};
\node[base node] (bot) [below right of=D] {$\bot$};
\path[]
(notA) edge [] node {$6$} (notE)
(notB) edge [] node {$2$} (C)
(C) edge [] node {$6$} (notE)
(notE) edge [] node {$4$} (D)
(notE) edge [] node {$5$} (notD)
(notD) edge [] node {} (bot)
(D) edge [] node {} (bot);
\end{conflictgraph}
\begin{prooftree}
\AxiomC{$4. \; \lnot d \lor e$}
\AxiomC{$5. \; d \lor e$}
\BinaryInfC{$e$}
\AxiomC{$6. \; a \lor \lnot c \lor \lnot e$}
\BinaryInfC{$a \lor \lnot c$}
\AxiomC{$2. \; b \lor c$}
\BinaryInfC{$ a \lor b$}
\end{prooftree}
\vspace{1cm}
Second Conflict in Step 11: \\
\begin{conflictgraph}
\node[base node] (notA) {$\lnot a$};
\node[base node] (B) [right of=notA] {$b$};
\node[base node] (notD) [right of=B] {$\lnot d$};
\node[base node] (E) [right of=notD] {$e$};
\node[base node] (C) [below of=E] {$c$};
\node[base node] (notE) [right of=C] {$\lnot e$};
\node[base node] (bot) [above right of=notE] {$\bot$};
\path[]
(notA) edge [] node {$8$} (B)
(B) edge [] node {$3$} (notD)
(notD) edge [] node {$5$} (E)
(notD) edge [] node {$7$} (C)
(C) edge [] node {$6$} (notE)
(notE) edge [] node {} (bot)
(E) edge [] node {} (bot);
\end{conflictgraph}
\begin{prooftree}
\AxiomC{$6. \; a \lor \lnot c \lor \lnot e$}
\AxiomC{$7. \; \lnot b \lor c \lor d$}
\BinaryInfC{$a \lor \lnot b \lor d \lor \lnot e$}
\AxiomC{$5. \; d \lor e$}
\BinaryInfC{$a \lor \lnot b \lor d$}
\AxiomC{$3. \; \lnot b \lor \lnot d$}
\BinaryInfC{$ a \lor \lnot b$}
\AxiomC{$8. \; a \lor b$}
\BinaryInfC{$a$}
\end{prooftree}
\vspace{1cm}
Second Conflict in Step 16: \\
\begin{conflictgraph}
\node (0) {};
\node[base node] (A) [right of=0] {$a$};
\node[base node] (notC) [right of=A] {$\lnot c$};
\node[base node] (B) [right of=notC] {$b$};
\node[base node] (notD) [right of=B] {$\lnot d$};
\node[base node] (D) [below of=notD] {$d$};
\node[base node] (bot) [above right of=D] {$\bot$};
\path[]
(0) edge [] node {$9$} (A)
(A) edge [] node {$1$} (notC)
(notC) edge [] node {$2$} (B)
(B) edge [] node {$3$} (D)
(B) edge [] node {$7$} (notD)
(notD) edge [] node {} (bot)
(D) edge [] node {} (bot);
\end{conflictgraph}
\begin{prooftree}
\AxiomC{$7. \; \lnot b \lor c \lor d$}
\AxiomC{$3. \; \lnot b \lor \lnot d$}
\BinaryInfC{$\lnot b \lor c$}
\AxiomC{$2. \; b \lor c$}
\BinaryInfC{$c$}
\AxiomC{$1. \; \lnot a \lor \lnot c$}
\BinaryInfC{$\lnot a$}
\AxiomC{$9. \; a$}
\BinaryInfC{$\bot$}
\end{prooftree}

107
3_sat_solvers_dpll/0011_sol.tex

@ -0,0 +1,107 @@
\hspace{-0.09cm}\scalebox{0.87}{
\begin{dplltabular}{7}
\dpllStep{1|2|3|4|5|6|7}
\dpllDecL{0|1|2|2|2|2|1}
\dpllAssi{-|
$\lnot a$|
$\lnot a, \lnot b$|
$\lnot a, \lnot b, c$|
$\lnot a, \lnot b, c, \lnot e$|
$\lnot a, \lnot b, c, \lnot e, \lnot d$|
$\lnot a$}
\dpllClause{1}{$\lnot a,\lnot c$}
{$\lnot a,\lnot c$|\done|\done|\done|\done|\done|\done}
\dpllClause{2}{$b,c$}
{$b,c$|$b,c$|$c$|\done|\done|\done|$b,c$}
\dpllClause{3}{$\lnot b, \lnot d$}
{$\lnot b,\lnot d$|$\lnot b,\lnot d$|\done|\done|\done|\done|$\lnot b,\lnot d$}
\dpllClause{4}{$\lnot d, e$}
{$\lnot d,e$|$\lnot d,e$|$\lnot d,e$|$\lnot d,e$|$\lnot d$|\done|$\lnot d,e$}
\dpllClause{5}{$d, e$}
{$d.e$|$d.e$|$d.e$|$d.e$|$d$|\conflict|$d,e$}
\dpllClause{6}{$a, \lnot c, \lnot e$}
{$a, \lnot c, \lnot e$|$\lnot c,\lnot e$|$\lnot c, \lnot e$|$\lnot e$|\done|\done|$\lnot c, \lnot e$}
\dpllClause{7}{$\lnot b, c, d$}
{$\lnot b,c,d$|$\lnot b,c,d$|\done|\done|\done|\done|$\lnot b,c,d$}
\dpllClause{8}{\textcolor{gray}{$a.b$}}
{-|-|-|-|-|$a,b$|$b$}
\dpllClause{9}{\textcolor{gray}{$a$}}
{-|-|-|-|-|-|-}
\dpllBCP{-|-|$c$|$\lnot e$|\lnot d|-|$b$}
\dpllPL{-|-|-|-|-|-|-}
\dpllDeci{$\lnot a$|$\lnot b$|-|-|-|-|-}
\end{dplltabular}
}
\scalebox{0.87}{
\begin{dplltabular}{8}
\dpllStep{8|9|10|11|12|13|14}
\dpllDecL{1|1|1|1|0|0|0}
\dpllAssi{ $\lnot a, b$|
$\lnot a, b, \lnot d$|
$\lnot a, b, \lnot d, c$|
$\lnot a, b, \lnot d, c, \lnot e$|
-|
$a$|
$a, \lnot c$}
\dpllClause{1}{$\lnot a,\lnot c$}
{\done|\done|\done|\done|$\lnot a,\lnot c$|$\lnot c$|\done}
\dpllClause{2}{$b,c$}
{\done|\done|\done|\done|$b,c$|$b,c$|$b$}
\dpllClause{3}{$\lnot b, \lnot d$}
{$\lnot d$|\done|\done|\done|$\lnot b,\lnot d$|$\lnot b,\lnot d$|$\lnot b,\lnot d$}
\dpllClause{4}{$\lnot d, e$}
{$\lnot d,e$|\done|\done|\done|$\lnot d,e$|$\lnot d,e$|$\lnot d,e$}
\dpllClause{5}{$d, e$}
{$d,e$|$e$|$e$|\conflict|$d,e$|$d,e$|$d,e$}
\dpllClause{6}{$a, \lnot c, \lnot e$}
{$\lnot c,\lnot e$|$\lnot c,\lnot e$|$\lnot e$|\done|$a, \lnot c, \lnot e$|\done|\done}
\dpllClause{7}{$\lnot b, c, d$}
{$d,c$|$c$|\done|\done|$\lnot b, c, d$|$\lnot b, c, d$|$\lnot b, d$}
\dpllClause{8}{\textcolor{gray}{$a.b$}}
{\done|\done|\done|\done|$a,b$|\done|\done}
\dpllClause{9}{\textcolor{gray}{$a$}}
{-|-|-|$a$|$a$|\done|\done}
\dpllBCP{$\lnot d$|$c$|$\lnot e$|-|$a$|$\lnot c$|$b$}
\dpllPL{-|-|-|-|-|-|-}
\dpllDeci{-|-|-|-|-|-|-}
\end{dplltabular}
}
\scalebox{0.87}{
\begin{dplltabular}{2}
\dpllStep{15|16}
\dpllDecL{0|0}
\dpllAssi{$a, \lnot c, b$|
$a, \lnot c, b, \lnot d$}
\dpllClause{1}{$\lnot a,\lnot c$}
{\done|\done}
\dpllClause{2}{$b,c$}
{\done|\done}
\dpllClause{3}{$\lnot b, \lnot d$}
{$\lnot d$|\done}
\dpllClause{4}{$\lnot d, e$}
{$\lnot d,e$|\done}
\dpllClause{5}{$d, e$}
{$d,e$|$e$}
\dpllClause{6}{$a, \lnot c, \lnot e$}
{\done|\done}
\dpllClause{7}{$\lnot b, c, d$}
{$d$|\conflict}
\dpllClause{8}{\textcolor{gray}{$a.b$}}
{\done|\done}
\dpllClause{9}{\textcolor{gray}{$a$}}
{\done|\done}
\dpllBCP{$\lnot d$|-}
\dpllPL{-|-}
\dpllDeci{-|UNSAT}
\end{dplltabular}
}
\vspace{0.5cm}
\pagebreak

1
3_sat_solvers_dpll/1001.tex

@ -0,0 +1 @@
\item \self Explain the basic \textit{DPLL algorithm} for checking satisfiability of propositional formulas in \textit{Conjunctive Normal Form (CNF)}. Give a pseudo-code implementation to illustrate your explanations. For simplicity, you can skip all advanced concepts such as Boolean Constraint Propagation, Pure Literals, and Clause Learning.

1
3_sat_solvers_dpll/1002.tex

@ -0,0 +1 @@
\item \self \textit{SAT solvers} make choices based on \textit{heuristics} on which variable and value to pick for the next decision. (a) Why is the variable order for decisions important for the performance of SAT solvers? (b) Explain a commonly used decision heuristics.

5
3_sat_solvers_dpll/1003.tex

@ -0,0 +1,5 @@
\item \self Given a formula $\phi$ in CNF representation.
(a) What is a \emph{partial assignment} of variables? (b)
What is a \emph{total assignment} of variables?
(c) What does it mean that a clause in \emph{conflicting} with an assignment?
(d) What does it mean that a clause in \emph{satisfied} by an assignment?

10
3_sat_solvers_dpll/1004.tex

@ -0,0 +1,10 @@
\item \self
Given an formula $\phi$ in CNF representation and an assignment $A$.
Tick the following statements if they are true.
\begin{enumerate}
\item[$\square$] A clause is \emph{satisfied} by $A$, if $A$ makes a clause true.
\item[$\square$] If a clause is \textit{conflicting} with an assignment $A$, if the assignment makes the clause false.
\item[$\square$] If a clause is \textit{conflicting} with an assignment $A$, all variables in the clause are given the opposite value in A.
\item[$\square$] A expression $\phi[A]$ means that all variables within $\phi$ are assigned according to its truth values in $A$.
\end{enumerate}

2
3_sat_solvers_dpll/1005.tex

@ -0,0 +1,2 @@
\item \self
Within the context of DPLL, explain the terms \textit{decision} and \textit{decision level}.

9
3_sat_solvers_dpll/1006.tex

@ -0,0 +1,9 @@
\item \self Given the set of clauses $C_{\phi} = \{ \{a,\lnot b\}, \{\lnot a, c\}, \{b, \lnot c\}, \{\lnot a, \lnot c\} \}$ and the assignment $A = \{\lnot a\}$.
Tick the correct statements.
\begin{enumerate}
\item[$\square$] $\phi [A] = \{ \{a,\lnot b\}, \{\lnot a, c\}, \{\lnot a, \lnot c\} \}$
\item[$\square$] $\phi [A] = \{ \{c\}, \{b, \lnot c\}, \{\lnot c\} \}$
\item[$\square$] $\phi [A] = \{ \{\lnot b\}, \{b, \lnot c\}\}$
\item[$\square$] $\phi [A] = \{ \{\lnot b\}, \{c\}, \{b, \lnot c\}, \{\lnot c\} \}$
\end{enumerate}

2
3_sat_solvers_dpll/1007.tex

@ -0,0 +1,2 @@
\item \self
In the context of the DPLL algorithm, what does a conflict that arises at decision level 0 imply about the satisfiability or unsatisfiability of a formula? Explain your answer.

9
3_sat_solvers_dpll/1008.tex

@ -0,0 +1,9 @@
\item \self Use the DPLL algorithm (\emph{without} BCP, PL and clause learning) to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor b \lor \lnot c)$
\item $(a \lor \lnot b \lor c)$
\item $(\lnot a \lor \lnot b \lor c)$
\item $(a \lor b \lor \lnot c)$
\end{enumerate}

15
3_sat_solvers_dpll/1009.tex

@ -0,0 +1,15 @@
\item \self Consider the formula $\phi$ that consists of the conjunction of the following clauses:
\begin{enumerate}[{Clause} 1:]
\item $(\lnot a \lor b)$
\item $(\lnot a \lor \lnot d)$
\item $(c \lor \lnot b)$
\item $(\lnot c \lor d)$
\end{enumerate}
Use the DPLL algorithm (\emph{without} BCP, PL and clause learning) to determine whether or not the set of clauses given is satisfiable. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}
\item \label{positive} Decide variables in alphabetical order starting with the \textit{positive} phase.
\item \label{negative} Decide variables in alphabetical order starting with the \textit{negative} phase.
\item What differences can you see between \ref{positive} and \ref{negative}? Explain in your own words, why for the DPLL algorithm making good decisions is very important.
\end{enumerate}

2
3_sat_solvers_dpll/1010.tex

@ -0,0 +1,2 @@
\item \self In the context of the DPLL algorithm, explain what
\emph{Boolean Constraint Propagation} is. Give an example.

11
3_sat_solvers_dpll/1011.tex

@ -0,0 +1,11 @@
\item \self Use the DPLL algorithm with \textit{Boolean Constrain Propagation} (\emph{without} PL and clause learning) to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot d \lor \lnot b \lor \lnot a)$
\item $(\lnot e \lor a \lor \lnot f)$
\item $(\lnot a \lor c \lor b)$
\item $(f \lor a \lor e)$
\item $(d \lor \lnot a \lor \lnot b)$
\item $(\lnot a \lor \lnot c \lor b)$
\end{enumerate}

2
3_sat_solvers_dpll/1012.tex

@ -0,0 +1,2 @@
\item \self
Why does the DPLL algorithm check for \textit{Boolean Constraint Propagations (BCP)} and \textit{Pure Literals (PL)} before making a decision?

3
3_sat_solvers_dpll/1013.tex

@ -0,0 +1,3 @@
\item \self
Why is the decision level in the DPLL algorithm only incremented after a decision was made
but not when the \textit{Pure Literal Rule} or the \textit{Boolean Constrain Propagation Rule} was applied?

11
3_sat_solvers_dpll/1014.tex

@ -0,0 +1,11 @@
\item \self Use the DPLL algorithm with \textit{Boolean Constrain Propagation} and \textit{Pure Literals} (\emph{without} clause learning) to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{positive} phase. If the set of clauses resulted in \texttt{SAT}, give a satisfying model.
\begin{enumerate}[{Clause} 1:]
\item $(\lnot c \lor d)$
\item $(a \lor \lnot d \lor \lnot e )$
\item $(b \lor \lnot c)$
\item $(c \lor e)$
\item $(\lnot b \lor \lnot c)$
\item $(a \lor b)$
\end{enumerate}

3
3_sat_solvers_dpll/1015.tex

@ -0,0 +1,3 @@
\item \self
Explain conflict driven clause learning (CDCL).
How do learned clauses prevent the DPLL algorithm of running into already observed conflicts multiple times?

1
3_sat_solvers_dpll/1016.tex

@ -0,0 +1 @@
\item \self In the context of DPLL, give the definition of the \textit{resolution rule} used to construct a resolution proof. Show how the resolution rule derives from the basic natural deduction rules by providing a natural deduction proof.

33
3_sat_solvers_dpll/1017.tex

@ -0,0 +1,33 @@
\item \self Consider the following conflict graph with the following set of clauses:
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=1.5cm,
thick,base node/.style={circle,draw,minimum size=20pt}, real node/.style={double,circle,draw,minimum size=20pt}]
\node[base node] (1) {$\lnot a$};
\node[base node] (2) [right of=1]{$\lnot b$};
\node[base node] (4) [right of=2] {$\lnot c$};
\node[base node] (5) [right of=4] {$\lnot e$};
\node[base node] (6) [above right of=5] {$d$};
\node[base node] (3) [below right of=5] {$\lnot d$};
\node[base node] (7) [below right of=6] {$\bot$};
\path[]
(1) edge [] node {$3$} (2)
edge [bend right] node {$4$} (3)
(2) edge [] node {$5$} (4)
edge [bend left=35] node {$1$} (6)
(4) edge [] node {$2$} (5)
edge [bend left=20] node {$1$} (6)
(5) edge [] node {$4$} (3)
(3) edge [] node {} (7)
(6) edge [] node {} (7);
\end{tikzpicture}
\begin{enumerate}[{Clause} 1:]
\item $\{b, c, d\}$
\item $\{c, \lnot e\}$
\item $\{a, \lnot b\}$
\item $\{a, \lnot d, e\}$
\item $\{b, \lnot c\}$
\end{enumerate}
State the learned clause by making a resolution proof according to the given conflict graph and given clauses.

16
3_sat_solvers_dpll/1018.tex

@ -0,0 +1,16 @@
\item \self Consider the formula $\phi$ that consists of the conjunction
of the following clauses:
\begin{enumerate}[{Clause} 1:]
\item $(a \lor b)$
\item $(\lnot b \lor c)$
\item $(\lnot a \lor \lnot c)$
\item $(b \lor c)$
\item $(a \lor \lnot b)$
\end{enumerate}
\begin{enumerate}
\item \label{dpll} Use DPLL with learning to show that $\phi$ is unsatisfiable. Decide variables in \textit{alphabetic order} and starting with the \textit{positive} phase.
\item State and briefly explain the \textit{resolution rule}.
\item Using your results from \ref{dpll}, give a resolution proof of the unsatisfiability of $\phi$.
\end{enumerate}

11
3_sat_solvers_dpll/1019.tex

@ -0,0 +1,11 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{a, b, \lnot c\}$
\item $\{\lnot b, c, d\}$
\item $\{c, d, \lnot e\}$
\item $\{\lnot a, d, \lnot e\}$
\item $\{a, b, \lnot d\}$
\item $\{c, \lnot d, e\}$
\end{enumerate}

12
3_sat_solvers_dpll/1020.tex

@ -0,0 +1,12 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{\lnot a, \lnot b\}$
\item $\{a, c, e\}$
\item $\{b, \lnot d\}$
\item $\{\lnot c, d, e\}$
\item $\{\lnot d, e\}$
\item $\{\lnot a, b\}$
\item $\{a, d, \lnot e\}$
\end{enumerate}

13
3_sat_solvers_dpll/1021.tex

@ -0,0 +1,13 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{a, \lnot c\}$
\item $\{b, c, e\}$
\item $\{b, \lnot e\}$
\item $\{\lnot a, c\}$
\item $\{d, e\}$
\item $\{b, \lnot d\}$
\item $\{\lnot d, \lnot e\}$
\item $\{a, c\}$
\end{enumerate}

12
3_sat_solvers_dpll/1022.tex

@ -0,0 +1,12 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{a,b\}$
\item $\{\lnot a,c\}$
\item $\{a,\lnot d\}$
\item $\{\lnot b, c\}$
\item $\{\lnot c, d\}$
\item $\{\lnot c, e\}$
\item $\{d,\lnot e\}$
\end{enumerate}

12
3_sat_solvers_dpll/1023.tex

@ -0,0 +1,12 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{\lnot a, \lnot b\}$
\item $\{a, d, e\}$
\item $\{b, \lnot c\}$
\item $\{c, \lnot d, e\}$
\item $\{\lnot c, e\}$
\item $\{\lnot a, b\}$
\item $\{a, c, \lnot e\}$
\end{enumerate}

11
3_sat_solvers_dpll/1024.tex

@ -0,0 +1,11 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{\lnot b, c, d\}$
\item $\{\lnot b, \lnot d\}$
\item $\{a, \lnot c\}$
\item $\{\lnot c, e\}$
\item $\{b, c\}$
\item $\{\lnot a, \lnot e\}$
\end{enumerate}

13
3_sat_solvers_dpll/1025.tex

@ -0,0 +1,13 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{b, d\}$
\item $\{b, c\}$
\item $\{\lnot b, \lnot e\}$
\item $\{\lnot a, \lnot c\}$
\item $\{\lnot c, \lnot d\}$
\item $\{\lnot b, c\}$
\item $\{a, b\}$
\item $\{\lnot b, d, e\}$
\end{enumerate}

12
3_sat_solvers_dpll/1026.tex

@ -0,0 +1,12 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $\{\lnot b, d, e\}$
\item $\{b, e\}$
\item $\{c, d\}$
\item $\{\lnot a, \lnot e\}$
\item $\{a, \lnot c, \lnot e\}$
\item $\{c, \lnot d\}$
\item $\{\lnot b, \lnot d\}$
\end{enumerate}

12
3_sat_solvers_dpll/1027.tex

@ -0,0 +1,12 @@
\item \self Use the DPLL algorithm with conflict-driven clause learning to determine whether or not the set of clauses given is satisfiable. Decide variables in alphabetical order starting with the \textit{negative} phase. For conflicts, draw conflict graphs after the end of the table, and add the learned clause to the table.\\
If the set of clauses resulted in \texttt{SAT}, give a satisfying model. If the set of clauses resulted in \texttt{UNSAT}, give a resolution proof that shows that the conjunction of the clauses from the table is unsatisfiable.
\begin{enumerate}[{Clause} 1:]
\item $(a \lor b \lor c)$
\item $(\lnot a \lor b)$
\item $(\lnot b \lor c)$
\item $(\lnot c \lor d)$
\item $(\lnot c \lor e)$
\item $(\lnot d \lor \lnot e)$
\end{enumerate}

10
3_sat_solvers_dpll/1028.tex

@ -0,0 +1,10 @@
\item \self It is Sunday and your fridge is almost empty. You think that you can probably prepare a decent pizza with the little ingredients you have.
You do have dough. The dough is absolutely necessary for your pizza. You also have arugula, bell pepper and eggplant. You want to put at least one of those three ingredients as toppings on your pizza. Cheese is necessary for the pizza too. You have cheddar and feta. You can use one or both kinds of cheese. You don't like the combination of feta and bell pepper, so you can put at most one of those two ingredients on your pizza. Furthermore you need to save some veggies for dinner, so you can only use either the bell pepper or the eggplant for your pizza.
Create a CNF from this description. You can use the following rule to make the formula shorter:
\begin{align*}
(\lnot s \land t) \lor (s \land \lnot t) \ent \lnot s \lor \lnot t
\end{align*}
Then use a DPLL to figure out which ingredients you should use for your pizza and which ingredients you shouldn’t use. Formulate your answer as a sentence.

10
3_sat_solvers_dpll/1029.tex

@ -0,0 +1,10 @@
\item \self Your little cousin needs help to plan her birthday party. There are five kids she thinks about inviting, but not all of them get along. Here is what she tells you:
My very best friend is Anthony, I have to invite him! I’m also good friends with Daisy and Connie, I want at least one of them to come. But Daisy does not like Benjamin, I can’t invite them both! But I do like Benjamin, and I also like Emily. I’d want one of them to be there, or both of them. But Emily is always fighting with Daisy, so only one of them can come.
Create a CNF from this description. You can use the following rule to make the formula shorter:
\begin{align*}
(\lnot s \land t) \lor (s \land \lnot t) \ent \lnot s \lor \lnot t
\end{align*}
Then use the DPLL algorithm to figure out which kids your cousin should invite to her birthday party, which kids she should not invite and which kids she can invite without upsetting any other invited guests. Formulate your answer as a sentence.

2
3_sat_solvers_dpll/1030.tex

@ -0,0 +1,2 @@
\item \lect What is the complexity of the SAT-Problem?
What does its complexity imply?

3
3_sat_solvers_dpll/1030_sol.tex

@ -0,0 +1,3 @@
The SAT-Problem is NP-complete.
Its complexity implies that it is very unlikely that there exists any polynomial algorithm.

1
3_sat_solvers_dpll/1031.tex

@ -0,0 +1 @@
\item \lect Define the \textit{Boolean Satisfiability Problem}?

1
3_sat_solvers_dpll/1031_sol.tex

@ -0,0 +1 @@
Given a propositional formula $\varphi$, the Boolean Satisfiability Problem asks whether there exists a model such that the formula evaluates to true.

2
3_sat_solvers_dpll/2002.tex

@ -0,0 +1,2 @@
\item \lect Explain the following terms and give examples: (a) literal,
(b) cube, and (c) clause.

9
3_sat_solvers_dpll/2002_sol.tex

@ -0,0 +1,9 @@
Let $\varphi$ be a propositional formula defined
over Boolean variables $x_1, . . . ,x_n$.
\begin{itemize}
\item A \emph{literal} is one of the variables $x_i$ or the negation of a variable, e.g., $x_1$.
\item A \emph{clause} is a disjunction of literals, e.g., $x_1 \vee x_2$.
\item A \emph{cube} is a conjunction of literals, e.g., $x_1 \wedge x_2$.
\end{itemize}

2
3_sat_solvers_dpll/2003.tex

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

31
3_sat_solvers_dpll/2003_sol.tex

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

1
3_sat_solvers_dpll/2004.tex

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

31
3_sat_solvers_dpll/2004_sol.tex

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

3
3_sat_solvers_dpll/3001.tex

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

4
3_sat_solvers_dpll/3002.tex

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

7
3_sat_solvers_dpll/3003.tex

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

7
3_sat_solvers_dpll/3004.tex

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

8
3_sat_solvers_dpll/3005.tex

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

8
3_sat_solvers_dpll/3006.tex

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

15
3_sat_solvers_dpll/3007.tex

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

15
3_sat_solvers_dpll/3008.tex

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

11
3_sat_solvers_dpll/3009.tex

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

11
3_sat_solvers_dpll/3011.tex

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

11
3_sat_solvers_dpll/3012.tex

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

11
3_sat_solvers_dpll/3013.tex

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

17
3_sat_solvers_dpll/3014.tex

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

17
3_sat_solvers_dpll/3015.tex

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

16
3_sat_solvers_dpll/3016.tex

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

16
3_sat_solvers_dpll/3017.tex

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

1
3_sat_solvers_dpll/3018.tex

@ -0,0 +1 @@
%\item \self Given the formula $\phi = (p \lor \lnot q \lor \lnot r) \land (\lnot p \lor q \lor \lnot r) \land (p \lor q \lor r)$, which type of normal form, does this formula represent? Name all parts of the formula with the correct terminology.

6
3_sat_solvers_dpll/3019.tex

@ -0,0 +1,6 @@
\item \self Given a formula in propositional logic. Explain how to extract a \textit{CNF} representation as well as a \textit{DNF} representation of $\phi$ using the truth table from $\phi$.

1
3_sat_solvers_dpll/3021.tex

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

1
3_sat_solvers_dpll/3022.tex

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

26
3_sat_solvers_dpll/3023.tex

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

1
3_sat_solvers_dpll/3024.tex

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