From 92c473bd78203124ba13e1ef592cf60a25a13950 Mon Sep 17 00:00:00 2001
From: NotXia <35894453+NotXia@users.noreply.github.com>
Date: Sat, 7 Sep 2024 15:40:53 +0200
Subject: [PATCH] Fix typos <noupdate>

---
 .../module1/sections/_constraint_programming.tex            | 6 +++---
 .../module1/sections/_sat.tex                               | 4 ++--
 .../module2/sections/_smt.tex                               | 3 +++
 3 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_constraint_programming.tex b/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_constraint_programming.tex
index 8699d00..3a513b7 100644
--- a/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_constraint_programming.tex
+++ b/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_constraint_programming.tex
@@ -124,7 +124,7 @@ Examine individual constraints and detect inconsistent partial assignments.
         \begin{example}[Generalized arc consistency]
             Given the variables $D(X_1) = \{ 1, 2, 3 \}$, $D(X_2) = \{ 1, 2 \}$, $D(X_3) = \{ 1, 2 \}$ and 
             the constraint $C: \texttt{alldifferent}([X_1, X_2, X_3])$,
-            $C$ is not GAC as $1 \in D(X_1)$ and $2 \in D(X_2)$ do not have a support.
+            $C$ is not GAC as $1 \in D(X_1)$ and $2 \in D(X_1)$ do not have a support.
             
             By applying a constraint propagation algorithm, we can reduce the domain to: 
             $D(X_1) = \{ \cancel{1}, \cancel{2}, 3 \}$ and $D(X_2) = D(X_3) = \{ 1, 2 \}$.
@@ -185,7 +185,7 @@ Examine individual constraints and detect inconsistent partial assignments.
 
 \begin{description}
     \item[Constraint propagation] \marginnote{Constraint propagation}
-        Algorithm that removes values from the domains of the variables to achieve a given level of consistency.
+        Algorithm that removes values from the domain of the variables to achieve a given level of consistency.
 
         Constraint propagation algorithms interact with each other and already propagated constraints might be woke up again by another constraint.
         Propagation will eventually reach a fixed point.
@@ -357,7 +357,7 @@ Define constraints in an extensive way.
 
 
 \begin{description}
-    \item[Backtraking tree search] \marginnote{Backtraking tree search}
+    \item[Backtracking tree search] \marginnote{Backtracking tree search}
         Tree where nodes are variables and branches are variable assignments.
 
     \item[Systematic search] \marginnote{Systematic search}
diff --git a/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex b/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex
index e01e751..2c9975c 100644
--- a/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex
+++ b/src/year1/combinatorial-decision-making-and-optimization/module1/sections/_sat.tex
@@ -153,7 +153,7 @@
         \item $p$ with $(\lnot p \vee \lnot r)$ derives $\lnot r$.
         \item $\lnot s$ with $(q \vee s)$ derives $q$.
         \item $\lnot r$ with $(r \vee t)$ derives $t$.
-        \item $q$ with $(\lnot q \vee \lnot t)$ derives $\not t$.
+        \item $q$ with $(\lnot q \vee \lnot t)$ derives $\lnot t$.
         \item $t$ and $\lnot t$ bring to $\bot$. This branch is UNSAT.
     \end{itemize}
 
@@ -221,7 +221,7 @@ DPLL with two improvements:
         When a contradiction is found, augment the original CNF with a conflict clause
         to prune the search space.
 
-        The conflict clause is obtained through resolution by combining two clauses that cause the contradiction.
+        The conflict clause is obtained through resolution by combining the two clauses that cause the contradiction.
 
     \item[\texttt{Backjumping}]
         Depending on the type of contradiction, skip decision literals that are not causing the conflict
diff --git a/src/year1/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex b/src/year1/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex
index 2d44faf..94df841 100644
--- a/src/year1/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex
+++ b/src/year1/combinatorial-decision-making-and-optimization/module2/sections/_smt.tex
@@ -180,6 +180,8 @@
         
         \begin{remark}
             Useful to deal with black-box functions (i.e. prove satisfiability without a specific theory).
+            
+            \indenttbox
             \begin{example}
                 The following formula can be proved to be unsatisfiable by only using syntactic manipulations of basic FOL concepts:
                 \begin{gather*}
@@ -478,6 +480,7 @@ The $\calT$-solver does the following:
         \end{enumerate}
         As we are at decision level 0 (as no decision literal has been fixed), we can conclude that $\varphi$ is unsatisfiable.
 
+        \indenttbox
         \begin{remark}
             Unit and theory propagation are alternated (see algorithm description).
         \end{remark}