1.1 --- a/damecco.tex	Thu Nov 24 22:09:36 2016 +0100
     1.2 +++ b/damecco.tex	Fri Nov 25 23:47:31 2016 +0100
     1.3 @@ -570,22 +570,21 @@
     1.4  \]
     1.5  
     1.6  \subsection{Consistency}
     1.7 -This section defines the consistency functions for the different
     1.8 -problem types mentioned in Section~\ref{sec:CommProb}.
     1.9 +Suppose $p=(u,v)$, where $u\in V_{small}$ and $v\in V_{large}$, $s$ is
    1.10 +a state of the matching procedure, $M(s)$ is consistent mapping by
    1.11 +$PT$ and $lab(u)=lab(v)$.  $Cons_{PT}(p,M(s))$ checks whether
    1.12 +including pair $p$ into $M(s)$ leads to a consistent mapping by $PT$.
    1.13 +
    1.14 +For example, the consistency function of induced subgraph isomorphism is as follows.
    1.15  \begin{notation}
    1.16  Let $\mathbf{\Gamma_{small} (u)}:=\{\tilde{u}\in V_{small} :
    1.17  (u,\tilde{u})\in E_{small}\}$\\ Let $\mathbf{\Gamma_{large}
    1.18    (v)}:=\{\tilde{v}\in V_{large} : (v,\tilde{v})\in E_{large}\}$
    1.19  \end{notation}
    1.20 -Suppose $p=(u,v)$, where $u\in V_{small}$ and $v\in V_{large}$, $s$ is
    1.21 -a state of the matching procedure, $M(s)$ is consistent mapping by
    1.22 -$PT$ and $lab(u)=lab(v)$.  $Cons_{PT}(p,M(s))$ checks whether
    1.23 -including pair $p$ into $M(s)$ leads to a consistent mapping by $PT$.
    1.24  
    1.25 -\subsubsection{Induced subgraph isomorphism}
    1.26  $M(s)\cup \{(u,v)\}$ is a consistent mapping by $IND$ $\Leftrightarrow
    1.27  (\forall \tilde{u}\in M_{small}: (u,\tilde{u})\in E_{small}
    1.28 -\Leftrightarrow (v,Pair(M(s),\tilde{u}))\in E_{large})$.\newline The
    1.29 +\Leftrightarrow (v,Pair(M(s),\tilde{u}))\in E_{large})$. The
    1.30  following formulation gives an efficient way of calculating
    1.31  $Cons_{IND}$.
    1.32  \begin{claim}
    1.33 @@ -596,74 +595,27 @@
    1.34    consistency function in the case of $IND$.
    1.35  \end{claim}
    1.36  
    1.37 -\subsubsection{Graph isomorphism}
    1.38 -$M(s)\cup \{(u,v)\}$ is a consistent mapping by $ISO$
    1.39 -$\Leftrightarrow$ $M(s)\cup \{(u,v)\}$ is a consistent mapping by
    1.40 -$IND$.
    1.41 -\begin{claim}
    1.42 -$Cons_{ISO}((u,v),M(s))$ is a consistency function by $ISO$ if and
    1.43 -  only if it is a consistency function by $IND$.
    1.44 -\end{claim}
    1.45 -\subsubsection{Subgraph isomorphism}
    1.46 -$M(s)\cup \{(u,v)\}$ is a consistent mapping by $SUB$ $\Leftrightarrow
    1.47 -(\forall \tilde{u}\in M_{small}:\\(u,\tilde{u})\in E_{small}
    1.48 -\Rightarrow (v,Pair(M(s),\tilde{u}))\in E_{large})$.
    1.49 -\newline
    1.50 -The following formulation gives an efficient way of calculating
    1.51 -$Cons_{SUB}$.
    1.52 -\begin{claim}
    1.53 -$Cons_{SUB}((u,v),M(s)):= (\forall \tilde{u}\in \Gamma_{small}(u)
    1.54 -  \ \cap\ M_{small}(s):\\(v,Pair(M(s),\tilde{u}))\in E_{large})$ is a
    1.55 -  consistency function by $SUB$.
    1.56 -\end{claim}
    1.57 -
    1.58  \subsection{Cutting rules}
    1.59  $Cut_{PT}(p,M(s))$ is defined by a collection of efficiently
    1.60  verifiable conditions. The requirement is that $Cut_{PT}(p,M(s))$ can
    1.61  be true only if it is impossible to extended $M(s)\cup \{p\}$ to a
    1.62  whole mapping.
    1.63 +
    1.64 +As an example, the cutting function of induced subgraph isomorphism is presented.
    1.65  \begin{notation}
    1.66 -
    1.67  Let $\mathbf{\tilde{T}_{small}}(s):=(V_{small}\backslash
    1.68  M_{small}(s))\backslash T_{small}(s)$, and
    1.69  \\ $\mathbf{\tilde{T}_{large}}(s):=(V_{large}\backslash
    1.70  M_{large}(s))\backslash T_{large}(s)$.
    1.71  \end{notation}
    1.72 -\subsubsection{Induced subgraph isomorphism}
    1.73 +
    1.74  \begin{claim}
    1.75  $Cut_{IND}((u,v),M(s)):= |\Gamma_{large} (v)\ \cap\ T_{large}(s)| <
    1.76    |\Gamma_{small} (u)\ \cap\ T_{small}(s)| \vee |\Gamma_{large}(v)\cap
    1.77    \tilde{T}_{large}(s)| < |\Gamma_{small}(u)\cap
    1.78    \tilde{T}_{small}(s)|$ is a cutting function by $IND$.
    1.79  \end{claim}
    1.80 -\subsubsection{Graph isomorphism}
    1.81 -Note that the cutting function of induced subgraph isomorphism defined
    1.82 -above is a cutting function by $ISO$, too, however it is less
    1.83 -efficient than the following while their computational complexity is
    1.84 -the same.
    1.85 -\begin{claim}
    1.86 -$Cut_{ISO}((u,v),M(s)):= |\Gamma_{large} (v)\ \cap\ T_{large}(s)| \neq
    1.87 -  |\Gamma_{small} (u)\ \cap\ T_{small}(s)| \vee |\Gamma_{large}(v)\cap
    1.88 -  \tilde{T}_{large}(s)| \neq |\Gamma_{small}(u)\cap
    1.89 -  \tilde{T}_{small}(s)|$ is a cutting function by $ISO$.
    1.90 -\end{claim}
    1.91  
    1.92 -\subsubsection{Subgraph isomorphism}
    1.93 -\begin{claim}
    1.94 -$Cut_{SUB}((u,v),M(s)):= |\Gamma_{large} (v)\ \cap\ T_{large}(s)| <
    1.95 -  |\Gamma_{small} (u)\ \cap\ T_{small}(s)|$ is a cutting function by
    1.96 -  $SUB$.
    1.97 -\end{claim}
    1.98 -Note that there is a significant difference between induced and
    1.99 -non-induced subgraph isomorphism:
   1.100 -
   1.101 -\begin{claim}
   1.102 -\label{claimSUB}
   1.103 -$Cut_{SUB}'((u,v),M(s)):= |\Gamma_{large} (v)\ \cap\ T_{large}(s)| <
   1.104 -|\Gamma_{small} (u)\ \cap\ T_{small}(s)| \vee |\Gamma_{large}(v)\cap
   1.105 -\tilde{T}_{large}(s)| < |\Gamma_{small}(u)\cap \tilde{T}_{small}(s)|$
   1.106 -is \textbf{not} a cutting function by $SUB$.
   1.107 -\end{claim}
   1.108  
   1.109  \section{The VF2++ Algorithm}
   1.110  Although any total ordering relation makes the search space of VF2 a