On Tue, Dec 19, 2000 at 09:43:27AM +0100, Sven LUTHER wrote: > What about writing some kind of code that resolve the vote in some kind of > easy to prove language, and then do some program property proofs on it ?
I'm not sure why this helped (because I didn't do it), but it did.
For something, X, not in the Smith set to win, we'd need to have:
every option in the Smith set beats X (coz it's not in the Smith set)
X doesn't appear in the against row (after some eliminations)
X does appear in the for row, so it beats some option, o
So, try to end up with something like:
Smith set: A B C
Winner: X
Other option: o
X o 90 0
A o 90 0
B o 90 0
C o 90 0
A B 60 30
B C 60 30
C A 60 30
A X 50 40
B X 50 40
C X 50 40
which would make all the cases where X loses get eliminated ASAP, and
the case where it wins never eliminated (so at the very least the voter
with a casting vote could choose it if they wanted).
This could arise from votes like:
30 ABCXo
20 BCAXo
10 XBCAo
30 XCABo
Which would be processed like:
(2) Initial totals table:
A B C X o
A - 60 30 50 90
B 30 - 60 50 90
C 60 30 - 50 90
X 40 40 40 - 90
o 0 0 0 0 -
(3) Adjusted totals table: (same as initial totals table)
(4,5,6) Winning criteria table:
Coord For Against
A/o 90 0
B/o 90 0
C/o 90 0
X/o 90 0
A/B 60 30
B/C 60 30
C/A 60 30
A/X 50 40
B/X 50 40
C/X 50 40
Note that A, B and C form a cycle, and each of A, B and C beat the other
two options, X and o, and thus A, B and C is the Smith set.
(7) All options appear in the "against" side
(8) All options appear in the "against" side (I'm not sure I can follow
this clause)
(9) Remove C/X and B/X,A/X, leaving:
A/o 90 0
B/o 90 0
C/o 90 0
X/o 90 0
A/B 60 30
B/C 60 30
C/A 60 30
(7) X appears in the "for" side (X/o), but not in the "against" side, and
is thus chosen.
Thus X, not in the Smith set, is chosen as the winner. Thus this method
doesn't meet the Smith criterion.
Also, the result changed by adding an option "o" which everybody
universally detested. If "o" hadn't been an option, "X" wouldn't have been
in the "for" side at all, and thus would've have ever been considered.
Cheers,
aj
--
Anthony Towns <[EMAIL PROTECTED]> <http://azure.humbug.org.au/~aj/>
I don't speak for anyone save myself. GPG signed mail preferred.
``Thanks to all avid pokers out there''
-- linux.conf.au, 17-20 January 2001
pgpDDiWa8rYpd.pgp
Description: PGP signature
