Introduction
David Weir (U of Sussex) Program Analysis Term 1, 2015 1 / 192
Illustrative Problem
Use the Stable Match problem to illustate key concepts
What is a problem?
What is an algorithm?
What is a measure of progress?
How do we analyse an algorithm’s running time? How do we prove that an algorithm is correct?
David Weir (U of Sussex) Program Analysis Term 1, 2015 2 / 192
Problem to Consider
Matching up men and women
Jack
Fred
Tom
Sam
?
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
3 / 192
Perfect Match
Everyone paired with exactly one person
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
4 / 192
Preferences
Men’s preferences
1st
Jack Sue
Fred Amy Tom Amy
2nd
3rd 4th
Lily
Amy
Alice
Lily
Sue
Alice
Alice
Lily
Sue
Sam Women’s preferences
Amy
Lily
Sue Alice
1st
2nd
3rd 4th Tom Jack Tom Amy Sam Jack Fred Tom
Jack
Fred
Sam
Tom
Sam
Fred
Jack
Sam
Fred
Alice Lily Sue
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
5 / 192
Stability
Might some couple elope?
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
6 / 192
Stability
Need to consider preferences of men and women Jack Lily Amy Alice Sue
Lily
Sue
Alice
Alice
Lily
Sue
Fred
Tom
Sam Amy Lily
Amy
Amy Sue Alice
Alice Jack Fred Sam Tom Lily Jack Sue Tom Amy Sam Jack Fred Tom
Tom
Sam
Fred
Jack
Sam
Fred
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
7 / 192
An Instability
Consider Jack and Amy
Jack has been matched with Sue
Amy has been matched with Tom
Jack prefers Amy to Sue
Amy prefers Jack to Tom
Both Jack and Amy would prefer to be matched Instability in the matching
Jack Fred Tom Sam
Alice Lily Sue Amy
Lily
Amy
Alice Sue Amy Amy Alice
Jack
Fred
Alice Lily Sue Amy
Lily
Sue
Alice
Alice
Lily
Sue
Amy
Lily
Sue
Jack
Fred
Sam
Tom
Sam
Fred
Jack
Sam
Fred
Tom Tom Jack
Sam
Jack
Tom Fred Tom
Sam
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
8 / 192
It Takes Two to Tango
Consider Tom and Sue
Tom has been matched with Amy
Sue has been matched with Jack
Tom prefers Sue to Amy
but Sue prefers Jack to Tom
Only Tom would prefer the match with Sue Not an instability in the matching
Jack Fred Tom Sam
Alice Lily Sue Amy
Lily
Amy
Alice Sue Amy Amy Alice
Jack
Fred
Alice Lily Sue Amy
Lily
Sue
Alice
Alice
Lily
Sue
Amy
Lily
Sue
Jack
Fred
Sam
Tom
Sam
Fred
Jack
Sam
Fred
Tom Tom Jack
Sam
Jack
Tom Fred Tom
Sam
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
9 / 192
Another Matching
Is it stable?
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
10 / 192
Preferences
Jack Lily Amy Alice Sue
Lily
Sue
Alice
Alice
Lily
Sue
Fred
Tom
Sam Amy Lily
Amy
Amy Sue Alice
Alice Jack Fred Sam Tom Lily Jack Sue Tom Amy Sam Jack Fred Tom
Tom
Sam
Fred
Jack
Sam
Fred
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
11 / 192
Any Instabilities?
A pair where both prefer each other to the assigned match What about Tom and Lily?
Tom would prefer Alice or Lily to Sue
Alice does not like Tom!
Lily however would prefer Tom to her match Fred This is an instability in the matching
Jack Fred Tom Sam
Alice Lily Sue Amy
Lily
Amy
Alice Sue Amy Amy Alice
Jack
Fred
Alice
Lily
Sue Amy
Lily
Sue
Alice
Alice
Lily
Sue
Amy
Lily
Sue
Jack
Fred
Sam
Tom
Sam
Fred
Jack
Sam
Fred
Tom Tom Jack
Sam
Jack
Tom Fred Tom
Sam
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
12 / 192
Definitions
A matching is perfect if everyone is paired with exactly one person A perfect matching is stable if the are no instabilities
David Weir (U of Sussex) Program Analysis Term 1, 2015 13 / 192
Questions
Can a stable matching always be found?
How can we construct a stable match when one exists? Stable Match Problem
Applies to other situations:
— matching hospitals and patients
— matching employers and applicants
David Weir (U of Sussex) Program Analysis Term 1, 2015 14 / 192
What a Problem is and isn’t
What a problem is:
Specification of a relationship between inputs and outputs Usually a mapping — one valid output for a given input
What a problem isn’t:
Not a matter of doing something in a particular way! Not procedural
The Stable Match Problem is a fairly generic problem
David Weir (U of Sussex) Program Analysis Term 1, 2015 15 / 192
What an Algorithm is and isn’t
What an algorithm is:
Specification as to how to tackle a problem Can be abstract
We will use informal pseudo-code language
What an algorithm isn’t:
Not the same as a program
Programs implement algorithms
Same algorithm implemented in different languages
Solving a problem means getting valid output for each input given to the algorithm
David Weir (U of Sussex) Program Analysis Term 1, 2015 16 / 192
Question for you
Write down a specification of the sorting problem.
David Weir (U of Sussex) Program Analysis Term 1, 2015 17 / 192
Question for you
Write down a specification of the sorting problem.
Input: A sequence of values A and an ordering relation r Output: A permutation of A that is in sorted order according to the relation r
David Weir (U of Sussex) Program Analysis Term 1, 2015 17 / 192
Question for you
Write down a specification of the problem that the binary search algorithm solves
David Weir (U of Sussex) Program Analysis Term 1, 2015 18 / 192
Question for you
Write down a specification of the problem that the binary search algorithm solves
Input: A sequence of values A that are ordered and a search item a
Output: true if a is in A, and false otherwise.
David Weir (U of Sussex) Program Analysis Term 1, 2015 18 / 192
Algorithm
Initialize each person to be free
while there’s a free man who hasn’t proposed to every woman
Choose one such man m
Let w be 1st woman on m’s list to whom m not proposed if w is free
assign m and w to be engaged else if w prefers m to her fiance ́ m′
assign m and w to be engaged, and m′ to be free else
w rejects m
Gale and Shapley, 1962
David Weir (U of Sussex) Program Analysis Term 1, 2015 19 / 192
Illustration
Initially, everyone is free
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Choose m = Tom Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Alice
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
✔
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Alice is free so Tom and Alice become engaged
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
✔
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Choose m = Jack Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
✔
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Lily
✔
✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Lily is free, so Jack and Lily become engaged to each other
✔
✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Choose m = Fred Jack
Alice Lily
Sue Amy
✔
✔
Fred
Tom
Sam
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Lily
✔
✔
✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Lily is already engaged to Jack, but prefers Fred
✔
✔
✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Jack and Lily break engagement and Fred and Lily become engaged
✔
✔
✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Choose m = Jack Jack
Alice Lily
Sue Amy
✔
✔
✔
Fred
Tom
Sam
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Amy
✔
✔
✔ ✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Amy is free, so Jack and Amy become engaged to each other
✔
✔
✔ ✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
m = Sam
✔
✔
✔ ✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Amy
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Amy is already engaged to Jack, but prefers Sam
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Jack and Amy break engagement and Sam and Amy become engaged
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
m = Jack
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Alice
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Alice is already engaged to Tom, but prefers Jack
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Tom and Alice break engagement and Jack and Alice become engaged
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
m = Tom
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Lily
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Lily is already engaged to Fred, but prefers Tom
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Fred and Lily break engagement and Tom and Lily become engaged
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
m = Fred
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
w = Sue
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
Sue is free, so Fred and Sue become engaged to each other
✔
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Illustration
No one is now free, so a stable match has been established
✔
✔
✔
✔
✔
✔ ✔✔
Jack
Fred
Tom
Sam
Alice Lily
Sue Amy
David Weir (U of Sussex)
Program Analysis
Term 1, 2015
20 / 192
Jack Lily Fred Lily Tom Alice Sam Amy
Amy Alice Sue Sue Alice Amy Lily Sue Amy Lily Sue Alice
Alice Jack Lily Tom Sue Jack Amy Sam
Fred Sam Tom Sam Fred Jack Sam Fred Tom Jack Fred Tom
Example for you
Apply the algorithm to this problem instance.
Jack
Sue
Alice
Amy
Lily
Alice
Tom
Sam
Fred
Jack
Fred
Amy
Alice
Sue
Lily
Lily
Jack
Fred
Sam
Tom
Tom
Amy
Sue
Lily
Alice
Sue
Tom
Fred
Sam
Jack
Sam
Alice
Sue
Lily
Amy
Amy
Tom
Fred
Jack
Sam
Always choose man in order of rows in table
David Weir (U of Sussex) Program Analysis Term 1, 2015 21 / 192
Example for you
Apply the algorithm to this problem instance.
Jack
Sue
Alice
Amy
Lily
Alice
Tom
Sam
Fred
Jack
Fred
Amy
Alice
Sue
Lily
Lily
Jack
Fred
Sam
Tom
Tom
Amy
Sue
Lily
Alice
Sue
Tom
Fred
Sam
Jack
Sam
Alice
Sue
Lily
Amy
Amy
Tom
Fred
Jack
Sam
Always choose man in order of rows in table
Tom paired with Amy Sam paired with Alice Fred paired with Sue Jack paired with Lily
David Weir (U of Sussex) Program Analysis Term 1, 2015 21 / 192
Algorithm
Initialize each person to be free
while there’s a free man who hasn’t proposed to every woman
Choose one such man m
Let w be 1st woman on m’s list to whom m not proposed if w is free
assign m and w to be engaged else if w prefers m to her fiance ́ m′
assign m and w to be engaged, and m′ to be free else
w rejects m
Gale and Shapley, 1962
David Weir (U of Sussex) Program Analysis Term 1, 2015 22 / 192
Questions for you
Give a problem instance involving two men and two women where there is only one stable match
David Weir (U of Sussex) Program Analysis Term 1, 2015 23 / 192
Questions for you
Give a problem instance involving two men and two women where there is only one stable match
manA
womanA
womanB
womanA
manA
manB
manB
womanB
womanA
womanB
manB
manA
David Weir (U of Sussex) Program Analysis Term 1, 2015 23 / 192
Questions for you
Give a problem instance involving two men and two women where there are two stable matches. Which one will the algorithm find?
David Weir (U of Sussex) Program Analysis Term 1, 2015 24 / 192
Questions for you
Give a problem instance involving two men and two women where there are two stable matches. Which one will the algorithm find?
manA
womanA
womanB
womanA
manB
manA
manB
womanB
womanA
womanB
manA
manB
David Weir (U of Sussex) Program Analysis Term 1, 2015 24 / 192
Issues
Is the algorithm guaranteed to terminate?
How efficient is the algorithm?
Can we be certain that the algorithm always finds a stable match? How fair is the algorithm?
Does it matter how we resolve the non-determinism?
David Weir (U of Sussex) Program Analysis Term 1, 2015 25 / 192
Termination
How many times could the while loop be executed?
Need some measure of progress
— a value that monotonically increases as number of executions of loop increases
Consider: the number of men that are still free
Reject: this doesn’t necessarily decrease each time loop is
executed
Consider: the number of engaged couples
Reject: this doesn’t necessarily increase each time loop is executed
David Weir (U of Sussex) Program Analysis Term 1, 2015 26 / 192
Measure of Progress
The number of proposals made so far
Always increases by 1 when loop executed Upper limit on number of proposals is n2
— where n is number of men (and number of women) Gives upper limit on executions of while loop
The algorithm will therefore always terminate
David Weir (U of Sussex) Program Analysis Term 1, 2015 27 / 192
Efficiency
Running time will depend on how long it takes for each execution of loop
Possible to do it in constant time
We will consider this in detail in the exercise classes Needs more detailed consideration of data structures
David Weir (U of Sussex) Program Analysis Term 1, 2015 28 / 192
Proving Correctness
A stable match is always found
Let’s show that it would be a contradiction to assert that . . .
there is an unstable pair in a match produced by the algorithm
A proof by contradiction
David Weir (U of Sussex) Program Analysis Term 1, 2015 29 / 192
Continuing Proof of Correctness
Suppose we have the following:
an unstable pair m and w
m paired by the algorithm with w′ ̸= w w paired by the algorithm with m′ ̸= m
Instability means:
m prefers w to w′
w refers m to m′
David Weir (U of Sussex) Program Analysis Term 1, 2015 30 / 192
Completing Proof of Correctness
Case 1: m didn’t propose to w at any point
m proposes in decreasing order of preference m must have proposed to w′
So w′ must be preferred to w by m Contradicts previous assumption
Case 2: m proposed to w but was rejected (immediately or at later point)
w would only reject m in favour of a man she preferred So m′ must be preferred to m by w
Contradicts previous assumption
David Weir (U of Sussex) Program Analysis Term 1, 2015 31 / 192