%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Automated Analysis of Approval Elections
%%% (c) 2012 by Ulle Endriss (ulle.endriss@uva.nl)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% This is the program mentioned in the following paper:
%%%
%%% U. Endriss. Automated Analysis of Social Choice Problems:
%%% Approval Elections with Small Fields of Candidates.
%%% Proc. 24th Benelux Conference on Artificial Intelligence
%%% (BNAIC-2012), October 2012.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Usage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% To generate all critical situations and additional plain axioms
%%% (kel, gar, or s_p) for a given set of axioms and a given number of
%%% candidates, use the predicate prettyprint/2. Example:
%%%
%%% ?- prettyprint(gar, 4).
%%% Critical situation: [2, 3, 2, 3]
%%% Plain axiom needed: [1, 1, 1, 1] should be weakly dominated by one of:
%%% [[0, 1, 0, 0], [1, 1, 0, 1]]
%%% true ;
%%% Critical situation: [2, 2, 2, 3]
%%% Plain axiom needed: [1, 0, 1, 1] should be weakly dominated by one of:
%%% [[1, 0, 0, 1], [1, 1, 0, 1], [1, 1, 1, 1]]
%%% true ;
%%% fail.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% To count the number of critical pairs and additional plain axioms
%%% for a given set of axioms and a given number of candidates, use the
%%% predicate count/5. Example:
%%%
%%% ?- count(s_p, 6, Situations, Axioms, Status).
%%% Situations = 61,
%%% Axioms = 63,
%%% Status = possible.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Main predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Pretty-print variant of check/3:
prettyprint(Rule, N) :-
check(Rule, N, Sit:InsOut:SinOuts),
write('Critical situation: '), writeln(Sit),
write('Plain axiom needed: '), write(InsOut),
writeln(' should be weakly dominated by one of:'),
writeln(SinOuts), nl.
% Find the next critical situation and the plain axiom to fix it:
check(Rule, N, Sit:InsOut:SinOuts) :-
situation(N, Sit),
sincere_outcomes(Sit, AllSinOuts),
undominated(Rule, AllSinOuts, Tops),
ballot(N, InsBal), insincere(InsBal),
vote(Sit, InsBal, InsOut),
\+ (member(A,Tops), wdominates(Rule,A,InsOut)),
findall(A, (member(A,Tops),\+sdominates(Rule,InsOut,A)), SinOuts).
% Count critical situations and additional plain axioms:
count(Rule, N, SitCount, AxiomCount, Flag) :-
findall(X, check(Rule,N,X), List),
setof(Sit, X^member(Sit:X,List), SitList),
length(SitList, SitCount),
setof(Y:Z, X^member(X:Y:Z,List), AxiomList),
length(AxiomList, AxiomCount),
(member(_:[],AxiomList) -> Flag = impossible ; Flag = possible).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Situations and Ballots
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Generate a situation as a list of 3's, 2's and 1's (at least one 3):
situation(N, Sit) :-
generate(N, [3,2,1], Sit),
once(member(3, Sit)).
% Generate a ballot as a list of 0's and 1's (at least one each):
ballot(N, Bal) :-
generate(N, [0,1], Bal),
once(member(0, Bal)),
once(member(1, Bal)).
% Generate a list of length N with elements taken from Elems:
generate(N, Elems, [X|List]) :-
N > 0, N1 is N - 1,
member(X, Elems),
generate(N1, Elems, List).
generate(0, _, []).
% Check whether the ballot suplied is sincere:
sincere([1|Bal]) :- !, sincere(Bal).
sincere(Bal) :- zeros(Bal).
% Check whether the ballot supplied is insincere:
insincere(Bal) :- \+ sincere(Bal).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Voting and sincere outcomes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Compute the outcome for a given situation and ballot:
vote(Sit, Bal, Out) :-
addlists(Sit, Bal, NewSit),
maxlist(NewSit, Max),
build_outcome(Max, NewSit, Out).
build_outcome(Max, [Max|Sit], [1|Out]) :- !,
build_outcome(Max, Sit, Out).
build_outcome(Max, [_|Sit], [0|Out]) :-
build_outcome(Max, Sit, Out).
build_outcome(_, [], []).
% For a given situation, generate the list of sincere outcomes:
sincere_outcomes(Sit, Outs) :-
length(Sit, N),
setof(Out, Bal^(ballot(N,Bal),sincere(Bal),vote(Sit,Bal,Out)), Outs).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Checking dominance
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Check whether A strictly dominates B for a given rule:
sdominates(Rule, A, B) :-
split(A, B, A1:A2:A3, B1:B2:B3),
zeros(A3), zeros(B1),
(member(1,A1) ; member(1,B3)),
rule(Rule, A2, B2).
% Check whether A weakly dominates B for a given rule:
wdominates(_, A, A) :- !.
wdominates(Rule, A, B) :-
split(A, B, _:A2:A3, B1:B2:_),
zeros(A3), zeros(B1),
(rule(Rule,A2,B2) ; (A2=B2, A2=[1])).
% Split two lists into three parts of matching lengths:
split(A, B, A1:A2:A3, B1:B2:B3) :-
append(A1, A2A3, A), length(A1, N1),
length(B1, N1), append(B1, B2B3, B),
append(A2, A3, A2A3), length(A2, N2),
length(B2, N2), append(B2, B3, B2B3).
% Condition on the "middle part" for the Kelly Principle:
rule(kel, [], []).
% Condition on the "middle part" for the Gardenfors Principle:
rule(gar, A, A).
% Condition on the "middle part" for the Sen-Puppe Principle:
rule(s_p, A, A) :- !.
rule(s_p, [X|A], [X|B]) :- rule(s_p, A, B).
rule(s_p, [1|A], [0|B]) :- flip(B, C), rule(s_p, A, C).
% Take a list of 0's and 1's and change the first 1 into a 0:
flip([0|A], [0|B]) :- flip(A, B).
flip([1|A], [0|A]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Undominated outcomes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% From list of coutcomes, extract those that are undominated:
undominated(Rule, Outs, TopOuts) :-
undominated(Rule, Outs, Outs, TopOuts).
undominated(_, [], _, []).
undominated(Rule, [A|Outs], AllOuts, TopOuts) :-
member(B, AllOuts),
sdominates(Rule, B, A), !,
undominated(Rule, Outs, AllOuts, TopOuts).
undominated(Rule, [A|Outs], AllOuts, [A|TopOuts]) :-
undominated(Rule, Outs, AllOuts, TopOuts).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Auxiliary predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Sum the elements of two lists (of equal length) to obtain a third:
addlists([X|Xs], [Y|Ys], [Z|Zs]) :- Z is X + Y, addlists(Xs, Ys, Zs).
addlists([], [], []).
% Compute the maximum of a given list of numbers:
maxlist([X,Y|List], Max) :- X > Y, !, maxlist([X|List], Max).
maxlist([_|List], Max) :- maxlist(List, Max).
maxlist([X], X).
% Check whether the list supplied is a (possibly empty) list of 0's:
zeros([0|A]) :- zeros(A).
zeros([]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%