From: Martin Mares Date: Sat, 8 Mar 2008 21:17:22 +0000 (+0100) Subject: More verification. X-Git-Tag: printed~180 X-Git-Url: http://mj.ucw.cz/gitweb/?a=commitdiff_plain;h=e4ece93696bd08db4ef45ed8b29e76ba6c7848c4;p=saga.git More verification. --- diff --git a/adv.tex b/adv.tex index 8eff275..69bdcae 100644 --- a/adv.tex +++ b/adv.tex @@ -716,7 +716,8 @@ We will calculate the number of comparisons~$c_i$ performed when processing the going from the $(i+1)$-th to the $i$-th level of the tree. The levels are numbered from the bottom, so leaves are at level~0, the root is at level $\ell\le \lceil \log_2 n\rceil$ and there are $n_i\le n/2^i$ vertices -at the $i$-th level, so we consider exactly $n_i$ edges. +at the $i$-th level, so we consider exactly $n_i$ edges. To avoid taking a~logarithm +of zero, we will define $\vert T_e\vert=1$ for $T_e=\emptyset$. \def\eqalign#1{\null\,\vcenter{\openup\jot \ialign{\strut\hfil$\displaystyle{##}$&$\displaystyle{{}##}$\hfil \crcr#1\crcr}}\,} @@ -755,7 +756,7 @@ $$ \para When we combine this lemma with the above reduction, we get the following theorem: -\thmn{Verification of the MST, Koml\'os \cite{komlos:verify}} +\thmn{Verification of the MST, Koml\'os \cite{komlos:verify}}\id{verify}% For every weighted graph~$G$ and its spanning tree~$T$, it is sufficient to perform $\O(m)$ comparisons of edge weights to determine whether~$T$ is minimum and to find all $T$-light edges in~$G$. @@ -851,9 +852,9 @@ our data structures in \df{slots} of $s=1/3\cdot\lceil\log n\rceil$ bits each. We will show soon that it is possible to precompute a~table of any reasonable function whose arguments fit in two slots. -\em{Top masks:} The array~$T_e$ will be represented by bit masks. For each +\em{Top masks:} The array~$T_e$ will be represented by a~bit mask~$M_e$ called the \df{top mask.} For each of the possible tops~$t$ (i.e., the ancestors of the current vertex), we store -a~single bit telling whether $t\in T_e$. Each bit mask fits in $\lceil\log n\rceil$ +a~single bit telling whether $t\in T_e$. Each top mask fits in $\lceil\log n\rceil$ bits and therefore in a~single machine word. If needed, it can be split to three slots. \em{Small and big lists:} The heaviest edge found so far for each top is stored @@ -861,14 +862,14 @@ by the algorithm in the array~$H_e$. Instead of keeping the real array, we store the labels of these edges in a~list encoded in a~bit string. Depending on the size of the list, we use two one of two possible encodings: \df{Small lists} are stored in a~vector which fits in a~single slot, with -the unused entries filled by a~special constant, so that we can infer the +the unused fields filled by a~special constant, so that we can infer the length of the list. If the data do not fit in a~small list, we use a~\df{big list} instead, which is stored in $\O(\log\log n)$ words, each of them containing a~slot-sized vector. Unlike the small lists, we use the big lists as arrays. If a~top~$t$ of depth~$d$ is active, we keep the corresponding entry of~$H_e$ in the $d$-th -entry of the big list. Otherwise, we keep that entry unused. +field of the big list. Otherwise, we keep that entry unused. We will want to perform all operations on small lists in constant time, but we can afford spending time $\O(\log\log n)$ on every big list. This @@ -880,7 +881,7 @@ of a~big list, we do not have enough time to see the whole big list. To solve this problem, we will introduce \df{pointers} as another kind of edge identifiers. A~pointer is an~index to the nearest big list on the path from the small list containing the pointer to the root. As each big list has at most $\lceil\log n\rceil$ -entries, the pointer fits in~$\ell$ bits, but we need one extra bit to distinguish +fields, the pointer fits in~$\ell$ bits, but we need one extra bit to distinguish between normal labels and pointers. \lemma @@ -909,7 +910,10 @@ the \ of each slot first and then finding the slot containing the $k$-th one. \:$\(m)$ --- for a~slot-sized bit mask~$m$, it returns a~small list -of the positions of bits set in~$m$. +of the positions of bits set in~$\(m)$. + +\:$\ to find the fields of~$H_p$ which +shall be deleted. Then we apply \ to actually delete them. Pointers +can be retained as they still refer to the same ancestor list. + +\:\em{Big from big:} We can copy the whole~$H_p$, since the layout of the +big lists is fixed and the items we do not want simply end up as unused +fields in~$H_e$. + +\:\em{Small from big:} We use the operation \ to construct a~list +of pointers (we use bit masking to add the ``this is a~pointer'' flags). + +\:\em{Big from small:} First we have to dereference the pointers in the +small list~$S$. For each slot~$B_i$ of the ancestor big list, we construct +a~subvector of~$S$ containing only the pointers referring to that slot, +adjusted to be relative to the beginning of the slot (we use \ +and \ from Algorithm \ref{vecops} and bit masking). Then we +use a~precomputed table to replace the pointers by the fields of~$B_i$ +they point to. Finally, we $\bor$ together the partial results. + +Finally, we have to spread the fields of the small list to the whole big list. +This is similar: for each slot of the big list, we find the part of the small +list keeping the fields we want (\ on the sub-words of~$M_e$ before +and above the intended interval of depths) and we use a~precomputed table +to shift the fields to the right locations in the slot (controlled by the +sub-word of~$M_e$ in the intended interval). +\qeditem +\endlist + +\thmn{Verification of MST on the RAM}\id{ramverify}% +There is a~RAM algorithm, which for every weighted graph~$G$ and its spanning tree~$T$ +determines whether~$T$ is minimum and finds all $T$-light edges in~$G$. + +\proof +Implement the Koml\'os's algorithm from Theorem \ref{verify} with the data +structures developed in this section. +According to Lemma \ref{verfh}, it runs in time $\sum_e \O(\log\vert T_e\vert + q_e) += \O(\sum_e \log\vert T_e\vert) + \O(\sum_e q_e)$. The second sum is $\O(m)$ +as there are $\O(1)$ query paths per edge, the first sum is $\O(\#\hbox{comparisons})$, +which is $\O(m)$ by Theorem \ref{verify}. +\qed \FIXME{Mention online version} +\FIXME{Mention Buchsbaum} %--------------------------------------------------------------------------------