
diff -r e9f28d631c8b -r b9a8744c5efc damecco.tex
--- a/damecco.tex	Mon Nov 28 20:18:13 2016 +0100
+++ b/damecco.tex	Wed Nov 30 06:21:19 2016 +0100
@@ -123,19 +123,13 @@
 fostered the design of various algorithms for handling special graph
 structures.
 
-The idea of using state space representation and checking some
-conditions in each state to prune the search tree has made the VF2
-algorithm one of the state of the art graph matching algorithms for
-more than a decade. Recently, biological questions of ever increasing
-importance have required more efficient, specialized algorithms.
-
 This paper presents VF2++, a new algorithm based on the original VF2,
 which runs significantly faster on most test cases and performs
 especially well on special graph classes stemming from biological
 questions. VF2++ handles graphs of thousands of nodes in practically
 near linear time including preprocessing. Not only is it an improved
 version of VF2, but in fact, it is by far the fastest existing
-algorithm regarding biological graphs.
+algorithm especially on biological graphs.
 
 The reason for VF2++' superiority over VF2 is twofold. Firstly, taking
 into account the structure and the node labeling of the graph, VF2++
@@ -185,30 +179,26 @@
 solution of several new and revised questions.  The expressiveness,
 the simplicity and the studiedness of graphs make them practical for
 modelling and appear constantly in several seemingly independent
-fields.  Bioinformatics and chemistry are amongst the most relevant
-and most important fields.
+fields, such as bioinformatics and chemistry.
 
 Complex biological systems arise from the interaction and cooperation
 of plenty of molecular components. Getting acquainted with such
-systems at the molecular level has primary importance, since
+systems at the molecular level is of primary importance, since
 protein-protein interaction, DNA-protein interaction, metabolic
 interaction, transcription factor binding, neuronal networks, and
-hormone signaling networks can be understood only this way.
+hormone signaling networks can be understood this way.
 
-For instance, a molecular structure can be considered as a graph,
-whose nodes correspond to atoms and whose edges to chemical bonds. The
-secondary structure of a protein can also be represented as a graph,
-where nodes are associated with aminoacids and the edges with hydrogen
-bonds. The nodes are often whole molecular components and the edges
-represent some relationships among them.  The similarity and
-dissimilarity of objects corresponding to nodes are incorporated to
-the model by \emph{node labels}.  Many other chemical and biological
-structures can easily be modeled in a similar way. Understanding such
-networks basically requires finding specific subgraphs, which can not
-avoid the application of graph matching algorithms.
+Many chemical and biological structures can easily be modeled
+as graphs, for instance, a molecular structure can be
+considered as a graph, whose nodes correspond to atoms and whose
+edges to chemical bonds. The similarity and dissimilarity of
+objects corresponding to nodes are incorporated to the model
+by \emph{node labels}. Understanding such networks basically
+requires finding specific subgraphs, thus calls for efficient
+graph matching algorithms.
 
-Finally, let some of the other real-world fields related to some
-variants of graph matching be briefly mentioned: pattern recognition
+Other real-world fields related to some
+variants of graph matching include pattern recognition
 and machine vision \cite{HorstBunkeApplications}, symbol recognition
 \cite{CordellaVentoSymbolRecognition}, face identification
 \cite{JianzhuangYongFaceIdentification}.  \\
@@ -220,18 +210,17 @@
 for various graph classes, like trees and planar
 graphs\cite{PlanarGraphIso}, bounded valence
 graphs\cite{BondedDegGraphIso}, interval graphs\cite{IntervalGraphIso}
-or permutation graphs\cite{PermGraphIso}.
+or permutation graphs\cite{PermGraphIso}, and recently, an FPT algorithm has been presented for the coloured hypergraph isomorphism problem in \cite{ColoredHiperGraphIso}.
 
 In the following, some algorithms based on other approaches are
-summarized, which do not need any restrictions on the graphs. However,
+summarized, which do not need any restrictions on the graphs. Even though,
 an overall polynomial behaviour is not expectable from such an
-alternative, it may often have good performance, even on a graph class
-for which polynomial algorithm is known. Note that this summary
-containing only exact matching algorithms is far not complete, neither
-does it cover all the recent algorithms.
+alternative, it may often have good practical performance, in fact,
+it might be the best choice even on a graph class for which polynomial
+algorithm is known.
 
 The first practically usable approach was due to
-Ullmann\cite{Ullmann} which is a commonly used depth-first
+\emph{Ullmann}\cite{Ullmann} which is a commonly used depth-first
 search based algorithm with a complex heuristic for reducing the
 number of visited states. A major problem is its $\Theta(n^3)$ space
 complexity, which makes it impractical in the case of big sparse
@@ -241,7 +230,7 @@
 improved version of this algorithm based on a bit-vector solution for
 the binary Constraint Satisfaction Problem.
 
-The Nauty algorithm\cite{Nauty} transforms the two graphs to
+The \emph{Nauty} algorithm\cite{Nauty} transforms the two graphs to
 a canonical form before starting to check for the isomorphism. It has
 been considered as one of the fastest graph isomorphism algorithms,
 although graph categories were shown in which it takes exponentially
@@ -253,7 +242,7 @@
 has to be injective and edge-preserving, hence it is possible to
 handle new matching types as well.
 
-The \textbf{RI} algorithm\cite{RI} and its variations are based on a
+The \emph{RI} algorithm\cite{RI} and its variations are based on a
 state space representation. After reordering the nodes of the graphs,
 it uses some fast executable heuristic checks without using any
 complex pruning rules. It seems to run really efficiently on graphs
@@ -261,7 +250,7 @@
 Search in Biological Databases\cite{Content}.
 
 The currently most commonly used algorithm is the
-\textbf{VF2}\cite{VF2}, the improved version of VF\cite{VF}, which was
+\emph{VF2}\cite{VF2}, the improved version of \emph{VF}\cite{VF}, which was
 designed for solving pattern matching and computer vision problems,
 and has been one of the best overall algorithms for more than a
 decade. Although, it can't be up to new specialized algorithms, it is
@@ -269,83 +258,72 @@
 a state space representation and checks some conditions in each state
 to prune the search tree.
 
-Our first graph matching algorithm was the first version of VF2 which
-recognizes the significance of the node ordering, more opportunities
-to increase the cutting efficiency and reduce its computational
-complexity. This project was initiated and sponsored by QuantumBio
-Inc.\cite{QUANTUMBIO} and the implementation --- along with a source
-code --- has been published as a part of LEMON\cite{LEMON} open source
-graph library.
-
-This paper introduces \textbf{VF2++}, a new further improved algorithm
-for the graph and (induced)subgraph isomorphism problem, which uses
-efficient cutting rules and determines a node order in which VF2 runs
-significantly faster on practical inputs.
-
-Meanwhile, another variant called \textbf{VF2 Plus}\cite{VF2Plus} has
+Meanwhile, another variant called \emph{VF2 Plus}\cite{VF2Plus} has
 been published. It is considered to be as efficient as the RI
 algorithm and has a strictly better behavior on large graphs.  The
 main idea of VF2 Plus is to precompute a heuristic node order of the
 small graph, in which the VF2 works more efficiently.
 
+This paper introduces \emph{VF2++}, a new further improved algorithm
+for the graph and (induced)subgraph isomorphism problem, which uses
+efficient cutting rules and determines a node order in which VF2 runs
+significantly faster on practical inputs.
+
+This project was initiated and sponsored by QuantumBio
+Inc.\cite{QUANTUMBIO} and the implementation --- along with a source
+code --- has been published as a part of LEMON\cite{LEMON} open source
+graph library.
+
 \section{Problem Statement}
-This section provides a detailed description of the problems to be
+This section provides a formal description of the problems to be
 solved.
 \subsection{Definitions}
 
