The MJRTY Algorithm

Boyer and Moore's MJRTY algorithm finds the candidate who has the absolute majority in an electorate if any candidate has it. It runs in time linear in the size of the electorate N and with only maintaining two counters i and k, together with a variable cand holding the current leader.

The algorithm works by first appointing an arbitrary candidate as the one with absolute majority. It's majority lead k is set to 0. Then, as the electorate is scanned it increments k when the voter chose the current leader, and decrements k when the voter chose a different candidate. When k=0, cand gets assigned the value of the candidate that the current voter voted for.

Boyer and Moore check a Fortran implementation of the algorithm. Others have taken a functional version of it, we will here present a version in SPL.

type cand
local cand : cand
in N : [1..]
in A : array [1..N] of cand
local k : int where k = 0
local i : int where i = 1

l0: while i <= N do
    [l1: 
    << cand := if k = 0 then A[i] else cand;
       k := k + (if k>0 /\ cand != A[i] then -1 else 1);
       i := i + 1	
    >>];

l2: (k,i) := (if 2*k > N then k else 0,1);
l3: while i<=N /\ 2*k <= N do
     [l4: (k,i) := (k + (A[i] = cand), i+1)];
l5:

The main specification is that when the algorithm terminates, then if k is more than half the size of N, then the value held in cand is indeed the majority leader (dually one can require that if there is a majority leader, then k is more than half the size of N and the current value of cand holds this candidate).

To specify the english specification we define an auxiliary function count counting the number of candidates, and give the main specification in spec.

      
 function count(c:cand,a:array [1..N] of cand,l:int,u:int):int =
               if l >= u then 0 else (c = a[u-1]) + count(c,a,l,u-1)

 CONJECTURE   spec: l5     ==> (2*k > N --> 2*count(cand,A,1,N+1) > N)

step-comments@cs.stanford.edu

Last modified: Fri Jul 24 11:46:27 PDT 1998