Pivot partitioning by scanning: Difference between revisions

From Algowiki
Jump to navigation Jump to search
 
(23 intermediate revisions by 2 users not shown)
Line 11: Line 11:
== Abstract View ==
== Abstract View ==
'''Invariant:'''  
'''Invariant:'''  
# The values of <math>m_1</math> and <math>m_2</math> only depend on the input sequence and are, hence, constant throughout the loop. More specifically, in there are
# The values of <math>m_1</math> and <math>m_2</math> only depend on the input sequence <math>S</math> and are, hence, constant throughout the loop. More specifically, in <math>S</math> there are
## <math>m_1-1</math> elements less than <math>p</math>,
## <math>m_1-1</math> elements less than <math>p</math>,
## <math>m_2-m_1</math> elements equal to <math>p</math>, and
## <math>m_2-m_1</math> elements equal to <math>p</math>, and
## <math>n - m_2+1</math> greater than <math>p</math>.
## <math>n - m_2+1</math> elements greater than <math>p</math>.
# Before and after each iteration, it is:
# Before and after each iteration, it is:
## <math>1 \le i_1 \le m_1 \le i_2 \le m_2 \le i_3 \le n+1</math>;
## <math>1 \le i_1 \le m_1 \le i_2 \le m_2 \le i_3 \le n+1</math>;
## <math>S[j] <p</math>  for <math> j \in \{1,...,i_1-1\}</math>; if <math>i_1 < m_1</math>, it is <math>S[i_1] \nless p</math>;
## <math>S[j] <p</math>  for <math> j \in \{1,...,i_1-1\}</math>; if <math>i_1 < m_1</math>, it is <math>S[i_1] \nless p</math>;
## <math>S[j] =p</math> for <math> j \in\{m_1,...,i_2-1\}</math>; if <math>i_2 < m_2</math>, it is <math>S[i_2] \ne p</math>;
## <math>S[j] =p</math> for <math> j \in\{m_1,...,i_2-1\}</math>; if <math>i_2 < m_2</math>, it is <math>S[i_2] \ne p</math>;
## <math>S[j] >p</math> for <math> j \in \{m_2,...,i_3-1\}</math>; if <math>i_3 \le m_1</math>, it is <math>S[i_3] \ngtr p</math>.   
## <math>S[j] >p</math> for <math> j \in \{m_2,...,i_3-1\}</math>; if <math>i_3 \le n</math>, it is <math>S[i_3] \ngtr p</math>.   


'''Variant:''' At least one of <math>i_1,i_2</math>, and <math>i_3</math> is increased by at least <math>1</math>, none of them is decreased.
'''Variant:''' At least one of <math>i_1,i_2</math>, and <math>i_3</math> is increased by at least <math>1</math>, none of them is decreased.


'''Break condition:''' It is <math>i_1=m_1, i_2=m_2</math> and <math>i_3 = n+1</math>
'''Break condition:''' It is <math>i_1=m_1, i_2=m_2</math> and <math>i_3 = n+1</math>.


== Induction basis ==
== Induction basis ==
Line 32: Line 32:
# Set <math>m_1:=1</math> .
# 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>.
# 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>
# 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>.
# 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_1:=1</math>.  
# <math>i_2:=m_1</math>.
# <math>i_2:=m_1</math>.
# <math>i_3:=m_2</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_1<m_1</math> and <math>S[i_1]<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_2<m_2</math> and <math>S[i_2]=p</math> , set <math>i_2:=i_2+1</math>.
# While <math>i_3<n+1</math> and <math>S[j]>p</math>, set <math>i_3:=i_3+1</math> .
# While <math>i_3<n+1</math> and <math>S[i_3]>p</math>, set <math>i_3:=i_3+1</math> .
'''Proof:''' Obvious.
'''Proof:''' Obvious.


Line 45: Line 45:


'''Abstract view:'''  
'''Abstract view:'''  
# Move each of <math>i_1,i_2</math>, and <math>i_3</math> forward as long as the invariant is not violated.
 