-Throughout the paper $G_{small}=(V_{small}, E_{small})$ and
-$G_{large}=(V_{large}, E_{large})$ denote two undirected graphs.
+Throughout the paper $G_{1}=(V_{1}, E_{1})$ and
+$G_{2}=(V_{2}, E_{2})$ denote two undirected graphs.
+
+\begin{definition}
+$\mathcal{L}: (V_{1}\cup V_{2}) \longrightarrow K$ is a \textbf{node
+    label function}, where K is an arbitrary set. The elements in K
+  are the \textbf{node labels}. Two nodes, u and v are said to be
+  \textbf{equivalent} if $\mathcal{L}(u)=\mathcal{L}(v)$.
+\end{definition}
+
+For the sake of simplicity, in this paper the graph, subgraph and induced subgraph isomorphisms are defined in a more general way.
+
 \begin{definition}\label{sec:ismorphic}
-$G_{small}$ and $G_{large}$ are \textbf{isomorphic} if $\exists M:
-  V_{small} \longrightarrow V_{large}$ bijection, for which the
+$G_{1}$ and $G_{2}$ are \textbf{isomorphic} (by the node label $\mathcal{L}$) if $\exists \mathfrak{m}:
+  V_{1} \longrightarrow V_{2}$ bijection, for which the
   following is true:
 \begin{center}
-$\forall u,v\in{V_{small}} : (u,v)\in{E_{small}} \Leftrightarrow
-  (M(u),M(v))\in{E_{large}}$
+$\forall u\in{V_{1}} : \mathcal{L}(u)=\mathcal{L}(\mathfrak{m}(u))$ and
+$\forall u,v\in{V_{1}} : (u,v)\in{E_{1}} \Leftrightarrow (\mathfrak{m}(u),\mathfrak{m}(v))\in{E_{2}}$
 \end{center}
 \end{definition}
-For the sake of simplicity in this paper subgraphs and induced
-subgraphs are defined in a more general way than usual:
+
 \begin{definition}
-$G_{small}$ is a \textbf{subgraph} of $G_{large}$ if $\exists I:
-  V_{small}\longrightarrow V_{large}$ injection, for which the
+$G_{1}$ is a \textbf{subgraph} of $G_{2}$ (by the node label $\mathcal{L}$) if $\exists \mathfrak{m}:
+  V_{1}\longrightarrow V_{2}$ injection, for which the
   following is true:
 \begin{center}
-$\forall u,v \in{V_{small}} : (u,v)\in{E_{small}} \Rightarrow (I(u),I(v))\in E_{large}$
+$\forall u\in{V_{1}} : \mathcal{L}(u)=\mathcal{L}(\mathfrak{m}(u))$ and
+$\mathbb{M}$
+$\forall u,v \in{V_{1}} : (u,v)\in{E_{1}} \Rightarrow (\mathfrak{m}(u),\mathfrak{m}(v))\in E_{2}$
 \end{center}
 \end{definition}
 
 \begin{definition} 
-$G_{small}$ is an \textbf{induced subgraph} of $G_{large}$ if $\exists
-  I: V_{small}\longrightarrow V_{large}$ injection, for which the
+$G_{1}$ is an \textbf{induced subgraph} of $G_{2}$ (by the node label $\mathcal{L}$) if $\exists
+  \mathfrak{m}: V_{1}\longrightarrow V_{2}$ injection, for which the
   following is true:
 \begin{center}
-$\forall u,v \in{V_{small}} : (u,v)\in{E_{small}} \Leftrightarrow
-  (I(u),I(v))\in E_{large}$
+$\forall u\in{V_{1}} : \mathcal{L}(u)=\mathcal{L}(\mathfrak{m}(u))$ and
+
+$\forall u,v \in{V_{1}} : (u,v)\in{E_{1}} \Leftrightarrow
+  (\mathfrak{m}(u),\mathfrak{m}(v))\in E_{2}$
 \end{center}
 \end{definition}
 
-\begin{definition}
-$lab: (V_{small}\cup V_{large}) \longrightarrow K$ is a \textbf{node
-    label function}, where K is an arbitrary set. The elements in K
-  are the \textbf{node labels}. Two nodes, u and v are said to be
-  \textbf{equivalent} if $lab(u)=lab(v)$.
-\end{definition}
-
-When node labels are given, the matched nodes must have the same
-labels.  For example, the node labeled isomorphism is phrased by
-\begin{definition}
-$G_{small}$ and $G_{large}$ are \textbf{isomorphic by the node label
-    function lab} if $\exists M: V_{small} \longrightarrow V_{large}$
-  bijection, for which the following is true:
-\begin{center}
-$(\forall u,v\in{V_{small}} : (u,v)\in{E_{small}} \Leftrightarrow
-  (M(u),M(v))\in{E_{large}})$ and $(\forall u\in{V_{small}} :
-  lab(u)=lab(M(u)))$
-\end{center}
-\end{definition}
-
-Note that he other two definitions can be extended in the same way.
 
 \subsection{Common problems}\label{sec:CommProb}
 
@@ -354,7 +332,7 @@
 problems also appear in many applications.
 
 The \textbf{subgraph matching problem} is the following: is
-$G_{small}$ isomorphic to any subgraph of $G_{large}$ by a given node
+$G_{1}$ isomorphic to any subgraph of $G_{2}$ by a given node
 label?
 
 The \textbf{induced subgraph matching problem} asks the same about the
@@ -382,77 +360,57 @@
 
 
 \subsection{Common notations}
-\indent Assume $G_{small}$ is searched in $G_{large}$.  The following
+\indent Assume $G_{1}$ is searched in $G_{2}$.  The following
 definitions and notations will be used throughout the whole paper.
 \begin{definition}
-A set $M\subseteq V_{small}\times V_{large}$ is called
-\textbf{mapping} if no node of $V_{small}\cup V_{large}$ appears
-in more than one pair in M.  That is, M uniquely associates some of
-the nodes in $V_{small}$ with some nodes of $V_{large}$ and vice
-versa.
+An injection $\mathfrak{m} : D \longrightarrow V_2$ is called (partial) \textbf{mapping}, where $D\subseteq V_1$.
+\end{definition}
+
+\begin{notation}
+$\mathfrak{D}(f)$ and $\mathfrak{R}(f)$ denote the domain and the range of a function $f$, respectively.
+\end{notation}
+
+\begin{definition}
+Mapping $\mathfrak{m}$ \textbf{covers} a node $u\in V_1\cup V_2$ if $u\in \mathfrak{D}(\mathfrak{m})\cup \mathfrak{R}(\mathfrak{m})$.
 \end{definition}
 
 \begin{definition}
-Mapping $M$ \textbf{covers} a node v if there exists a pair in M, which
-contains v.
+A mapping $\mathfrak{m}$ is $\mathbf{whole\ mapping}$ if $\mathfrak{m}$ covers all the
+nodes of $V_{1}$, i.e. $\mathfrak{D}(\mathfrak{m})=V_1$.
 \end{definition}
 
 \begin{definition}
-A mapping $M$ is $\mathbf{whole\ mapping}$ if $M$ covers all the
-nodes in $V_{small}$.
+Let \textbf{extend}$(\mathfrak{m},(u,v))$ denote the function $f : \mathfrak{D}(\mathfrak{m})\cup\{u\}\longrightarrow\mathfrak{R}(\mathfrak{m})\cup\{v\}$, for which $\forall w\in \mathfrak{D}(\mathfrak{m}) : \mathfrak{m}(w)=f(w)$ and $f(u)=v$ holds. Where $u\notin\mathfrak{D}(\mathfrak{m})$ and $v\notin\mathfrak{R}(\mathfrak{m})$, otherwise $extend(\mathfrak{m},(u,v))$ is undefined.
 \end{definition}
 
 \begin{notation}
-Let $\mathbf{M_{small}(s)} := \{u\in V_{small} : \exists v\in
-V_{large}: (u,v)\in M(s)\}$ and $\mathbf{M_{large}(s)} := \{v\in
-V_{large} : \exists u\in V_{small}: (u,v)\in M(s)\}$.
+Throughout the paper, $\mathbf{PT}$ denotes a generic problem type
+which can be substituted by any of the $\mathbf{ISO}$, $\mathbf{SUB}$
+and $\mathbf{IND}$ problems.
 \end{notation}
 
