[EM] Automatic Criterion Checking

[bql at bolson.org]

I wish we had nice clean definitions of our favorite criteria that were 
amenable to automatic checking. Then we just implement any new method in a 
few lines of code, and run the checker. In most cases I believe the 
computations could be completed in a few hours or a few days on any of our 
common home computers.

For example, let's see if I can formulate an automatic check for 
"Independence of Irrelevant Alternatives".

For any set of voters who vote honest preferences about some number of 
candidates, removing any combination of the non-winning choices shall not 
change the winner.

Combinatorics:
For C choices and V voters. There are factorial(C) possible ranking 
preferences for a voter. Multiply that by V voters and you get "any set of 
voters". For 20 voters and 5 choices that's 5*4*3*2*20 = 2400 possible 
sets of voters. Note that making the number of voters large is relatively 
easier than making the number of choices large. Choosing 1,2 or 3 of the 4 
non-winning choices to discard results in 4 + 4*3/2 + 4*3*2/6 = 14 
combinations of the non-winning to be run in a trial election. Add one 
more for the base case of having all 5 choices in and that's 15 * 2400 = 
36000 trial elections to run. Easily computable.

Of course, what that exhaustively proves is only the 20 voters, 5 choices 
case. Is that good enough? How about 100 voters with 2,3,4,5 or 6 choices? 
That could probably still be run in a day.

Brian Olson
http://bolson.org/