# If the algorithm is not done yet, identify two out of the three index pointers <math>i_1,i_2</math>, and <math>i_3</math>such that at least one of these two can be moved one step forward after a swap of the elements at these two positions.
# If the algorithm is not done yet, identify two out of the three index pointers <math>i_1,i_2</math>, and <math>i_3</math>such that at least one of these two can be moved one step forward after a swap of the elements at these two positions.
# Then move each of <math>i_1,i_2</math>, and <math>i_3</math> forward as long as the invariant is not violated.


'''Implementation:'''  
'''Implementation:'''  
Line 57: Line 58:
### Swap <math>S[i_1]</math> and <math>S[i_3]</math>.
### Swap <math>S[i_1]</math> and <math>S[i_3]</math>.
###Set <math>i_3:=i_3+1</math> until <math>i_3=n+1</math> or else <math>S[i_3] \ngtr p</math>.
###Set <math>i_3:=i_3+1</math> until <math>i_3=n+1</math> or else <math>S[i_3] \ngtr p</math>.
## While and , set .
## While <math>i_1<m_1</math> and <math>S[i_1]<p</math>: set <math>i_1:=i_1+1</math>.
# Otherwise (that is, <math>i_1=m_1</math>):
# Otherwise (that is, <math>i_1=m_1</math>):
## Swap <math>S[i_2]</math> and <math>S[i_3]</math>.
## Swap <math>S[i_2]</math> and <math>S[i_3]</math>.
## Set <math>i_2:=i_2+1</math> until <math>i_2=m2</math> or else <math>S[i_2] \ne p</math> .
## Set <math>i_2:=i_2+1</math> until <math>i_2=m_2</math> or else <math>S[i_2] \ne p</math> .
## Set <math>i_3:=i_3+1</math> until <math>i_3=n+1</math> or else <math>S[i_3] \ngtr p</math>.
## Set <math>i_3:=i_3+1</math> until <math>i_3=n+1</math> or else <math>S[i_3] \ngtr p</math>.


'''Correctness''': Due to the various "otherwise" clauses, all possible cases are covered. Therefore, it remains to show that the invariants are maintained in each of the considered cases.  
'''Correctness''': Due to the various "otherwise" clauses, all possible cases are covered. Therefore, it remains to show that the invariants are maintained in each of the considered cases.  
As the values of and are never changed after initialization, all three parts of the first invariant are trivially maintained. Since (resp., , ) is only increased in case (resp., , ), Invariant 2.1 is maintained as well. So, we will focus on Invariants 2.2-2.4.  
As the values of <math>m_1</math> and <math>m_2</math> are never changed after initialization, all three parts of the first invariant are trivially maintained. Since <math>i_1</math> (resp., <math>i_2</math>, <math>i_3</math>) is only increased in case <math>i_1<m_1</math> (resp., <math>i_2<m_2</math>, <math>i_3<n+1</math>), Invariant 2.1 is maintained as well. So, we will focus on Invariants 2.2-2.4.  
If Step 2 applies, maintenance of Invariants 2.2-2.4 might be obvious. So consider Step 3. If Step 3 applies, we know that , but  or (or both). Due to , all elements less than  are correctly placed at the positions . Therefore, both cases, the case  and  and the case  and  are impossible, because there cannot be exactly one wrongly placed element. In other words, it is and  in Step 3. Again due to , it is and . Steps 2.1.2 and 2.2.2 ensure and , so we have and . This observation justifies the procedure of Step 3.
If Step 2 applies, maintenance of Invariants 2.2-2.4 might be obvious. So consider Step 3. If Step 3 applies (<math>i_1=m_1</math>), the break condition is not yet met, so we know <math>i_2<m_2</math> or <math>i_3<n+1</math>, or both. Without loss of generality, assume <math>i_2<m_2</math> (the other case is mirror-symmetric). Invariant 2.3 implies <math>S[i_2]\neq p</math>, which amounts to <math>S[i_2]>p</math> in Step 3. So, not all elements <math>>p</math> are on the correct positions, which implies <math>i_3<n+1</math>. In summary, it is safe to apply Step 3.
 