-\begin{notation}
-Let $\mathbf{Pair(M,v)}$ be the pair of $v$ in $M$ if such a node
-exist, otherwise $\mathbf{Pair(M,v)}$ is undefined, where $M$ is a mapping and $v\in V_{small}\cup V_{large}$.
-\end{notation}
-
-Note that if $\mathbf{Pair(M,v)}$ exists, then it is unique
-
-The definitions of the isomorphism types can be rephrased on the
-existence of a special whole mapping $M$, since it represents a
-bijection. For example
-\begin{center}
-$M\subseteq V_{small}\times V_{large}$ represents an induced subgraph
-  isomorphism $\Leftrightarrow$ $M$ is whole mapping and $\forall u,v
-  \in{V_{small}} : (u,v)\in{E_{small}} \Leftrightarrow
-  (Pair(M,u),Pair(M,v))\in E_{large}$.
-\end{center}
-
-Throughout the paper, $\mathbf{PT}$ denotes a generic problem type
-which can be substituted by any of $\mathbf{ISO}$, $\mathbf{SUB}$
-and $\mathbf{IND}$.
-
 \begin{definition}
-Let M be a mapping. A logical function $\mathbf{Cons_{PT}}$ is a
+Let $\mathfrak{m}$ be a mapping. A logical function $\mathbf{Cons_{PT}}$ is a
 \textbf{consistency function by } $\mathbf{PT}$ if the following
-holds. If there exists whole mapping $W$ of type $PT$ for which
-$M\subseteq W$, then $Cons_{PT}(M)$ is true.
+holds. If there exists a whole mapping $w$ satisfying the requirements of $PT$, for which $\mathfrak{m}$ is exactly $w$ restricted to $\mathfrak{D}(\mathfrak{m})$.
 \end{definition}
 
 \begin{definition} 
-Let M be a mapping. A logical function $\mathbf{Cut_{PT}}$ is a
+Let $\mathfrak{m}$ be a mapping. A logical function $\mathbf{Cut_{PT}}$ is a
 \textbf{cutting function by } $\mathbf{PT}$ if the following
-holds. $\mathbf{Cut_{PT}(M)}$ is false if $M$ can be extended to a
-whole mapping $W$ of type $PT$.
+holds. $\mathbf{Cut_{PT}(\mathfrak{m})}$ is false if there exists a sequence of extend operations, which results in a whole mapping satisfying the requirements of $PT$.
 \end{definition}
 
 \begin{definition}
-$M$ is said to be \textbf{consistent mapping by} $\mathbf{PT}$ if
-  $Cons_{PT}(M)$ is true.
+$\mathfrak{m}$ is said to be \textbf{consistent mapping by} $\mathbf{PT}$ if
+  $Cons_{PT}(\mathfrak{m})$ is true.
 \end{definition}
 
 $Cons_{PT}$ and $Cut_{PT}$ will often be used in the following form.
 \begin{notation}
-Let $\mathbf{Cons_{PT}(p, M)}:=Cons_{PT}(M\cup\{p\})$, and
-$\mathbf{Cut_{PT}(p, M)}:=Cut_{PT}(M\cup\{p\})$, where
-$p\in{V_{small}\!\times\!V_{large}}$ and $M\cup\{p\}$ is mapping.
+Let $\mathbf{Cons_{PT}(p, \mathfrak{m})}:=Cons_{PT}(extend(\mathfrak{m},p))$, and
+$\mathbf{Cut_{PT}(p, \mathfrak{m})}:=Cut_{PT}(extend(\mathfrak{m},p))$, where
+$p\in{V_{1}\backslash\mathfrak{D}(\mathfrak{m}) \!\times\!V_{2}\backslash\mathfrak{R}(\mathfrak{m})}$.
 \end{notation}
 
 $Cons_{PT}$ will be used to check the consistency of the already
@@ -462,11 +420,13 @@
 \subsection{Overview of the algorithm}
 VF2 uses a state space representation of mappings, $Cons_{PT}$ for
 excluding inconsistency with the problem type and $Cut_{PT}$ for
-pruning the search tree.  Each state $s$ of the matching process can
-be associated with a mapping $M(s)$.
+pruning the search tree.
 
 Algorithm~\ref{alg:VF2Pseu} is a high level description of
-the VF2 matching algorithm.
+the VF2 matching algorithm. Each state of the matching process can
+be associated with a mapping $\mathfrak{m}$. The initial state
+is associated with a mapping $\mathfrak{m}$, for which
+$\mathfrak{D}(\mathfrak{m})=\emptyset$, i.e. it starts with an empty mapping.
 
 
 \begin{algorithm}
@@ -476,132 +436,120 @@
 \caption{\hspace{0.5cm}$A\ high\ level\ description\ of\ VF2$}\label{alg:VF2Pseu}
 \begin{algorithmic}[1]
 
-\Procedure{VF2}{State $s$, ProblemType $PT$} \If{$M(s$) covers
-  $V_{small}$} \State Output($M(s)$) \Else
-  
-  \State Compute the set $P(s)$ of the pairs candidate for inclusion
-  in $M(s)$ \ForAll{$p\in{P(s)}$} \If{Cons$_{PT}$($p, M(s)$) $\wedge$
-    $\neg$Cut$_{PT}$($p, M(s)$)} \State Compute the nascent state
-  $\tilde{s}$ by adding $p$ to $M(s)$ \State \textbf{call}
-  VF2($\tilde{s}$, $PT$) \EndIf \EndFor \EndIf \EndProcedure
+\Procedure{VF2}{Mapping $\mathfrak{m}$, ProblemType $PT$}
+  \If{$\mathfrak{m}$ covers
+    $V_{1}$} \State Output($\mathfrak{m}$)
+  \Else
+  \State Compute the set $P_\mathfrak{m}$ of the pairs candidate for inclusion
+  in $\mathfrak{m}$ \ForAll{$p\in{P_\mathfrak{m}}$} \If{Cons$_{PT}$($p,\mathfrak{m}$) $\wedge$
+    $\neg$Cut$_{PT}$($p,\mathfrak{m}$)}
+    \State \textbf{call}
+  VF2($extend(\mathfrak{m},p)$, $PT$) \EndIf \EndFor \EndIf \EndProcedure
 \end{algorithmic}
 \end{algorithm}
 
 
-The initial state $s_0$ is associated with $M(s_0)=\emptyset$, i.e. it
-starts with an empty mapping.
+For the current mapping $\mathfrak{m}$, the algorithm computes $P_\mathfrak{m}$, the set of
+candidate node pairs for adding to the current mapping $\mathfrak{m}_s$.
 
-For each state $s$, the algorithm computes $P(s)$, the set of
-candidate node pairs for adding to the current state $s$.
-
-For each pair $p$ in $P(s)$, $Cons_{PT}(p,M(s))$ and
-$Cut_{PT}(p,M(s))$ are evaluated. If $Cons_{PT}(p,M(s))$ is true and
-$Cut_{PT}(p,M(s))$ is false, the successor state $\tilde{s}=s\cup
-\{p\}$ is computed, and the whole process is recursively applied to
-$\tilde{s}$. Otherwise, $\tilde{s}$ is not consistent by $PT$, or it
-can be proved that $s$ can not be extended to a whole mapping.
+For each pair $p$ in $P_\mathfrak{m}$, $Cons_{PT}(p,\mathfrak{m})$ and
+$Cut_{PT}(p,\mathfrak{m})$ are evaluated. If the former is true and
+the latter is false, the whole process is recursively applied to
+$extend(\mathfrak{m},p)$. Otherwise, $extend(\mathfrak{m},p)$ is not consistent by $PT$, or it
+can be proved that $\mathfrak{m}$ can not be extended to a whole mapping.
 
 In order to make sure of the correctness, see
 \begin{claim}
 Through consistent mappings, only consistent whole mappings can be
-reached, and all of the whole mappings are reachable through
+reached, and all the consistent whole mappings are reachable through
 consistent mappings.
 \end{claim}
 
-Note that a state may be reached in exponentially many different ways, since the
-order of insertions into $M$ does not influence the nascent mapping.
+Note that a mapping may be reached in exponentially many different ways, since the
+order of extensions does not influence the nascent mapping.
 
 However, one may observe
 
 \begin{claim}
 \label{claim:claimTotOrd}
