From: Martin Mares <mj@ucw.cz>
Date: Fri, 7 Mar 2008 13:55:27 +0000 (+0100)
Subject: First bits of verification.
X-Git-Tag: printed~186
X-Git-Url: http://mj.ucw.cz/gitweb/?a=commitdiff_plain;h=570f1069a00a80272d2073263a8f2d305253cff6;p=saga.git

First bits of verification.
---

diff --git a/adv.tex b/adv.tex
index e40c812..4b0e7be 100644
--- a/adv.tex
+++ b/adv.tex
@@ -541,7 +541,110 @@ which need careful handling, so we omit the description of this algorithm.
 
 %--------------------------------------------------------------------------------
 
-%\section{Verification of minimality}
+\section{Verification of minimality}
+
+Now we will turn our attention to a~slightly different problem: given a~spanning
+tree, how to verify that it is minimal? We will show that this can be achieved
+in linear time and it will serve as a~basis for the randomized linear-time
+MST algorithm in the next section.
+
+MST verification has been studied by Koml\'os \cite{komlos:verify}, who has
+proven that $\O(m)$ edge comparisons are sufficient, but his algorithm needed
+superlinear time to find the edges to compare. Dixon, Rauch and Tarjan
+have later shown in \cite{dixon:verify} that the overhead can be reduced
+to linear time on the RAM using preprocessing and table lookup on small
+subtrees. This algorithm was then simplified by King in \cite{king:verifytwo}.
+We will follow the results of Koml\'os and King, but as we have the power of the
+RAM data structures from Section~\ref{bitsect} at our command, we will not have
+to worry about much technical details.
+
+To verify that a~spanning~$T$ is minimal, it is sufficient to check that all
+edges outside~$T$ are $T$-heavy (by Theorem \ref{mstthm}). In fact, we will be
+able to find all $T$-light edges efficiently. For each edge $uv\in E\setminus T$,
+we will find the heaviest edge of the tree path $T[u,v]$ and compare its weight
+to $w(uv)$. It is therefore sufficient to solve this problem:
+
+\problem
+Given a~weighted tree~$T$ and a~set of \df{query paths} $Q \subseteq \{ T[u,v] ; u,v\in V(T) \}$
+specified by their endpoints, find the heaviest edge for every path in~$Q$.
+
+\para
+Finding the heaviest edges can be burdensome if the tree~$T$ is degenerated,
+so we will first reduce it to the same problem on a~balanced tree. We run
+the Bor\o{u}vka's algorithm on~$T$, which certainly produces $T$ itself, and we
+record the order in which the subtrees have been merged in another tree~$B(T)$.
+The queries on~$T$ can be then easily translated to queries on~$B(T)$.
+
+\defn
+For a~weighted tree~$T$ we define its \df{Bor\o{u}vka tree} $B(T)$ which records
+the execution of the Bor\o{u}vka's algorithm run on~$T$. The leaves of $B(T)$
+are exactly the vertices of~$T$, every internal vertex~$v$ at level~$i$ from the bottom
+corresponds to a~component tree~$C(v)$ formed in the $i$-th phase of the algorithm. When
+a~tree $C(v)$ selects an adjacent edge~$xy$ and gets merged with some other trees to form
+a~component $C(u)$, we add an~edge $uv$ to~$B(T)$ and set its weight to $w(xy)$.
+
+\obs
+As the algorithm finishes with a~single component after the last phase, the Bor\o{u}vka tree
+is really a~tree. All its vertices are on the same level and each internal vertex has
+at least two sons. Such trees will be called \df{complete branching trees.}
+
+\lemma
+For every pair of vertices $x,y\in V(T)$, the heaviest edge of the path $T[x,y]$
+has the same weight as the heaviest edge of~$B(T)[x,y]$.
+
+\proof
+\qed
+
+\para
+We will make one more simplification: For an~arbitrary tree~$T$, we split each
+query path $T[x,y]$ to two half-paths $T[x,a]$ and $T[a,y]$ where~$a$ is the
+lowest common ancestor of~$x$ and~$y$ in~$T$. It is therefore sufficient to
+consider only paths which connect a~vertex with one of its ancestors.
+
+Finding the common ancestors is not trivial, but Harel and Tarjan have shown
+in \cite{harel:nca} that linear time is sufficient on the RAM. Several more
+accessible algorithms have been developed since then (see the Alstrup's survey
+paper \cite{alstrup:nca} and a~particularly elegant algorithm shown by Bender
+and Falach-Colton in \cite{bender:lca}). Any of them implies the following
+theorem:
+
+\thmn{Lowest common ancestors}\id{lcathm}%
+On the RAM, it is possible to preprocess a~tree~$T$ in time $\O(n)$ and then
+answer lowest common ancestor queries presented online in constant time.
+
+\proof
+See for example Bender and Falach-Colton \cite{bender:lca}.
+\qed
+
+\para
+We summarize the reductions in the following lemma, also showing that they can
+be performed in linear time:
+
+\lemma
+For each tree~$T$ and a~set of query paths~$Q$ on~$T$, it is possible to find
+a~complete branching tree~$T'$ in linear time together with a~set~$Q'$ of query
+paths on~$T'$, such that the weights of the heaviest edges of the new paths can
+be transformed to the weights of the heaviest edges of the paths in~$Q$ in
+linear time.
+The tree $T$ has at most $2n(T)$ vertices. The set~$Q'$ contains
+at most~$2\vert Q\vert$ paths and each of them connects a~vertex of~$T'$ with one
+of its ancestors.
+
+\proof
+The tree~$T'$ will be the Bor\o{u}vka tree for~$T$. We run the contractive version
+of the Bor\o{u}vka's algorithm (Algorithm \ref{contbor}) on~$T$. It runs in linear time,
+for example because trees are planar (Theorem \ref{planarbor}). The construction of~$T'$
+itself adds only a~constant overhead to every step of the algorithm. As~$T'$ has~$m(T)=n(T)-1$
+leaves and it is a~complete branching tree, it has at most~$m(T)$ internal vertices,
+so~$n(T')\le 2n(T)$ as promised.
+
+For each query path $T[x,y]$ we find the lower common ancestor of~$x$ and~$y$
+using Theorem \ref{lcathm} and replace the path by the two half-paths. This
+produces a~set~$Q'$ of at most~$2\vert Q\vert$ paths. If we remember the origin
+of each of the new paths, the reconstruction of answers to the original queries
+is then trivial.
+\qed
+
 
 %--------------------------------------------------------------------------------
 
diff --git a/biblio.bib b/biblio.bib
index 6d9df00..d56cf90 100644
--- a/biblio.bib
+++ b/biblio.bib
@@ -1033,3 +1033,14 @@ inproceedings{ pettie:minirand,
   year={1998},
   publisher={ACM Press New York, NY, USA}
 }
+
+@article{ harel:nca,
+  title={{Fast algorithms for finding nearest common ancestors}},
+  author={Harel, D. and Tarjan, R.E.},
+  journal={SIAM Journal on Computing},
+  volume={13},
+  number={2},
+  pages={338--355},
+  year={1984},
+  publisher={Society for Industrial and Applied Mathematics Philadelphia, PA, USA}
+}