== Java Implementation ==
<syntaxhighlight lang="java">
    //snipped from https://foo.algo.informatik.tu-darmstadt.de
    //preperated for Spec
    //AUTHOR: Thomas Lüdecke
    //30.05.2015 05:22 | git 4072e171
 
 
    private List<Integer> list executePivotPartitioning(int pivot, int m1, int m2List<Integer> list){
        //init and save
        int i1 = 0;
        int i2 = m1;
        int i3 = m2;
 
        //int i = 0; //Iteration Counter
        //Inductionbase
        while(i1 < m1 && list.get(i1) < pivot){
          i1++;
        }
 
        while(i2 < m2 && list.get(i2) == pivot){
          i2++;
        }
 
        while(i3 <list.size() && list.get(i3) > pivot){
          i3++;
        }
       
        //each Iteration is one induction step
        while(i1 < m1 || i2 < m2 || i3 < list.size()) {
 
            if(i1 < m1) {
                if(list.get(i1) == pivot) {
                    swap(i1,i2, list);
                    while(i2 < m2 && list.get(i2) == pivot){
                        i2++;
                    }
                }else{
                    swap(i1,i3, list);
                    while(i3 <list.size() && list.get(i3) > pivot){
                        i3++;
                    }
                }
                while(i1 < m1 && list.get(i1) < pivot){
                    i1++;
                }
                //i++; //iteration end
            }else{
                swap(i2,i3, list);
                while(i2 < m2 && list.get(i2) == pivot){
                    i2++;
                }
                while(i3 <list.size() && list.get(i3) > pivot){
                    i3++;
                }
                //i++; //iteration end
            }
        }
        return list;
    }
 
    //AUTHOR: Alexander Jandousek   
    private void swap(int i1, int i2, List<Integer> list){
        int temp = list.get(i1);
        list.set(i1, list.get(i2));
        list.set(i2, temp);
    }
 
    //These methods are used to init m1 and m2 before calling executePivotPartitioning(...)
    //AUTHOR: Alexander Jandousek
    private int calcM1(int pivot, List<Integer> list){
        int m1 = 0;
        for(int n : list){
            m1 = (n < pivot)? m1+1: m1;
        }
        return m1;
    }
 
    //AUTHOR: Alexander Jandousek, Thomas Lüdecke
    private int calcM2(int pivotList<Integer> list){
        int m2 = calcM1(pivot,list); //not optimized
        for(int n : list){
            m2 = (n == pivot)? m2+1: m2;
        }
        return m2;
    }   
</syntaxhighlight>

Latest revision as of 08:30, 30 May 2015

