Pivot partitioning by scanning: Difference between revisions
No edit summary |
No edit summary |
||
Line 26: | Line 26: | ||
== Induction basis == | == Induction basis == | ||
'''Abstract view:''' | |||
# Set <math>m_1</math> and <math>m_2</math> according to the loop invariant. | |||
# Initialize <math>i_1,i_2</math> and <math>i_3</math>. | |||
'''Implementation:''' | |||
# Set <math>m_1:=1</math> . | |||
# For <math>j \in {1,...,n}</math>: If <math>S[j]<p</math> increase <math>m_1</math> by <math>1</math>. | |||
# Set <math>m_2:m_1</math> | |||
# For <math>j \in {1,...,n}</math>: If <math>S[j]=p</math> increase <math>m_2</math> by <math>1</math>. | |||
# <math>i_1:=1</math>. | |||
# <math>i_2:=m_1</math>. | |||
# <math>i_3:=m_2</math>. | |||
# While <math>i_1<m_1</math> and <math>S[j]<p</math>, set <math>i_1:=i_1+1</math>. | |||
# While <math>i_2<m_2</math> and <math>S[j]=p</math> , set <math>i_2:=i_2+1</math>. | |||
# While <math>i_3<n</math> and <math>S[j]>p</math>, set <math>i_3:=i_3+1</math> . | |||
'''Proof:''' Obvious. | |||
'''Abstract view:''' <math>\forall v,w \in V</math> we set | '''Abstract view:''' <math>\forall v,w \in V</math> we set | ||
# <math>M(v,v):=0, \forall v \in V</math> | # <math>M(v,v):=0, \forall v \in V</math> | ||
Line 34: | Line 52: | ||
'''Proof:''' Nothing to show. | '''Proof:''' Nothing to show. | ||
==Induction basis== | |||
== Induction step == | == Induction step == |
Revision as of 16:59, 15 January 2015
Algorithmic problem: Pivot partioning by scanning
Prerequisites: None
Type of algorithm: loop
Auxiliary data: Five index pointers, [math]\displaystyle{ m_1,m_2,i_1,i_2,i_3 \in \mathbb N. }[/math]
Abstract View
Invariant:
- The values of [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] only depend on the input sequence and are, hence, constant throughout the loop. More specifically, in there are
- [math]\displaystyle{ m_1-1 }[/math] elements less than [math]\displaystyle{ p }[/math],
- [math]\displaystyle{ m_1-m_2 }[/math] elements equal to [math]\displaystyle{ p }[/math], and
- [math]\displaystyle{ n - m_2 }[/math]greater than [math]\displaystyle{ p }[/math].
- Before and after each iteration, it is:
- [math]\displaystyle{ 1 \le i_2 \le m_1 \le m_2 \le i_3 \le i_3 \le n+1 }[/math];
- [math]\displaystyle{ S[j] \lt p }[/math] for [math]\displaystyle{ j \in {1,...,i_1-1} }[/math]; if [math]\displaystyle{ i_1 \lt m_1 }[/math], it is [math]\displaystyle{ S[i_1] \nless p }[/math];
- [math]\displaystyle{ S[j] =p }[/math] for [math]\displaystyle{ j \in {m_1,...,i_2-1} }[/math]; if [math]\displaystyle{ i_2 \lt m_2 }[/math], it is [math]\displaystyle{ S[i_2] \ne p }[/math];
- [math]\displaystyle{ S[j] \gt p }[/math]for [math]\displaystyle{ j \in {m_2,...,i_3-1} }[/math]; if [math]\displaystyle{ i_3 \le m_1 }[/math], it is [math]\displaystyle{ S[i_3] \ngtr p }[/math].
Variant: At least one of [math]\displaystyle{ i_1,i_2 }[/math], and [math]\displaystyle{ i_3 }[/math] is increased by at least [math]\displaystyle{ 1 }[/math], none of them is decreased.
Break condition: It is [math]\displaystyle{ i_1=m_1, i_2=m_2 }[/math] and [math]\displaystyle{ i_3 = n+1 }[/math]
Induction basis
Abstract view:
- Set [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] according to the loop invariant.
- Initialize [math]\displaystyle{ i_1,i_2 }[/math] and [math]\displaystyle{ i_3 }[/math].
Implementation:
- Set [math]\displaystyle{ m_1:=1 }[/math] .
- For [math]\displaystyle{ j \in {1,...,n} }[/math]: If [math]\displaystyle{ S[j]\lt p }[/math] increase [math]\displaystyle{ m_1 }[/math] by [math]\displaystyle{ 1 }[/math].
- Set [math]\displaystyle{ m_2:m_1 }[/math]
- For [math]\displaystyle{ j \in {1,...,n} }[/math]: If [math]\displaystyle{ S[j]=p }[/math] increase [math]\displaystyle{ m_2 }[/math] by [math]\displaystyle{ 1 }[/math].
- [math]\displaystyle{ i_1:=1 }[/math].
- [math]\displaystyle{ i_2:=m_1 }[/math].
- [math]\displaystyle{ i_3:=m_2 }[/math].
- While [math]\displaystyle{ i_1\lt m_1 }[/math] and [math]\displaystyle{ S[j]\lt p }[/math], set [math]\displaystyle{ i_1:=i_1+1 }[/math].
- While [math]\displaystyle{ i_2\lt m_2 }[/math] and [math]\displaystyle{ S[j]=p }[/math] , set [math]\displaystyle{ i_2:=i_2+1 }[/math].
- While [math]\displaystyle{ i_3\lt n }[/math] and [math]\displaystyle{ S[j]\gt p }[/math], set [math]\displaystyle{ i_3:=i_3+1 }[/math] .
Proof: Obvious.
Abstract view: [math]\displaystyle{ \forall v,w \in V }[/math] we set
- [math]\displaystyle{ M(v,v):=0, \forall v \in V }[/math]
- [math]\displaystyle{ M(v,w):=l(v,w), (v,w) \in A }[/math]
- [math]\displaystyle{ M(v,w):= +\infty }[/math], otherwise
Implementation: Obvious.
Proof: Nothing to show.
Induction basis
Induction step
Abstract view:
Implementation:
Correctness: Let [math]\displaystyle{ p }[/math] denote a shoortest [math]\displaystyle{ (v,w }[/math]-path subject to the constraint that all internal nodes are taken from [math]\displaystyle{ \{u_1, \ldots, u_n \} }[/math].
- If [math]\displaystyle{ p }[/math] does not contain [math]\displaystyle{ u_i }[/math], [math]\displaystyle{ p }[/math] is even a shortest [math]\displaystyle{ (v,w) }[/math]-path such that all internal nodes are taken from [math]\displaystyle{ \{u_1, \ldots , u_{i-1} \} }[/math]. In this case, the induction hypothesis implies that the value of [math]\displaystyle{ M(v,w) }[/math] immediately before the i-th iteration equals the length of [math]\displaystyle{ p }[/math]. Clearly, the i-th iteration does not change the value of [math]\displaystyle{ M(v,w) }[/math] in this case.
- On the other hand, suppose [math]\displaystyle{ p }[/math] does contain [math]\displaystyle{ u_i }[/math]. Due to the prefix property, the segment of [math]\displaystyle{ p }[/math] from [math]\displaystyle{ v }[/math] to [math]\displaystyle{ u_i }[/math] and from [math]\displaystyle{ u_i }[/math] to [math]\displaystyle{ w }[/math] are a shortest [math]\displaystyle{ (v,u_i) }[/math]-path and a shortest [math]\displaystyle{ (u_i,w) }[/math]-path, respectively, subject to the constraint that all internal nodes are from [math]\displaystyle{ \{u_1, \ldots , u_{i-1} \} }[/math]. The induction hypothesis implies that tehese lengths equal the values [math]\displaystyle{ M(v,u_i) }[/math] and [math]\displaystyle{ M(u_i, w) }[/math], respectively.
Complexity
Statement: [math]\displaystyle{ \mathcal{O}(n^3) }[/math]
Proof: The overall loop has [math]\displaystyle{ n }[/math] iterations. In each iteration, we update all [math]\displaystyle{ n^2 }[/math] matrix entities. Each update requires a constant number of steps.