-Let $\prec$ an arbitrary total ordering relation on $V_{small}$.  If
-the algorithm ignores each $p=(u,v) \in P(s)$, for which
+Let $\prec$ be an arbitrary total ordering relation on $V_{1}$.  If
+the algorithm ignores each $p=(u,v) \in P_\mathfrak{m}$, for which
 \begin{center}
-$\exists (\tilde{u},\tilde{v})\in P(s): \tilde{u} \prec u$,
+$\exists (\tilde{u},\tilde{v})\in P_\mathfrak{m}: \tilde{u} \prec u$,
 \end{center}
-then no state can be reached more than once, and each state associated
-with a whole mapping remains reachable.
+then no mapping can be reached more than once, and each whole mapping remains reachable.
 \end{claim}
 
 Note that the cornerstone of the improvements to VF2 is a proper
 choice of a total ordering.
 
-\subsection{The candidate set P(s)}
+\subsection{The candidate set}
 \label{candidateComputingVF2}
-Let $P(s)$ be the set of the candidate pairs for inclusion in $M(s)$.
+Let $P_\mathfrak{m}$ be the set of the candidate pairs for inclusion in $\mathfrak{m}$.
 
 \begin{notation}
-Let $\mathbf{T_{small}(s)}:=\{u \in V_{small} : u$ is not covered by
-$M(s)\wedge\exists \tilde{u}\in{V_{small}: (u,\tilde{u})\in E_{small}}
-\wedge \tilde{u}$ is covered by $M(s)\}$, and
-\\ $\mathbf{T_{large}(s)}\!:=\!\{v \in\!V_{large}\!:\!v$ is not
-covered by
-$M(s)\wedge\!\exists\tilde{v}\!\in\!{V_{large}\!:\!(v,\tilde{v})\in\!E_{large}}
-\wedge \tilde{v}$ is covered by $M(s)\}$
+Let $\mathbf{T_{1}(\mathfrak{m})}:=\{u \in V_{1}\backslash\mathfrak{D}(\mathfrak{m}) : \exists \tilde{u}\in{\mathfrak{D}(\mathfrak{m}): (u,\tilde{u})\in E_{1}}\}$, and
+ $\mathbf{T_{2}(\mathfrak{m})} := \{v \in V_{2}\backslash\mathfrak{R}(\mathfrak{m}) : \exists\tilde{v}\in{\mathfrak{R}(\mathfrak{m}):(v,\tilde{v})\in E_{2}}\}$.
 \end{notation}
 
-The set $P(s)$ includes the pairs of uncovered neighbours of covered
+The set $P_\mathfrak{m}$ includes the pairs of uncovered neighbours of covered
 nodes, and if there is not such a node pair, all the pairs containing
 two uncovered nodes are added. Formally, let
 \[
- P(s)\!=\!
+ P_\mathfrak{m}\!=\!
   \begin{cases} 
-   T_{small}(s)\times T_{large}(s)&\hspace{-0.15cm}\text{if }
-   T_{small}(s)\!\neq\!\emptyset\!\wedge\!T_{large}(s)\!\neq
-   \emptyset,\\ (V_{small}\!\setminus\!M_{small}(s))\!\times\!(V_{large}\!\setminus\!M_{large}(s))
-   &\hspace{-0.15cm}otherwise.
+   T_{1}(\mathfrak{m})\times T_{2}(\mathfrak{m})&\hspace{-0.15cm}\text{if }
+   T_{1}(\mathfrak{m})\!\neq\!\emptyset\ \text{and }T_{2}(\mathfrak{m})\!\neq
+   \emptyset,\\ (V_{1}\!\setminus\!\mathfrak{D}(\mathfrak{m}))\!\times\!(V_{2}\!\setminus\!\mathfrak{R}(\mathfrak{m}))
+   &\hspace{-0.15cm}\text{otherwise}.
   \end{cases}
 \]
 
 \subsection{Consistency}
-Suppose $p=(u,v)$, where $u\in V_{small}$ and $v\in V_{large}$, $s$ is
-a state of the matching procedure, $M(s)$ is consistent mapping by
-$PT$ and $lab(u)=lab(v)$.  $Cons_{PT}(p,M(s))$ checks whether
-including pair $p$ into $M(s)$ leads to a consistent mapping by $PT$.
+Suppose $p=(u,v)$, where $u\in V_{1}$ and $v\in V_{2}$, $\mathfrak{m}$ is a consistent mapping by
+$PT$. $Cons_{PT}(p,\mathfrak{m})$ checks whether
+including pair $p$ into $\mathfrak{m}$ leads to a consistent mapping by $PT$.
 
 For example, the consistency function of induced subgraph isomorphism is as follows.
 \begin{notation}
-Let $\mathbf{\Gamma_{small} (u)}:=\{\tilde{u}\in V_{small} :
-(u,\tilde{u})\in E_{small}\}$, and $\mathbf{\Gamma_{large}
-  (v)}:=\{\tilde{v}\in V_{large} : (v,\tilde{v})\in E_{large}\}$, where $u\in V_{small}$ and $v\in V_{large}$.
+Let $\mathbf{\Gamma_{1} (u)}:=\{\tilde{u}\in V_{1} :
+(u,\tilde{u})\in E_{1}\}$, and $\mathbf{\Gamma_{2}
+  (v)}:=\{\tilde{v}\in V_{2} : (v,\tilde{v})\in E_{2}\}$, where $u\in V_{1}$ and $v\in V_{2}$.
 \end{notation}
 
-$M(s)\cup \{(u,v)\}$ is a consistent mapping by $IND$ $\Leftrightarrow
-(\forall \tilde{u}\in M_{small}: (u,\tilde{u})\in E_{small}
-\Leftrightarrow (v,Pair(M(s),\tilde{u}))\in E_{large})$. The
+$extend(\mathfrak{m},(u,v))$ is a consistent mapping by $IND$ $\Leftrightarrow
+(\forall \tilde{u}\in \mathfrak{D}(\mathfrak{m}): (u,\tilde{u})\in E_{1}
+\Leftrightarrow (v,\mathfrak{m}(\tilde{u}))\in E_{2})$. The
 following formulation gives an efficient way of calculating
 $Cons_{IND}$.
 \begin{claim}
-$Cons_{IND}((u,v),M(s)):=(\forall \tilde{v}\in \Gamma_{large}(v)
-  \ \cap\ M_{large}(s):\\(Pair(M(s),\tilde{v}),u)\in E_{small})\wedge
-  (\forall \tilde{u}\in \Gamma_{small}(u)
-  \ \cap\ M_{small}(s):(v,Pair(M(s),\tilde{u}))\in E_{large})$ is a
+$Cons_{IND}((u,v),\mathfrak{m}):=\mathcal{L}(u)\!\!=\!\!\mathcal{L}(v)\wedge(\forall \tilde{v}\in \Gamma_{2}(v)\cap\mathfrak{R}(\mathfrak{m}):(u,\mathfrak{m}^{-1}(\tilde{v}))\in E_{1})\wedge
+  (\forall \tilde{u}\in \Gamma_{1}(u)
+  \cap \mathfrak{D}(\mathfrak{m}):(v,\mathfrak{m}(\tilde{u}))\in E_{2})$ is a
   consistency function in the case of $IND$.
 \end{claim}
 
 \subsection{Cutting rules}
-$Cut_{PT}(p,M(s))$ is defined by a collection of efficiently
-verifiable conditions. The requirement is that $Cut_{PT}(p,M(s))$ can
-be true only if it is impossible to extended $M(s)\cup \{p\}$ to a
+$Cut_{PT}(p,\mathfrak{m})$ is defined by a collection of efficiently
+verifiable conditions. The requirement is that $Cut_{PT}(p,\mathfrak{m})$ can
+be true only if it is impossible to extend $extend(\mathfrak{m},p)$ to a
 whole mapping.
 
 As an example, the cutting function of induced subgraph isomorphism is presented.
 \begin{notation}