Algorithmic problem: Pivot partioning

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:

  1. The values of [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] only depend on the input sequence [math]\displaystyle{ S }[/math] and are, hence, constant throughout the loop. More specifically, in [math]\displaystyle{ S }[/math] there are
    1. [math]\displaystyle{ m_1-1 }[/math] elements less than [math]\displaystyle{ p }[/math],
    2. [math]\displaystyle{ m_2-m_1 }[/math] elements equal to [math]\displaystyle{ p }[/math], and
    3. [math]\displaystyle{ n - m_2+1 }[/math] elements greater than [math]\displaystyle{ p }[/math].
  2. Before and after each iteration, it is:
    1. [math]\displaystyle{ 1 \le i_1 \le m_1 \le i_2 \le m_2 \le i_3 \le n+1 }[/math];
    2. [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];
    3. [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];
    4. [math]\displaystyle{ S[j] \gt p }[/math] for [math]\displaystyle{ j \in \{m_2,...,i_3-1\} }[/math]; if [math]\displaystyle{ i_3 \le n }[/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:

  1. Set [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] according to the loop invariant.
  2. Initialize [math]\displaystyle{ i_1,i_2 }[/math] and [math]\displaystyle{ i_3 }[/math].

Implementation:

  1. Set [math]\displaystyle{ m_1:=1 }[/math] .
  2. 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].
  3. Set [math]\displaystyle{ m_2:=m_1 }[/math].
  4. 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].
  5. [math]\displaystyle{ i_1:=1 }[/math].
  6. [math]\displaystyle{ i_2:=m_1 }[/math].
  7. [math]\displaystyle{ i_3:=m_2 }[/math].
  8. While [math]\displaystyle{ i_1\lt m_1 }[/math] and [math]\displaystyle{ S[i_1]\lt p }[/math], set [math]\displaystyle{ i_1:=i_1+1 }[/math].
  9. While [math]\displaystyle{ i_2\lt m_2 }[/math] and [math]\displaystyle{ S[i_2]=p }[/math] , set [math]\displaystyle{ i_2:=i_2+1 }[/math].
  10. While [math]\displaystyle{ i_3\lt n+1 }[/math] and [math]\displaystyle{ S[i_3]\gt p }[/math], set [math]\displaystyle{ i_3:=i_3+1 }[/math] .

Proof: Obvious.

Induction step

Abstract view:

  1. If the algorithm is not done yet, identify two out of the three index pointers [math]\displaystyle{ i_1,i_2 }[/math], and [math]\displaystyle{ i_3 }[/math]such that at least one of these two can be moved one step forward after a swap of the elements at these two positions.
  2. Then move each of [math]\displaystyle{ i_1,i_2 }[/math], and [math]\displaystyle{ i_3 }[/math] forward as long as the invariant is not violated.

Implementation:

  1. If [math]\displaystyle{ i_1=m_1 }[/math] and [math]\displaystyle{ i_2=m_2 }[/math] and [math]\displaystyle{ i_3=n+1 }[/math], terminate the algorithm and return [math]\displaystyle{ m_1,m_2 }[/math].
  2. If [math]\displaystyle{ i_1\lt m_1 }[/math] :
    1. If [math]\displaystyle{ S[i_1]=p }[/math]:
      1. Swap [math]\displaystyle{ S[i_1] }[/math] and [math]\displaystyle{ S[i_2] }[/math].
      2. Set [math]\displaystyle{ i_2:=i_2+1 }[/math] until [math]\displaystyle{ i_2=m_2 }[/math] or else [math]\displaystyle{ S[i_2] \ne p }[/math].
    2. Otherwise (that is, [math]\displaystyle{ S[i_1]\gt p }[/math]):
      1. Swap [math]\displaystyle{ S[i_1] }[/math] and [math]\displaystyle{ S[i_3] }[/math].
      2. Set [math]\displaystyle{ i_3:=i_3+1 }[/math] until [math]\displaystyle{ i_3=n+1 }[/math] or else [math]\displaystyle{ S[i_3] \ngtr p }[/math].
    3. While [math]\displaystyle{ i_1\lt m_1 }[/math] and [math]\displaystyle{ S[i_1]\lt p }[/math]: set [math]\displaystyle{ i_1:=i_1+1 }[/math].
  3. Otherwise (that is, [math]\displaystyle{ i_1=m_1 }[/math]):
    1. Swap [math]\displaystyle{ S[i_2] }[/math] and [math]\displaystyle{ S[i_3] }[/math].
    2. Set [math]\displaystyle{ i_2:=i_2+1 }[/math] until [math]\displaystyle{ i_2=m_2 }[/math] or else [math]\displaystyle{ S[i_2] \ne p }[/math] .
    3. Set [math]\displaystyle{ i_3:=i_3+1 }[/math] until [math]\displaystyle{ i_3=n+1 }[/math] or else [math]\displaystyle{ S[i_3] \ngtr p }[/math].

