diff --git a/report/report.tex b/report/report.tex
index 0c90747..7e8f329 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -426,7 +426,108 @@ article takes advantage of the representation of those matrices as bitsets to
 make extensive use of bitwise operations.
 
 The to-be-built permutation matrix is a $\card{needle} \times \card{haystack}$
-matrix, 
+matrix. Each $1$ in a cell $(i, j)$ indicates that the $i$-th needle part is a
+possible match with the $j$-th haystack part. This matrix is called $perm$
+thereafter.
+
+The algorithm, left apart the \textsc{refine} function (detailed just after),
+is described in Figure~\ref{alg:ullmann}.
+
+\begin{figure}[h]
+\begin{algorithmic}
+    \Function{find\_at\_depth}{depth, perm, freeVert}
+        \If{no 1s on \lstc{perm[depth]}}
+            \State{} \Return{}
+        \EndIf{}
+
+        \State{} Save perm
+
+        \For{$0 \leq$ chosen $< \card{\text{haystack}}$ such that
+                \lstc{perm[depth][chosen]} $ = 1$ and \lstc{freeVert[chosen]}}
+            \State{} Put $0$s everywhere on \lstc{perm[depth]}, but on
+                \lstc{chosen}
+
+            \State{} Refine perm
+            \If{a row of perm has only $0$s}
+                \State{} \Return{}
+            \EndIf{}
+
+            \If{depth $=$ $\card{\text{needle}} - 1$}
+                \State{} Store perm as a result
+            \Else{}
+                \State{} \Call{find\_at\_depth}{depth$+1$, perm, freeVert with
+                    freeVert[chosen] $= 0$}
+            \EndIf{}
+
+            \State{} Restore perm
+        \EndFor{}
+    \EndFunction{}
+
+    \vspace{1em}
+
+    \Function{find}{perm}
+        \State{} \Return{} \Call{find\_at\_depth}{0, perm, [$1, \ldots, 1$]}
+    \EndFunction{}
+\end{algorithmic}
+    \caption{Ullmann's algorithm (without refining)}\label{alg:ullmann}
+\end{figure}
+
+The refining process is the actual keystone of the algorithm. It is the
+mechanism allowing the algorithm to cut down many exploration branches, by
+removing ones from the matrix.
+
+The idea is that a match between a needle's vertex $i$ and a haystack's vertex
+$j$ is only possible if, for each neighbour $k$ of $i$, $j$ has a neighbour
+$k'$ such that the permutation matrix has a one in position $(k, k')$. In other
+words, a match between $i$ and $j$ is only possible if every neighbour $k$ of
+$i$ (in needle) has a possibly matching (\wrt{} $perm$) vertex $k'$ (in
+haystack) which is a neighbour of $j$.
+
+This condition is checked on every $1$ in the permutation matrix. If it is not
+met, the cell is nulled. This, though, potentially creates new ones not
+matching the condition: the process must be run again, until no new zeroes
+appear.
+
+In the initial article~\cite{ullmann1976algorithm}, Ullmann advocates for
+bitwise tricks to complete this expensive step: indeed, checking the existence
+of such a $k'$ can be done by checking the nullity of the bitwise \textsc{and}
+of the adjacency of $j$ and the permutation matrix row of $k$.
+
+The refining function is detailed in Figure~\ref{alg:ullmann_refine}.
+
+\todo{Insert explaining figure}
+
+\begin{figure}[h]
+    \begin{algorithmic}
+        \Function{refine}{perm}
+            \While{changes during last run}
+                \For{each needle vertex $i$}
+                    \For{each haystack vertex $j$}
+                        \For{each neighbour $k$ of $i$ in needle}
+                            \If{\lstc{perm[k] & haystack\_adjacency[j]}
+                                    $= 0$}
+                                \State{} \lstc{perm[i][j]} $\gets 0$
+                            \EndIf{}
+                        \EndFor{}
+                    \EndFor{}
+                \EndFor{}
+            \EndWhile{}
+        \EndFunction{}
+    \end{algorithmic}
+    \caption{Ullmann's refining function}\label{alg:ullmann_refine}
+\end{figure}
+
+\subsection{Implementation optimisations}
+
+
+The matrix is first filled according to the signatures matches. It is then
+refined a bit more, by making sure that for every match, every potentially
+matching gate has the same ``wire kinds''. Indeed, a gate needle's wire must
+have at least the same inbound adjacent signatures as its matching haystack
+wire, and same goes for outbound adjacent signatures. Thus, two circuits cannot
+be matched if this condition is not respected for each pair of corresponding
+wires of those circuits, and their corresponding cell in the permutation matrix
+can be nulled.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Performance}