/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * Approval Voting: A Prolog Program to Check Manipulability Results * * (c) 2007 by Ulle Endriss (ulle@illc.uva.nl) * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ /* * This is the program mentioned in the following paper: * * U. Endriss. Vote Manipulation in the Presence of Multiple Sincere Ballots. * Proc. 11th Conference on Theoretical Aspects of Rationality and Knowledge * (TARK-2007), June 2007. * * The program can be used to automatically prove results on the manipulability * of approval voting for a given number of candidates. It can also display * tables of outcomes of elections for different combinations of the ballot * cast by the would-be manipulator and the tally of approvals received from * the other voters. * * This program has been written for SWI-Prolog (www.swi-prolog.org), * but should also work with most other Prolog systems. * * To run the program, first start Prolog and compile this file; then enter * one of the following two types of query (for varying numbers of candidates): * * ?- table(3). % to generate tables such as Tables 1 and 2 from the paper * ?- theorem(5). % to prove theorems such as Theorems 2 and 3 from the paper * */ /* * * USER PREDICATES * * * * * * * * * * * * * * * * * * * * * * * * * * * */ /* table(+Candidates). * Print the full table of outcomes for a given number of candidates. * * There is one row for each "situation" before the final voter casts his vote. * Each of the candidates may be either pivotal (having received a maximum * number of approvals from the other voters), subpivotal (having received * exactly one approval less than the pivotal candidates), or insignificant * (having received fewer approvals than the subpivotal candidates and therefore * having no chance of winning). Pivotal candidates are marked by a P, * subpivotal candidates by an S, and insignificant candidates by an I * (so the notation differs somewhat from the TARK-2007 paper). * * Then there is one column for each possible ballot the final voter may choose. * Ballots are shown as a sequence of zeros and ones in square brackets. A 1 * signifies that the final voter approves of the candidate in question, a 0 * signifies that he does not approve of that candidate (so, again, the notation * is a little different from the TARK-2007 paper). * * The table cells show the outcome for each combination of situation and ballot. * The notation for outcomes is as in the TARK-2007 paper: For instance, if there * are 4 candidates, then 421 denotes the set including the most preferred * candidate (4) as well as the two least preferred candidates (21). * * Sample query and output: * ?- table(3). * ----------------------------------------------------- * | | [100] [110] [111] | [001] [010] [011] [101] | * ----------------------------------------------------- * | PPP | 3 32 321 | 1 2 21 31 | * | PPS | 3 32 32 | 321 2 2 3 | * | PPI | 3 32 32 | 32 2 2 3 | * | PSP | 3 3 31 | 1 321 1 31 | * | PSS | 3 3 3 | 31 32 321 3 | * | PSI | 3 3 3 | 3 32 32 3 | * | PIP | 3 3 31 | 1 31 1 31 | * | PIS | 3 3 3 | 31 3 31 3 | * | PII | 3 3 3 | 3 3 3 3 | * | SPP | 321 2 21 | 1 2 21 1 | * | SPS | 32 2 2 | 21 2 2 321 | * | SPI | 32 2 2 | 2 2 2 32 | * | SSP | 31 321 1 | 1 21 1 1 | * | SIP | 31 31 1 | 1 1 1 1 | * | IPP | 21 2 21 | 1 2 21 1 | * | IPS | 2 2 2 | 21 2 2 21 | * | IPI | 2 2 2 | 2 2 2 2 | * | ISP | 1 21 1 | 1 21 1 1 | * | IIP | 1 1 1 | 1 1 1 1 | * ----------------------------------------------------- * * This is the same table as Table 1 in the TARK-2007 paper. */ table(C) :- write_table_head(C), generate_situation(C, Situation), write('| '), write_situation(Situation), write(' | '), sincere_row(Situation), write('| '), insincere_row(Situation), write('|'), nl, fail. table(C) :- fill('-', (2 ** C) * (C + 3) + 5). /* theorem(+Candidates). * Derive and print out the manipulability theorem for the given number of * candidates. This predicate can be used to automatically generate theorems * such as Theorem 3 (manipulability for four candidates) from the TARK-2007 * paper. * * Sample query and output: * ?- theorem(5). * Theorem: In approval voting with 5 candidates, * suppose that all but one voter have cast their ballot. * Then the final voter has no incentive to cast an * insincere ballot, unless his preferences over sets * of candidates satisfy one of the following 10 conditions: * -- 54321 strictly dominates all of 5431, 4. * -- 54321 strictly dominates all of 5421, 4. * -- 54321 strictly dominates all of 542, 4. * -- 5432 strictly dominates all of 542, 4. * -- 54321 strictly dominates all of 541, 4. * -- 5431 strictly dominates all of 541, 4. * -- 5421 strictly dominates all of 541, 4. * -- 54321 strictly dominates all of 531, 5431, 3. * -- 5321 strictly dominates all of 531, 3. * -- 4321 strictly dominates all of 431, 3. * * These sequences of numbers encode election outcomes (before tie-breaking), * as described in the comments for the predicate table/1. */ theorem(C) :- findall( (InsO,SinOs), critical_pair(C,InsO,SinOs), List), remove_duplicates(List, NewList), length(NewList, Length), write_theorem_text(C, Length), member((InsOutcome,SinOutcomes), NewList), write('-- '), write_outcomes([InsOutcome]), write(' strictly dominates all of '), write_outcomes(SinOutcomes), write('. '), nl, fail. theorem(_). /* * * MAIN PREDICATES (GENERAL) * * * * * * * * * * * * * * * * * * * * * * * */ /* Throughout the program, ballots, situations and outcomes are represented * using lists of the following kind (the notation for printed solutions is * slightly different from this internal represenation, as discussed above): * * Ballots: [1,0,1,0,0} -> 5 candidates, approve of best and 3rd-best * Situations: [2,3,3,1,3] -> 3 means pivotal, 2 subpivotal, 1 insignificant * Outcomes: [4,3] -> 4th and 3rd least favourites are pre-winners */ /* generate_situation(+Candidates, -Situation). * If exhaustive backtracking is applied, this predicate will in turn generate * all "situations" regarding the relative number of approvals submitted for * each candidate before the final voter casts his ballot. Pivotal candidates * are represented using a 3, subpivotal candidates using a 2, and insignificant * ones using a 1. */ generate_situation(C, Situation) :- length(Situation, C), only_contains(Situation, [3,2,1]), \+ \+ member(3, Situation). /* generate_ballot(+Candidates, -Ballots). * If exhaustive backtracking is applied, this predicate will in turn generate * all ballots for a given number of candidates. */ generate_ballot(C, Ballot) :- length(Ballot, C), only_contains(Ballot, [0,1]), \+ \+ member(1, Ballot). /* is_sincere(+Ballot). * Check whether a given ballot is sincere. This means checking that the list * representing the ballot starts with a 1 and that it only contains 0s after * the first 0 encountered (if any). */ is_sincere([1|Rest]) :- !, is_sincere(Rest). is_sincere(Ballot) :- only_contains(Ballot, [0]). /* sincere_ballots(+Candidates, -Ballots). * Generate the list of all sincere ballots for the given number of candidates. */ sincere_ballots(C, Ballots) :- Goal = (generate_ballot(C,Ballot), is_sincere(Ballot)), findall(Ballot, Goal, Ballots). /* insincere_ballots(+Candidates, -Ballots). * Generate the list of all insincere ballots for the given number of candidates. */ insincere_ballots(C, Ballots) :- Goal = (generate_ballot(C,Ballot), \+ is_sincere(Ballot)), findall(Ballot, Goal, Ballots). /* vote(+Situation, +Ballot, -Otcome). * Compute the outcome of an election for a given situation (tally of approvals * for all but the final voter) and the ballot of the final voter. */ vote(Situation, Ballot, Outcome) :- add_lists(Situation, Ballot, FinalSituation), max(FinalSituation, MaxCount), make_outcome(FinalSituation, MaxCount, Outcome). /* vote_list(+Situation, +Ballots, -Outcomes). * Apply the voting rule to an entire list of ballots, but keep the situation fixed. */ vote_list(_, [], []). vote_list(Situation, [B|Ballots], [O|Outcomes]) :- vote(Situation, B, O), vote_list(Situation, Ballots, Outcomes). /* make_outcome(+FinalSituation, +MaxCount, -Outcome). * Given a tally of votes (final situation) and the maximal number occurring in * that list, compute the corresponding outcome using our notation. This means * collecting the positions (counting backwards) of the occurrences of that * maximal number in the first list in another list. */ make_outcome([], _, []). make_outcome([Max|Situation], Max, [Position|Outcome]) :- !, length([Max|Situation], Position), make_outcome(Situation, Max, Outcome). make_outcome([_|Situation], Max, Outcome) :- make_outcome(Situation, Max, Outcome). /* * * MAIN PREDICATES (TABLE) * * * * * * * * * * * * * * * * * * * * * * * * */ /* sincere_row(+Situation). * Print out the part of a row in the table corresponding to the sincere ballots. */ sincere_row(Situation) :- length(Situation, Candidates), generate_ballot(Candidates, Ballot), is_sincere(Ballot), vote(Situation, Ballot, Outcome), write_outcome(Candidates, Outcome), fail. sincere_row(_). /* insincere_row(+Situation). * Print out the part of a row in the table corresponding to the insincere ballots. */ insincere_row(Situation) :- length(Situation, Candidates), generate_ballot(Candidates, Ballot), \+ is_sincere(Ballot), vote(Situation, Ballot, Outcome), write_outcome(Candidates, Outcome), fail. insincere_row(_). /* * * MAIN PREDICATES (THEOREM) * * * * * * * * * * * * * * * * * * * * * * * */ /* critical_pairs(+Candidates, -InsincereOutcome, -Outcomes). * Find a critical pair for a given number if candidates. A critical pair * consists of a particular outcome forced by means of an insincere ballot * and the list of sincere outcomes it has to dominate for giving grounds for * manipulation. That is, critical pairs are the conditions (or exceptions) * listed in our theorems. It works by first generating a particular situation * (tally of votes of the others), all sincere ballots, and all insincere * ballots. Then we apply the voting rule to the chosen situation for every * possible ballot and generate the lists of "sincere outcomes" and of * "insincere outcomes". We pick one of these insincere outcomes, which must * not be dominated by any of the sincere outcomes, to try to build a critical * pair. Then we select all those sincere outcomes that are dominated by the * chose insincere outcome. Backtracking will generate all critical pairs. */ critical_pair(C, InsOutcome, Outcomes) :- generate_situation(C, Situation), sincere_ballots(C, SinBallots), insincere_ballots(C, InsBallots), vote_list(Situation, SinBallots, SinOutcomes), vote_list(Situation, InsBallots, InsOutcomes), member(InsOutcome, InsOutcomes), \+ any_dominates(C, SinOutcomes, InsOutcome), get_undominated(C, SinOutcomes, UndomSinOutcomes), remove_duplicates(UndomSinOutcomes, Outcomes). /* dominates(+Candidates, +Good, +Bad). * Check whether the set of candidates called Good dominates the set of * candidates called Bad, according to our axioms. The clever bits are * implemented further down ("theorem prover"). */ dominates(C, Good, Bad) :- dominated(C, Bad, Good). /* strictly_domaines(Candidates, +Good, +Bad). * The strict version of the above. */ strictly_dominates(C, Good, Bad) :- dominates(C, Good, Bad), \+ dominates(C, Bad, Good). /* any_dominates(+Candidates. +DomOuctomes, +Outcome). * For a given number of candidates, check whether any of the outcomes in thw * first list dominates the other outcome. */ any_dominates(C, DomOutcomes, Outcome) :- member(DomOutcome, DomOutcomes), dominates(C, DomOutcome, Outcome). /* get_undominated(+Candidates, +Outcomes, -UndominatedOutcomes). * Get all the undominated outcomes from a lits of outcomes. */ get_undominated(C, Outcomes, Undominated) :- get_undominated(C, Outcomes, Outcomes, Undominated). get_undominated(_, [], _, []). get_undominated(C, [H|T], Outcomes, [H|Undominated]) :- \+ (member(O,Outcomes), strictly_dominates(C, O, H)), !, get_undominated(C, T, Outcomes, Undominated). get_undominated(C, [_|T], Outcomes, Undominated) :- get_undominated(C, T, Outcomes, Undominated). /* * * THEOREM PROVER * * * * * * * * * * * * * * * * * * * * * * * * * * * * */ /* In this section, we implement the predicate dominated/3, which can be used * check whether a given set of candidates is dominated by a second given set * of candidates according to the axioms for preferences over sets of candidates * before tie-breaking proposed in the TARK-2007 paper. (The first argument of * dominated/3 is used to carry along the number of candidates.) * * This amounts to implementing a simple theorem prover for our axiom system. * We treat this as a (breadth-first) search problem. Suppose we want to check * whether "Bad" is dominated by "Good". We make "Bad" the initial state; "Good" * is the goal state. More precisely: any set dominated by "Good" using only the * axiom (DOM) is a goal state. Note that (DOM) implies reflexivity. Axioms (ADD) * and (REM) are used to move between states (from worse to better states). * Observe that transitivity is used implicitly (sequence of moves). * * Note: Strictly speaking, our approach requires proof that any theorem can be * derived using only a single application of (DOM) at the very end. An alternative * would have been to implement (DOM) also as a move and to use just reflexivity * for the goal condition (but that would be more complex). */ /* dominated(+Candidates, +Bad, +Good). * Check whether the set Bad is dominated by the set Good, for the given number * of candidates. Examples: * * ?- dominated(5, [4,2,1], [5,3]). * Yes * * ?- dominated(4, [3], [4,3,2,1]). * No * * ?- dominated(4, [4,3,2,1], [3]). * No */ dominated(C, Bad, Good) :- solve_breadthfirst(C, Good, Bad, _). /* Move from a bad to a good state (knowing the number of candidates C: */ move(C, Bad, Good) :- add(C, Bad, Good) ; rem(Bad, Good). add(C, [H|T], [X,H|T]) :- Min is H + 1, between(Min, C, X). rem(Bad, Good) :- append(Good, [_], Bad), \+ empty(Good). /* The goal is reached when (DOM) becomes applicable: */ goal(CurrState, GoalState) :- dom(CurrState, GoalState). dom([H1|Bad], [H2|Good]) :- H1 =< H2, dom(Bad, Good). dom([], []). /* Implementation of a standard breadth-first search algoritm: */ solve_breadthfirst(C, Goal, Node, Path) :- breadthfirst(C, Goal, [[Node]], RevPath), reverse(RevPath, Path). breadthfirst(_, Goal, [[Node|Path]|_], [Node|Path]) :- goal(Node, Goal). breadthfirst(C, Goal, [Path|Paths], SolutionPath) :- expand_breadthfirst(C, Path, ExpPaths), append(Paths, ExpPaths, NewPaths), breadthfirst(C, Goal, NewPaths, SolutionPath). expand_breadthfirst(C, [Node|Path], ExpPaths) :- findall([NewNode,Node|Path], move_cyclefree(C, Path,Node,NewNode), ExpPaths). move_cyclefree(C, Visited, Node, NextNode) :- move(C, Node, NextNode), \+ member(NextNode, Visited). /* * * SIMPLE PREDICATES FOR PRINTING * * * * * * * * * * * * * * * * * * * * */ /* write_situation(+Situation). * Print out the string encoding a given "situation". This means translating * a list of 1s, 2s and 3s into a sequence of Is, Ss and Ps. */ write_situation([]). write_situation([3|Rest]) :- write('P'), write_situation(Rest). write_situation([2|Rest]) :- write('S'), write_situation(Rest). write_situation([1|Rest]) :- write('I'), write_situation(Rest). /* write_ballot(+Ballot). * Print a given ballot. */ write_ballot(Ballot) :- write('['), write_list_elements(Ballot), write(']'). /* write_ballots(+Ballots). * Print a given list of ballots. */ write_ballots([]). write_ballots([H|T]) :- write_ballot(H), write(' '), write_ballots(T). /* write_outcome(+Candidates, +Outcome). * Print a single outcome wih spacing (to get the same length everywhere). */ write_outcome(C, Outcome) :- length(Outcome, Length), write(' '), write_list_elements(Outcome), fill(' ', C - Length + 2). /* write_outcomes(+Outcomes). * Print a list of outcomes (without any spacing). */ write_outcomes([]). write_outcomes([X]) :- !, write_list_elements(X). write_outcomes([H|T]) :- write_list_elements(H), write(', '), write_outcomes(T). /* write_table_head(+Candidates). * Print out the heading for the table for a given number of candidates. */ write_table_head(C) :- sincere_ballots(C, SincereBallots), insincere_ballots(C, InsincereBallots), BallotWidth is C + 3, BallotNum is 2 ** C, fill('-', BallotNum * BallotWidth + 5), nl, write('|'), fill(' ', BallotWidth - 1), write('| '), write_ballots(SincereBallots), write('| '), write_ballots(InsincereBallots), write('|'), nl, fill('-', BallotNum * BallotWidth + 5), nl. /* write_theorem_text(+Candidates, +Conditions). * Print out the generic text for the theorem, for a given number of candidates, * and a given number of conditions under which it does not apply. */ write_theorem_text(Candidates, Conditions) :- nl, write('Theorem: In approval voting with '), write(Candidates), write(' candidates,'), nl, write('suppose that all but one voter have cast their ballot.'), nl, write('Then the final voter has no incentive to cast an'), nl, write('insincere ballot, unless his preferences over sets'), nl, write('of candidates satisfy one of the following '), write(Conditions), write(' conditions:'), nl. /* * * GENERAL AUXILIARY PREDICATES * * * * * * * * * * * * * * * * * * * * * */ /* only_contains(+List, +Allowed). * Check that every element in the first list also occurs in the second. */ only_contains([], _). only_contains([H|T], Allowed) :- member(H, Allowed), only_contains(T, Allowed). /* add_lists(+List1, +List2, -List3). * Add the elements of two lists (assumed to be of equal length) to obtain * a third list. */ add_lists([], [], []). add_lists([H1|T1], [H2|T2], [H3|T3]) :- H3 is H1 + H2, add_lists(T1, T2, T3). /* remove_duplicates(+List, -CleanList). * Remove any duplicate elements from a given list. */ remove_duplicates([], []). remove_duplicates([H|T], Result) :- member(H, T), !, remove_duplicates(T, Result). remove_duplicates([H|T], [H|Result]) :- remove_duplicates(T, Result). /* empty(+List). * Check whether the given list is empty. */ empty([]). /* max(+List, -Max). * Compute the maximum of a given list of numbers. */ max([X], X). max([X,Y|R], Max) :- X > Y, !, max([X|R], Max). max([_,X|R], Max) :- max([X|R], Max). /* fill(+String, +Times). * Print out the given straing for the given number of times. */ fill(_, 0). fill(String, Times) :- Times > 0, write(String), TimesLeft is Times - 1, fill(String, TimesLeft). /* write_list_elements(+List). * Print the elements of a list without commas or square brackets. */ write_list_elements([]). write_list_elements([H|T]) :- write(H), write_list_elements(T).