% Additional rules for House Allocation problem.
% Tuples of form pref(Agent,House,Rank) is the input.

% Generated matching
{ match(X,Y) : pref(X,Y,_) }.

% An agent cannot be matched to two houses.
:- match(X,_), 2 { match(X,_) }.
% A house cannot be matched to two agents.
:- match(_,Y), 2 { match(_,Y) }.

% Only one triple with a rank for an agent.
:- pref(Agent,_,Rank), 2 { pref(Agent,_,Rank) }.
% Ranks (for an agent) must be contiguous starting from 1.
:- pref(Agent,_,Rank), Rank>1, not pref(Agent,_,Rank-1).

% Pareto optimal?
% Can't have an unmatched agent and an unmatched house
% if acceptable to the agent.
:- pref(Agent,House,_), not match(Agent,_), not match(_,House).

% Can't have a matched agent and an unmatched house where
% agent prefers the unmatched house.
:- match(Agent,House1), not match(_,House2),
   pref(Agent,House1,Rank1), pref(Agent,House2,Rank2), Rank2<Rank1.

% Can't have a cyclic coalition
path(Agent1,Agent2) :- match(Agent1,House1), match(Agent2,House2),
  pref(Agent1,House1,Rank1), pref(Agent1,House2,Rank2), Rank2<Rank1.

path(Agent1,Agent2) :- path(Agent1,Agent3), path(Agent3,Agent2).

:- pref(Agent1,_,_), path(Agent1,Agent1).

#maximize { 1,X,Y : match(X,Y) }.

#show match/2.