%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 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([]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%