-Let $\mathbf{\tilde{T}_{small}}(s):=(V_{small}\backslash
-M_{small}(s))\backslash T_{small}(s)$, and
-\\ $\mathbf{\tilde{T}_{large}}(s):=(V_{large}\backslash
-M_{large}(s))\backslash T_{large}(s)$.
+Let $\mathbf{\tilde{T}_{1}}(\mathfrak{m}):=(V_{1}\backslash
+\mathfrak{D}(\mathfrak{m}))\backslash T_{1}(\mathfrak{m})$, and
+\\ $\mathbf{\tilde{T}_{2}}(\mathfrak{m}):=(V_{2}\backslash
+\mathfrak{R}(\mathfrak{m}))\backslash T_{2}(\mathfrak{m})$.
 \end{notation}
 
 \begin{claim}
-$Cut_{IND}((u,v),M(s)):= |\Gamma_{large} (v)\ \cap\ T_{large}(s)| <
-  |\Gamma_{small} (u)\ \cap\ T_{small}(s)| \vee |\Gamma_{large}(v)\cap
-  \tilde{T}_{large}(s)| < |\Gamma_{small}(u)\cap
-  \tilde{T}_{small}(s)|$ is a cutting function by $IND$.
+$Cut_{IND}((u,v),\mathfrak{m}):= |\Gamma_{2} (v)\ \cap\ T_{2}(\mathfrak{m})| <
+  |\Gamma_{1} (u)\ \cap\ T_{1}(\mathfrak{m})| \vee |\Gamma_{2}(v)\cap
+  \tilde{T}_{2}(\mathfrak{m})| < |\Gamma_{1}(u)\cap
+  \tilde{T}_{1}(\mathfrak{m})|$ is a cutting function by $IND$.
 \end{claim}
 
-
 \section{The VF2++ Algorithm}
 Although any total ordering relation makes the search space of VF2 a
 tree, its choice turns out to dramatically influence the number of
@@ -625,25 +573,116 @@
 candidate set calculating were described in \cite{VF2Plus}, too.
 
 It should be noted that all the methods described in this section are
-extendable to handle directed graphs and edge labels as well.
+extendable to handle directed graphs and edge labels as well.\newline
 
 The basic ideas and the detailed description of VF2++ are provided in
 the following.
 