Correctness: Due to the various "otherwise" clauses, all possible cases are covered. Therefore, it remains to show that the invariants are maintained in each of the considered cases. As the values of [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] are never changed after initialization, all three parts of the first invariant are trivially maintained. Since [math]\displaystyle{ i_1 }[/math] (resp., [math]\displaystyle{ i_2 }[/math], [math]\displaystyle{ i_3 }[/math]) is only increased in case [math]\displaystyle{ i_1\lt m_1 }[/math] (resp., [math]\displaystyle{ i_2\lt m_2 }[/math], [math]\displaystyle{ i_3\lt n+1 }[/math]), Invariant 2.1 is maintained as well. So, we will focus on Invariants 2.2-2.4. If Step 2 applies, maintenance of Invariants 2.2-2.4 might be obvious. So consider Step 3. If Step 3 applies ([math]\displaystyle{ i_1=m_1 }[/math]), the break condition is not yet met, so we know [math]\displaystyle{ i_2\lt m_2 }[/math] or [math]\displaystyle{ i_3\lt n+1 }[/math], or both. Without loss of generality, assume [math]\displaystyle{ i_2\lt m_2 }[/math] (the other case is mirror-symmetric). Invariant 2.3 implies [math]\displaystyle{ S[i_2]\neq p }[/math], which amounts to [math]\displaystyle{ S[i_2]\gt p }[/math] in Step 3. So, not all elements [math]\displaystyle{ \gt p }[/math] are on the correct positions, which implies [math]\displaystyle{ i_3\lt n+1 }[/math]. In summary, it is safe to apply Step 3.

Java Implementation

    //snipped from https://foo.algo.informatik.tu-darmstadt.de
    //preperated for Spec
    //AUTHOR: Thomas Lüdecke
    //30.05.2015 05:22 | git 4072e171


    private List<Integer> list executePivotPartitioning(int pivot, int m1, int m2,  List<Integer> list){
        //init and save
        int i1 = 0;
        int i2 = m1;
        int i3 = m2;

        //int i = 0; //Iteration Counter
        //Inductionbase
        while(i1 < m1 && list.get(i1) < pivot){
           i1++;
        }

        while(i2 < m2 && list.get(i2) == pivot){
           i2++;
        }

        while(i3 <list.size() && list.get(i3) > pivot){
           i3++;
        }
        
        //each Iteration is one induction step
        while(i1 < m1 || i2 < m2 || i3 < list.size()) {

            if(i1 < m1) {
                if(list.get(i1) == pivot) {
                    swap(i1,i2, list);
                    while(i2 < m2 && list.get(i2) == pivot){
                        i2++;
                    }
                }else{
                    swap(i1,i3, list);
                    while(i3 <list.size() && list.get(i3) > pivot){
                        i3++;
                    }
                }
                while(i1 < m1 && list.get(i1) < pivot){
                    i1++;
                }
                //i++; //iteration end
            }else{
                swap(i2,i3, list);
                while(i2 < m2 && list.get(i2) == pivot){
                    i2++;
                }
                while(i3 <list.size() && list.get(i3) > pivot){
                    i3++;
                }
                //i++; //iteration end
            }
        }
        return list;
    }

    //AUTHOR: Alexander Jandousek    
    private void swap(int i1, int i2, List<Integer> list){
        int temp = list.get(i1);
        list.set(i1, list.get(i2));
        list.set(i2, temp);
    }

    //These methods are used to init m1 and m2 before calling executePivotPartitioning(...)
    //AUTHOR: Alexander Jandousek
    private int calcM1(int pivot,  List<Integer> list){
        int m1 = 0;
        for(int n : list){
            m1 = (n < pivot)? m1+1: m1;
        }
        return m1;
    }

    //AUTHOR: Alexander Jandousek, Thomas Lüdecke
    private int calcM2(int pivot,  List<Integer> list){
        int m2 = calcM1(pivot,list); //not optimized
        for(int n : list){
            m2 = (n == pivot)? m2+1: m2;
        }
        return m2;
    }