+The goal is to find a matching order in which the algorithm is able to
+recognize inconsistency or prune the infeasible branches on the
+highest levels and goes deep only if it is needed.
+
+\begin{notation}
+Let $\mathbf{Conn_{H}(u)}:=|\Gamma_{1}(u)\cap H\}|$, that is the
+number of neighbours of u which are in H, where $u\in V_{1} $ and
+$H\subseteq V_{1}$.
+\end{notation}
+
+The principal question is the following. Suppose a mapping $\mathfrak{m}$ is
+given. For which node of $T_{1}(\mathfrak{m})$ is the hardest to find a
+consistent pair in $G_{2}$? The more covered neighbours a node in
+$T_{1}(\mathfrak{m})$ has --- i.e. the largest $Conn_{\mathfrak{D}(\mathfrak{m})}$ it has
+---, the more rarely satisfiable consistency constraints for its pair
+are given.
+
+In biology, most of the graphs are sparse, thus several nodes in
+$T_{1}(\mathfrak{m})$ may have the same $Conn_{\mathfrak{D}(\mathfrak{m})}$, which makes
+reasonable to define a secondary and a tertiary order between them.
+The observation above proves itself to be as determining, that the
+secondary ordering prefers nodes with the most uncovered neighbours
+among which have the same $Conn_{\mathfrak{D}(\mathfrak{m})}$ to increase
+$Conn_{\mathfrak{D}(\mathfrak{m})}$ of uncovered nodes so much, as possible.  The
+tertiary ordering prefers nodes having the rarest uncovered labels.
+
+Note that the secondary ordering is the same as the ordering by $deg$,
+which is a static data in front of the above used.
+
+These rules can easily result in a matching order which contains the
+nodes of a long path successively, whose nodes may have low $Conn$ and
+is easily matchable into $G_{2}$. To avoid that, a BFS order is
+used, which provides the shortest possible paths.
+\newline
+
+In the following, some examples on which the VF2 may be slow are
+described, although they are easily solvable by using a proper
+matching order.
+
+\begin{example}
+Suppose $G_{1}$ can be mapped into $G_{2}$ in many ways
+without node labels. Let $u\in V_{1}$ and $v\in V_{2}$.
+\newline
+$\mathcal{L}(u):=black$
+\newline
+$\mathcal{L}(v):=black$
+\newline
+$\mathcal{L}(\tilde{u}):=red \ \forall \tilde{u}\in (V_{1}\backslash
+\{u\})$
+\newline
+$\mathcal{L}(\tilde{v}):=red \ \forall \tilde{v}\in (V_{2}\backslash
+\{v\})$
+\newline
+
+Now, any mapping by $\mathcal{L}$ must contain $(u,v)$, since
+$u$ is black and no node in $V_{2}$ has a black label except
+$v$. If unfortunately $u$ were the last node which will get covered,
+VF2 would check only in the last steps, whether $u$ can be matched to
+$v$.
+\newline
+However, had $u$ been the first matched node, u would have been
+matched immediately to v, so all the mappings would have been
+precluded in which node labels can not correspond.
+\end{example}
+
+\begin{example}
+Suppose there is no node label given, $G_{1}$ is a small graph and
+can not be mapped into $G_{2}$ and $u\in V_{1}$.
+\newline
+Let $G'_{1}:=(V_{1}\cup
+\{u'_{1},u'_{2},..,u'_{k}\},E_{1}\cup
+\{(u,u'_{1}),(u'_{1},u'_{2}),..,(u'_{k-1},u'_{k})\})$, that is,
+$G'_{1}$ is $G_{1}\cup \{ a\ k$ long path, which is disjoint
+from $G_{1}$ and one of its starting points is connected to $u\in
+V_{1}\}$.
+\newline
+Is there a subgraph of $G_{2}$, which is isomorph with
+$G'_{1}$?
+\newline
+If unfortunately the nodes of the path were the first $k$ nodes in the
+matching order, the algorithm would iterate through all the possible k
+long paths in $G_{2}$, and it would recognize that no path can be
+extended to $G'_{1}$.
+\newline
+However, had it started by the matching of $G_{1}$, it would not
+have matched any nodes of the path.
+\end{example}
+
+These examples may look artificial, but the same problems also appear
+in real-world instances, even though in a less obvious way.
+
 \subsection{Preparations}
 \begin{claim}
 \label{claim:claimCoverFromLeft}
 The total ordering relation uniquely determines a node order, in which
-the nodes of $V_{small}$ will be covered by VF2. From the point of
+the nodes of $V_{1}$ will be covered by VF2. From the point of
 view of the matching procedure, this means, that always the same node
-of $G_{small}$ will be covered on the d-th level.
+of $G_{1}$ will be covered on the d-th level.
 \end{claim}
 
 \begin{definition}
-An order $(u_{\sigma(1)},u_{\sigma(2)},..,u_{\sigma(|V_{small}|)})$ of
-$V_{small}$ is \textbf{matching order} if exists $\prec$ total
+An order $(u_{\sigma(1)},u_{\sigma(2)},..,u_{\sigma(|V_{1}|)})$ of
+$V_{1}$ is \textbf{matching order} if exists $\prec$ total
 ordering relation, s.t. the VF2 with $\prec$ on the d-th level finds
-pair for $u_{\sigma(d)}$ for all $d\in\{1,..,|V_{small}|\}$.
+pair for $u_{\sigma(d)}$ for all $d\in\{1,..,|V_{1}|\}$.
 \end{definition}
 
 \begin{claim}\label{claim:MOclaim}
@@ -656,105 +695,13 @@
 order, and every matching order can be determined by a total ordering,
 however, more than one different total orderings may determine the
 same matching order.
-\subsection{Idea behind the algorithm}
-The goal is to find a matching order in which the algorithm is able to
-recognize inconsistency or prune the infeasible branches on the
-highest levels and goes deep only if it is needed.
-
-\begin{notation}
-Let $\mathbf{Conn_{H}(u)}:=|\Gamma_{small}(u)\cap H\}|$, that is the
-number of neighbours of u which are in H, where $u\in V_{small} $ and
-$H\subseteq V_{small}$.
-\end{notation}
-
-The principal question is the following. Suppose a state $s$ is
-given. For which node of $T_{small}(s)$ is the hardest to find a
-consistent pair in $G_{large}$? The more covered neighbours a node in
-$T_{small}(s)$ has --- i.e. the largest $Conn_{M_{small}(s)}$ it has
----, the more rarely satisfiable consistency constraints for its pair
-are given.
-
-In biology, most of the graphs are sparse, thus several nodes in
-$T_{small}(s)$ may have the same $Conn_{M_{small}(s)}$, which makes
-reasonable to define a secondary and a tertiary order between them.
-The observation above proves itself to be as determining, that the
-secondary ordering prefers nodes with the most uncovered neighbours
-among which have the same $Conn_{M_{small}(s)}$ to increase
-$Conn_{M_{small}(s)}$ of uncovered nodes so much, as possible.  The
-tertiary ordering prefers nodes having the rarest uncovered labels.
-
-Note that the secondary ordering is the same as the ordering by $deg$,
-which is a static data in front of the above used.
-
-These rules can easily result in a matching order which contains the
-nodes of a long path successively, whose nodes may have low $Conn$ and
-is easily matchable into $G_{large}$. To avoid that, a BFS order is
-used, which provides the shortest possible paths.
-\newline
-
-In the following, some examples on which the VF2 may be slow are
-described, although they are easily solvable by using a proper
-matching order.
-
-\begin{example}
-Suppose $G_{small}$ can be mapped into $G_{large}$ in many ways
-without node labels. Let $u\in V_{small}$ and $v\in V_{large}$.
-\newline
-$lab(u):=black$
-\newline
-$lab(v):=black$
-\newline
-$lab(\tilde{u}):=red \ \forall \tilde{u}\in (V_{small}\backslash
-\{u\})$
-\newline
-$lab(\tilde{v}):=red \ \forall \tilde{v}\in (V_{large}\backslash
-\{v\})$
-\newline
-
-Now, any mapping by the node label $lab$ must contain $(u,v)$, since
-$u$ is black and no node in $V_{large}$ has a black label except
-$v$. If unfortunately $u$ were the last node which will get covered,
-VF2 would check only in the last steps, whether $u$ can be matched to
-$v$.
-\newline
-However, had $u$ been the first matched node, u would have been
-matched immediately to v, so all the mappings would have been
-precluded in which node labels can not correspond.
-\end{example}
-
-\begin{example}
-Suppose there is no node label given, $G_{small}$ is a small graph and
-can not be mapped into $G_{large}$ and $u\in V_{small}$.
-\newline
-Let $G'_{small}:=(V_{small}\cup
-\{u'_{1},u'_{2},..,u'_{k}\},E_{small}\cup
-\{(u,u'_{1}),(u'_{1},u'_{2}),..,(u'_{k-1},u'_{k})\})$, that is,
-$G'_{small}$ is $G_{small}\cup \{ a\ k$ long path, which is disjoint
-from $G_{small}$ and one of its starting points is connected to $u\in
-V_{small}\}$.
-\newline
-Is there a subgraph of $G_{large}$, which is isomorph with
-$G'_{small}$?
-\newline
-If unfortunately the nodes of the path were the first $k$ nodes in the
-matching order, the algorithm would iterate through all the possible k
-long paths in $G_{large}$, and it would recognize that no path can be
-extended to $G'_{small}$.
-\newline
-However, had it started by the matching of $G_{small}$, it would not
-have matched any nodes of the path.
-\end{example}
-
-These examples may look artificial, but the same problems also appear
-in real-world instances, even though in a less obvious way.
 
 \subsection{Total ordering}
-Instead of the total ordering relation, the matching order will be
-searched directly.
+The matching order will be searched directly.
 \begin{notation}
-Let \textbf{F$_\mathcal{M}$(l)}$:=|\{v\in V_{large} :
-l=lab(v)\}|-|\{u\in V_{small}\backslash \mathcal{M} : l=lab(u)\}|$ ,
-where $l$ is a label and $\mathcal{M}\subseteq V_{small}$.
+Let \textbf{F$_\mathcal{M}$(l)}$:=|\{v\in V_{2} :
+l=\mathcal{L}(v)\}|-|\{u\in V_{1}\backslash \mathcal{M} : l=\mathcal{L}(u)\}|$ ,
+where $l$ is a label and $\mathcal{M}\subseteq V_{1}$.
 \end{notation}
 
 \begin{definition}Let $\mathbf{arg\ max}_{f}(S) :=\{u\in S : f(u)=max_{v\in S}\{f(v)\}\}$ and $\mathbf{arg\ min}_{f}(S) := arg\ max_{-f}(S)$, where $S$ is a finite set and $f:S\longrightarrow \mathbb{R}$.
@@ -768,9 +715,9 @@
 \caption{\hspace{0.5cm}$The\ method\ of\ VF2++\ for\ determining\ the\ node\ order$}\label{alg:VF2PPPseu}
 \begin{algorithmic}[1]
 \Procedure{VF2++order}{} \State $\mathcal{M}$ := $\emptyset$
-\Comment{matching order} \While{$V_{small}\backslash \mathcal{M}
+\Comment{matching order} \While{$V_{1}\backslash \mathcal{M}
   \neq\emptyset$} \State $r\in$ arg max$_{deg}$ (arg
-min$_{F_\mathcal{M}\circ lab}(V_{small}\backslash
+min$_{F_\mathcal{M}\circ \mathcal{L}}(V_{1}\backslash
 \mathcal{M})$)\label{alg:findMin} \State Compute $T$, a BFS tree with
 root node $r$.  \For{$d=0,1,...,depth(T)$} \State $V_d$:=nodes of the
 $d$-th level \State Process $V_d$ \Comment{See Algorithm
@@ -786,7 +733,7 @@
 \caption{\hspace{.5cm}$The\ method\ for\ processing\ a\ level\ of\ the\ BFS\ tree$}\label{alg:VF2PPProcess1}
 \begin{algorithmic}[1]
 \Procedure{VF2++ProcessLevel}{$V_{d}$} \While{$V_d\neq\emptyset$}
-\State $m\in$ arg min$_{F_\mathcal{M}\circ\ lab}($ arg max$_{deg}($arg
+\State $m\in$ arg min$_{F_\mathcal{M}\circ\ \mathcal{L}}($ arg max$_{deg}($arg
 max$_{Conn_{\mathcal{M}}}(V_{d})))$ \State $V_d:=V_d\backslash m$
 \State Append node $m$ to the end of $\mathcal{M}$ \State Refresh
 $F_\mathcal{M}$ \EndWhile \EndProcedure
@@ -795,7 +742,7 @@
 
 Algorithm~\ref{alg:VF2PPPseu} is a high level description of the
 matching order procedure of VF2++. It computes a BFS tree for each
-component in ascending order of their rarest $lab$ and largest $deg$,
+component in ascending order of their rarest node labels and largest $deg$,
 whose root vertex is the component's minimal
 node. Algorithm~\ref{alg:VF2PPProcess1} is a method to process a level of the BFS tree, which appends the nodes of the current level in descending
 lexicographic order by $(Conn_{\mathcal{M}},deg,-F_\mathcal{M})$ separately
@@ -807,43 +754,53 @@
 
 \subsection{Cutting rules}
 \label{VF2PPCuttingRules}
-This section presents the cutting rule of VF2++ in the case of IND, which is improved
-by using extra information coming from the node labels. For other problem types, the rules can be formulated similarly.
+This section presents the cutting rules of VF2++, which are improved by using extra information coming from the node labels.
 \begin{notation}
-Let $\mathbf{\Gamma_{small}^{l}(u)}:=\{\tilde{u} : lab(\tilde{u})=l
-\wedge \tilde{u}\in \Gamma_{small} (u)\}$ and
-$\mathbf{\Gamma_{large}^{l}(v)}:=\{\tilde{v} : lab(\tilde{v})=l \wedge
-\tilde{v}\in \Gamma_{large} (v)\}$, where $u\in V_{small}$, $v\in
-V_{large}$ and $l$ is a label.
+Let $\mathbf{\Gamma_{1}^{l}(u)}:=\{\tilde{u} : \mathcal{L}(\tilde{u})=l
+\wedge \tilde{u}\in \Gamma_{1} (u)\}$ and
+$\mathbf{\Gamma_{2}^{l}(v)}:=\{\tilde{v} : \mathcal{L}(\tilde{v})=l \wedge
+\tilde{v}\in \Gamma_{2} (v)\}$, where $u\in V_{1}$, $v\in
+V_{2}$ and $l$ is a label.
 \end{notation}
 
+\subsubsection{Induced subgraph isomorphism}
 \begin{claim}
-\[LabCut_{IND}((u,v),M(s))\!:=\!\!\!\!\!\bigvee_{l\ is\ label}\!\!\!\!\!\!\!|\Gamma_{large}^{l} (v) \cap T_{large}(s)|\!<\!|\Gamma_{small}^{l}(u)\cap T_{small}(s)|\ \vee\]\[\bigvee_{l\ is\ label} \newline |\Gamma_{large}^{l}(v)\cap \tilde{T}_{large}(s)| < |\Gamma_{small}^{l}(u)\cap \tilde{T}_{small}(s)|\] is a cutting function by IND.
+\[LabCut_{IND}((u,v),\mathfrak{m}):=\bigvee_{l\ is\ label}|\Gamma_{2}^{l} (v) \cap T_{2}(\mathfrak{m})|\!<\!|\Gamma_{1}^{l}(u)\cap T_{1}(\mathfrak{m})|\ \vee\]\[\bigvee_{l\ is\ label} \newline |\Gamma_{2}^{l}(v)\cap \tilde{T}_{2}(\mathfrak{m})| < |\Gamma_{1}^{l}(u)\cap \tilde{T}_{1}(\mathfrak{m})|\] is a cutting function by IND.
+\end{claim}
+\subsubsection{Graph isomorphism}
+\begin{claim}
+\[LabCut_{ISO}((u,v),\mathfrak{m}):=\bigvee_{l\ is\ label}|\Gamma_{2}^{l} (v) \cap T_{2}(\mathfrak{m})|\!\neq\!|\Gamma_{1}^{l}(u)\cap T_{1}(\mathfrak{m})|\  \vee\]\[\bigvee_{l\ is\ label} \newline |\Gamma_{2}^{l}(v)\cap \tilde{T}_{2}(\mathfrak{m})| \neq |\Gamma_{1}^{l}(u)\cap \tilde{T}_{1}(\mathfrak{m})|\] is a cutting function by ISO.
 \end{claim}
 
+\subsubsection{Subgraph isomorphism}
+\begin{claim}
+\[LabCut_{SU\!B}((u,v),\mathfrak{m}):=\bigvee_{l\ is\ label}|\Gamma_{2}^{l} (v) \cap T_{2}(\mathfrak{m})|\!<\!|\Gamma_{1}^{l}(u)\cap T_{1}(\mathfrak{m})|\] is a cutting function by SUB.
+\end{claim}
 
-\subsection{Implementation details}
+
+
+\section{Implementation details}
 This section provides a detailed summary of an efficient
 implementation of VF2++.
 \subsubsection{Storing a mapping}
 After fixing an arbitrary node order ($u_0, u_1, ..,
-u_{|G_{small}|-1}$) of $G_{small}$, an array $M$ is usable to store
+u_{|G_{1}|-1}$) of $G_{1}$, an array $M$ is usable to store
 the current mapping in the following way.
 \[
  M[i] =
   \begin{cases} 
-   v & if\ (u_i,v)\ is\ in\ the\ mapping\\ INVALID &
+   v & if\ (u_i,v)\ is\ in\ the\ mapping\\ INV\!ALI\!D &
    if\ no\ node\ has\ been\ mapped\ to\ u_i,
   \end{cases}
 \]
-where $i\in\{0,1, ..,|G_{small}|-1\}$, $v\in V_{large}$ and $INVALID$
+where $i\in\{0,1, ..,|G_{1}|-1\}$, $v\in V_{2}$ and $INV\!ALI\!D$
 means "no node".
 \subsubsection{Avoiding the recurrence}
 The recursion of Algorithm~\ref{alg:VF2Pseu} can be realized
 as a \textit{while loop}, which has a loop counter $depth$ denoting the
 all-time depth of the recursion. Fixing a matching order, let $M$
 denote the array storing the all-time mapping. Based on Claim~\ref{claim:claimCoverFromLeft},
-$M$ is $INVALID$ from index $depth$+1 and not $INVALID$ before
+$M$ is $INV\!ALI\!D$ from index $depth$+1 and not $INV\!ALI\!D$ before
 $depth$. $M[depth]$ changes
 while the state is being processed, but the property is held before
 both stepping back to a predecessor state and exploring a successor
@@ -858,12 +815,12 @@
 \subsubsection{Calculating the candidates for a node}
 Being aware of Claim~\ref{claim:claimCoverFromLeft}, the
 task is not to maintain the candidate set, but to generate the
-candidate nodes in $G_{large}$ for a given node $u\in V_{small}$.  In
+candidate nodes in $G_{2}$ for a given node $u\in V_{1}$.  In
 case of any of the three problem types and a mapping $M$ if a node $v\in
-V_{large}$ is a potential pair of $u\in V_{small}$, then $\forall
-u'\in V_{small} : (u,u')\in
-E_{small}\ and\ u'\ is\ covered\ by\ M\ \Rightarrow (v,Pair(M,u'))\in
-E_{large}$. That is, each covered neighbour of $u$ has to be mapped to
+V_{2}$ is a potential pair of $u\in V_{1}$, then $\forall
+u'\in V_{1} : (u,u')\in
+E_{1}\ and\ u'\ is\ covered\ by\ M\ \Rightarrow (v,Pair(M,u'))\in
+E_{2}$. That is, each covered neighbour of $u$ has to be mapped to
 a covered neighbour of $v$.
 
 Having said that, an algorithm running in $\Theta(deg)$ time is
@@ -879,16 +836,16 @@
 numbers $\{0,1,..,|K|-1\}$, where $K$ is the set of the labels. It
 enables $F_\mathcal{M}$ to be stored in an array. At first, the node order
 $\mathcal{M}=\emptyset$, so $F_\mathcal{M}[i]$ is the number of nodes
-in $V_{small}$ having label i, which is easy to compute in
-$\Theta(|V_{small}|)$ steps.
+in $V_{1}$ having label $i$, which is easy to compute in
+$\Theta(|V_{1}|)$ steps.
 
-Representing $\mathcal{M}\subseteq V_{small}$ as an array of
-size $|V_{small}|$, both the computation of the BFS tree, and processing its levels by Algorithm~\ref{alg:VF2PPProcess1} can be done inplace by swapping nodes.
+Representing $\mathcal{M}\subseteq V_{1}$ as an array of
+size $|V_{1}|$, both the computation of the BFS tree, and processing its levels by Algorithm~\ref{alg:VF2PPProcess1} can be done inplace by swapping nodes.
 
 \subsubsection{Cutting rules}
 In Section~\ref{VF2PPCuttingRules}, the cutting rules were
-described using the sets $T_{small}$, $T_{large}$, $\tilde T_{small}$
-and $\tilde T_{large}$, which are dependent on the all-time mapping
+described using the sets $T_{1}$, $T_{2}$, $\tilde T_{1}$
+and $\tilde T_{2}$, which are dependent on the all-time mapping
 (i.e. on the all-time state). The aim is to check the labeled cutting
 rules of VF2++ in $\Theta(deg)$ time.
 
@@ -896,93 +853,37 @@
 checking whether a node is in a certain set takes constant time,
 e.g. they are given by their 0-1 characteristic vectors. Let $L$ be an
 initially zero integer lookup table of size $|K|$. After incrementing
-$L[lab(u')]$ for all $u'\in \Gamma_{small}(u) \cap T_{small}(s)$ and
-decrementing $L[lab(v')]$ for all $v'\in\Gamma_{large} (v) \cap
-T_{large}(s)$, the first part of the cutting rules is checkable in
+$L[\mathcal{L}(u')]$ for all $u'\in \Gamma_{1}(u) \cap T_{1}(\mathfrak{m})$ and
+decrementing $L[\mathcal{L}(v')]$ for all $v'\in\Gamma_{2} (v) \cap
+T_{2}(s)$, the first part of the cutting rules is checkable in
 $\Theta(deg)$ time by considering the proper signs of $L$. Setting $L$
 to zero takes $\Theta(deg)$ time again, which makes it possible to use
 the same table through the whole algorithm. The second part of the
 cutting rules can be verified using the same method with $\tilde
-T_{small}$ and $\tilde T_{large}$ instead of $T_{small}$ and
-$T_{large}$. Thus, the overall complexity is $\Theta(deg)$.
+T_{1}$ and $\tilde T_{2}$ instead of $T_{1}$ and
+$T_{2}$. Thus, the overall complexity is $\Theta(deg)$.
 
-An other integer lookup table storing the number of covered neighbours
-of each node in $G_{large}$ gives all the information about the sets
-$T_{large}$ and $\tilde T_{large}$, which is maintainable in
+Another integer lookup table storing the number of covered neighbours
+of each node in $G_{2}$ gives all the information about the sets
+$T_{2}$ and $\tilde T_{2}$, which is maintainable in
 $\Theta(deg)$ time when a pair is added or substracted by incrementing
 or decrementing the proper indices. A further improvement is that the
-values of $L[lab(u')]$ in case of checking $u$ is dependent only on
-$u$, i.e. on the size of the mapping, so for each $u\in V_{small}$ an
+values of $L[\mathcal{L}(u')]$ in case of checking $u$ are dependent only on
+$u$, i.e. on the size of the mapping, so for each $u\in V_{1}$ an
 array of pairs (label, number of such labels) can be stored to skip
 the maintaining operations. Note that these arrays are at most of size
-$deg$. Skipping this trick, the number of covered neighbours has to be
-stored for each node of $G_{small}$ as well to get the sets
-$T_{small}$ and $\tilde T_{small}$.
+$deg$.
 
-Using similar tricks, the consistency function can be evaluated in
+Using similar techniques, the consistency function can be evaluated in
 $\Theta(deg)$ steps, as well.
 
-\section{The VF2 Plus Algorithm}
-The VF2 Plus algorithm is a recently improved version of VF2. It was
-compared with the state of the art algorithms in \cite{VF2Plus} and
-has proved itself to be competitive with RI, the best algorithm on
-biological graphs.  \\ A short summary of VF2 Plus follows, which uses
-the notation and the conventions of the original paper.
+\section{Experimental results}
+This section compares the performance of VF2++ and VF2 Plus. According to
+our experience, both algorithms run faster than VF2 with orders of
+magnitude, thus its inclusion was not reasonable.
 
-\subsection{Ordering procedure}
-VF2 Plus uses a sorting procedure that prefers nodes in $V_{small}$
-with the lowest probability to find a pair in $V_{small}$ and the
-highest number of connections with the nodes already sorted by the
-algorithm.
-
-\begin{definition}
-$(u,v)$ is a \textbf{feasible pair} if $lab(u)=lab(v)$ and
-  $deg(u)\leq deg(v)$, where $u\in{V_{small}}$ and $ v\in{V_{large}}$.
-\end{definition}
-$P_{lab}(L):=$ a priori probability to find a node with label $L$ in
-$V_{large}$
-\newline
-$P_{deg}(d):=$ a priori probability to find a node with degree $d$ in
-$V_{large}$
-\newline
-$P(u):=P_{lab}(L)*\bigcup_{d'>d}P_{deg}(d')$\\ $M$ is the set of
-already sorted nodes, $T$ is the set of nodes candidate to be
-selected, and $degreeM$ of a node is the number of its neighbours in
-$M$.
-\begin{algorithm}
-\algtext*{EndIf}%ne nyomtasson end if-et
-\algtext*{EndFor}%nenyomtasson ..  
-\algtext*{EndProcedure}%ne nyomtasson ..
-\algtext*{EndWhile}
-\caption{}\label{alg:VF2PlusPseu}
-\begin{algorithmic}[1]
-\Procedure{VF2 Plus order}{} \State Select the node with the lowest
-$P$.  \If {more nodes share the same $P$} \State select the one with
-maximum degree \EndIf \If {more nodes share the same $P$ and have the
-  max degree} \State select the first \EndIf \State Put the selected
-node in the set $M$. \label{alg:putIn} \State Put all its unsorted
-neighbours in the set $T$.  \If {$M\neq V_{small}$} \State From set
-$T$ select the node with maximum $degreeM$.  \If {more nodes have
-  maximum $degreeM$} \State Select the one with the lowest $P$ \EndIf
-\If {more nodes have maximum $degreeM$ and $P$} \State Select the
-first.  \EndIf \State \textbf{goto \ref{alg:putIn}.}  \EndIf
-\EndProcedure
-\end{algorithmic}
-\end{algorithm}
-
-Using these notations, Algorithm~\ref{alg:VF2PlusPseu}
-provides the description of the sorting procedure.
-
-Note that $P(u)$ is not the exact probability of finding a consistent
-pair for $u$ by choosing a node of $V_{large}$ randomly, since
-$P_{lab}$ and $P_{deg}$ are not independent, though calculating the
-real probability would take quadratic time, which may be reduced by
-using fittingly lookup tables.
-
-\section{Experimental results}
-This section compares the performance of VF2++ and VF2 Plus. Both
-algorithms have run faster with orders of magnitude than VF2, thus its
-inclusion was not reasonable.
+The algorithms were implemented in C++ using the open source
+LEMON graph and network optimization library\cite{LEMON}. The test were carried out on a linux based system with an Intel i7 X980 3.33 GHz CPU and 6 GB of RAM.
 \subsection{Biological graphs}
 The tests have been executed on a recent biological dataset created
 for the International Contest on Pattern Search in Biological
@@ -996,7 +897,7 @@
 contact map dataset contains graphs with 150-800 nodes and an average
 degree of 20.  \\
 
-In the following, the induced subgraph isomorphism and the graph
+In the following, both the induced subgraph isomorphism and the graph
 isomorphism will be examined.
 
 This dataset provides graph pairs, between which all the induced subgraph isomorphisms have to be found. For runtime results, please see Figure~\ref{fig:bioIND}.
@@ -1258,8 +1159,8 @@
 small graphs of various size.
 
 For each chart, a number $0<\rho< 1$ has been fixed, and the following
-has been executed 150 times. Generating a large graph $G_{large}$ of an average degree of $\delta$,
-choose 10 of its induced subgraphs having $\rho\ |V_{large}|$ nodes,
+has been executed 150 times. Generating a large graph $G_{2}$ of an average degree of $\delta$,
+choose 10 of its induced subgraphs having $\rho\ |V_{2}|$ nodes,
 and for all the 10 subgraphs find a mapping by using both the graph
 matching algorithms.  The $\delta = 5, 10, 35$ and $\rho = 0.05, 0.1,
 0.3, 0.6, 0.8, 0.95$ cases have been examined, see
@@ -1581,9 +1482,7 @@
 
 
 \section{Conclusion}
-In this paper, after providing a short summary of the recent
-algorithms, a new graph matching algorithm based on VF2, called VF2++,
-has been presented and analyzed from a practical viewpoint.
+This paper presented VF2++, a new graph matching algorithm based on VF2, called VF2++, and analyzed it from a practical viewpoint.
 
 Recognizing the importance of the node order and determining an
 efficient one, VF2++ is able to match graphs of thousands of nodes in
@@ -1593,8 +1492,8 @@
 most of the unfruitful branches without going astray.
 
 In order to show the efficiency of the new method, it has been
-compared to VF2 Plus, which is the best concurrent algorithm based on
-\cite{VF2Plus}.
+compared to VF2 Plus\cite{VF2Plus}, which is the best contemporary algorithm.
+.
 
 The experiments show that VF2++ consistently outperforms VF2 Plus on
 biological graphs. It seems to be asymptotically faster on protein and
@@ -1603,8 +1502,8 @@
 asymptotic behaviour on protein graphs.
 
 Regarding random sparse graphs, not only has VF2++ proved itself to be
-faster than VF2 Plus, but it has a practically linear behaviour both
-in the case of induced subgraph- and graph isomorphism, as well.
+faster than VF2 Plus, but it also has a practically linear behaviour both
+in the case of induced subgraph- and graph isomorphism.
 
 
 




