Question on a SAT encoding of the Stable Marriage problem

[neng...@gmail.com]

I have written a program in B-Prolog for the stable marriage benchmark used in the ASP competitions(see below). The program implements the encoding proposed in the paper "SAT Encodings of the Stable Marriage Problem with Ties and Incomplete Lists", in SAT 2002, by Ian P. Gent , Patrick Prosser , Barbara Smith , Toby Walsh. I was really excited about the compactness of the encoding. The encoding allows ties in preference lists and only uses O(n^2) clause-like constraints. Nevertheless, my implementation does not work.

For the following simple problem:

M1: 1 (3 2) 4
M2: 3 4 1 2
M3: 2 ( 4 3) 1
M4: 3 2 1 4

W1: 2 1 3 4
W2: 2 3 4 1
W3: 1 3 2 4
W4: 3 1 2 4

where people in parentheses are equally preferred. The matching (m1,w1), (m2,w3), (m3,w2), (m4,w4) is a strong stable matching, but it does not satisfy the channeling constraint 5(a)(b) given in the paper for i=1, j=1, p=1, q=2.

X1,1 = 1 & X1,2=0 -> Y1,2=1 & Y1,3=0

Is the proposed encoding of the paper too good to be true or I misunderstood something?

% marriage.pl (for B-Prolog): The Stable Marriage problem with ties
% https://www.mat.unical.it/aspcomp2013/StableMarriage
% by Neng-Fa Zhou, Feb. 9, 2013

/* This B-Prolog prorgam implements the SAT Encoding described in the paper:
"SAT Encodings of the Stable Marriage Problem with Ties and Incomplete Lists"
in SAT 2002, by Ian P. Gent , Patrick Prosser , Barbara Smith , Toby Walsh
*/

%% the main predicate is test/0 defined below.

solve(As):-
length(As,Len),
N is integer(sqrt(Len//2)), % N man and N woman
new_hashtable(MMap,N), new_hashtable(WMap,N),
new_array(WScoreMatrix,[N,N]),
new_array(MScoreMatrix,[N,N]),
fill_score_matrices(As,MMap,WMap,1,1,WScoreMatrix,MScoreMatrix),
%
writeln('MScoreMatrix'),
write_matrix(MScoreMatrix),
writeln('WScoreMatrix'),
write_matrix(WScoreMatrix),

new_array(MRankMatrix,[N,N]), % MRankMatrix[M,W]=p(P-,P,P+) where P is W's position in M's list,
new_array(MVarMatrix,[N]), % P- is the previous tied woman's position and P+ is the next ranked woman's position
foreach(M in 1..N, create_vars_fill_ranks(M,N,MVarMatrix,MRankMatrix,MScoreMatrix)),
%
new_array(WRankMatrix,[N,N]), % WRankMatrix[W,M]= p(Q-,Q,Q+)
new_array(WVarMatrix,[N]),
foreach(W in 1..N, create_vars_fill_ranks(W,N,WVarMatrix,WRankMatrix,WScoreMatrix)),

writeln('MRankMatrix'),
write_matrix(MRankMatrix),
writeln('WRankMatrix'),
write_matrix(WRankMatrix),
%
foreach(M in 1..N, mono_constraint(M,N,MVarMatrix)),
foreach(W in 1..N, mono_constraint(W,N,WVarMatrix)),
foreach(M in 1..N, W in 1..N, channel_and_strongstable_constraints(M,W,MVarMatrix,WVarMatrix,MRankMatrix,WRankMatrix)),
%
term_variables((MVarMatrix,WVarMatrix),Vars),
Vars :: 0..1,
cp_solve(Vars),
writeln(MVarMatrix),
writeln(WVarMatrix),
fail.

write_matrix(Matrix):-
foreach(I in 1..Matrix^length, J in 1..Matrix[1]^length, [Cij],
(Cij @= Matrix[I,J], write(' '), write(Cij), write(' '),
(J =:= Matrix[1]^length->nl;true))).

%%%
fill_score_matrices([],_,_,_,_,_,_) => true.
fill_score_matrices([manAssignsScore(M,W,Score)|As],MMap,WMap,MNo,WNo,WScoreMatrix,MScoreMatrix) =>
get_num(M,MMap,MNo,MNo1,ThisMNo),
get_num(W,WMap,WNo,WNo1,ThisWNo),
MScoreMatrix[ThisMNo,ThisWNo] @= Score,
fill_score_matrices(As,MMap,WMap,MNo1,WNo1,WScoreMatrix,MScoreMatrix).
fill_score_matrices([womanAssignsScore(W,M,Score)|As],MMap,WMap,MNo,WNo,WScoreMatrix,MScoreMatrix) =>
get_num(W,WMap,WNo,WNo1,ThisWNo),
get_num(M,MMap,MNo,MNo1,ThisMNo),
WScoreMatrix[ThisWNo,ThisMNo] @= Score,
fill_score_matrices(As,MMap,WMap,MNo1,WNo1,WScoreMatrix,MScoreMatrix).

get_num(Person,Map,No,No1,ThisNo),
hashtable_get(Map,Person,ThisNo)
=>
No1=No.
get_num(Person,Map,No,No1,ThisNo) =>
hashtable_put(Map,Person,No),
ThisNo=No,No1 is No+1.

%%%
% MVarVect[M,P]=1 iff man M is matched to a woman in P^th or later position in his preference list
% WVarVect[W,P]=1 iff man W is matched to a man in P^th or later position in her preference list
%%%
create_vars_fill_ranks(M,N,VarMatrix,RankMatrix,ScoreMatrix):-
Scores @= [(Pref,W) : W in 1..N, [Pref], Pref @= ScoreMatrix[M,W]],
sort('>=',Scores,SortedScores),
create_vars_fill_ranks_aux(M,SortedScores,RankMatrix,Vars),
VarVect=..[v|Vars],
VarMatrix[M] @= VarVect.

create_vars_fill_ranks_aux(M,[(Score,W)|Scores],RankMatrix,Vars):-
Vars=[_|VarsR],
RankMatrix[M,W] @= p(1,1,NextPos),
create_vars_fill_ranks_aux(M,Score,1,2,NextPos,Scores,RankMatrix,VarsR).

% the previous person's position is PrevPos and the preference is PrevScore in person I's list
create_vars_fill_ranks_aux(_M,_PrevScore,_PrevPos,Pos,NextPos,[],_RankMatrix,Vars):-Vars=[0],NextPos=Pos. % a dummy 0
create_vars_fill_ranks_aux(M,PrevScore,PrevPos,Pos,NextPos,[(Score,W)|Scores],RankMatrix,Vars):-
Score==PrevScore,!,
Vars=[_|VarsR],
RankMatrix[M,W] @= p(PrevPos, Pos,NextPos),
Pos1 is Pos+1,
create_vars_fill_ranks_aux(M,PrevScore,Pos,Pos1,NextPos,Scores,RankMatrix,VarsR).
create_vars_fill_ranks_aux(M,_PrevScore,_PrevPos,Pos,NextPos,[(Score,W)|Scores],RankMatrix,Vars):-
Vars=[_|VarsR],
NextPos=Pos, % for each person in the previous group prefered evenly by M, if Q be the person's position in M's list, Q+ = Pos
RankMatrix[M,W] @= p(Pos,Pos,NextPos1), % Pos is the first position in the next group, so Pos- = Pos
Pos1 is Pos+1,
create_vars_fill_ranks_aux(M,Score,Pos,Pos1,NextPos1,Scores,RankMatrix,VarsR).

%%%
mono_constraint(M,N,MVarMatrix):-
MVarVect @= MVarMatrix[M],
MVarVect[1] @= 1,
foreach(P in 2..N, % notice that there is a dummy 0 at index N+1
(MVarVect[P]$=0 $=> MVarVect[P+1]$=0)).

channel_and_strongstable_constraints(M,W,MVarMatrix,WVarMatrix,MRankMatrix,WRankMatrix):-
MRankMatrix[M,W] @= p(PrevP,P,_),
WRankMatrix[W,M] @= p(_,Q,NextQ),
write(mw(M,W)),writeln(pq(P,Q)),
% Channelling constraints
MVarMatrix[M,P]$=1 $/\ MVarMatrix[M,P+1]$=0 $=> WVarMatrix[W,Q]$=1, % 5(a)
MVarMatrix[M,P]$=1 $/\ MVarMatrix[M,P+1]$=0 $=> WVarMatrix[W,Q+1]$=0, % 5(b)
WVarMatrix[W,Q]$=1 $/\ WVarMatrix[W,Q+1]$=0 $=> MVarMatrix[M,P]$=1, % 6(a)
WVarMatrix[W,Q]$=1 $/\ WVarMatrix[W,Q+1]$=0 $=> MVarMatrix[M,P+1]$=0, % 6(b)
% Strong stability constraint
MVarMatrix[M,PrevP]$=1 $=> WVarMatrix[W,NextQ]$=0. % 7st

test:-
solve([manAssignsScore(m_1,w_1,4), manAssignsScore(m_1,w_2,2), manAssignsScore(m_1,w_3,2), manAssignsScore(m_1,w_4,1),
manAssignsScore(m_2,w_1,2), manAssignsScore(m_2,w_2,1), manAssignsScore(m_2,w_3,4), manAssignsScore(m_2,w_4,3),
manAssignsScore(m_3,w_1,1), manAssignsScore(m_3,w_2,3), manAssignsScore(m_3,w_3,2), manAssignsScore(m_3,w_4,2),
manAssignsScore(m_4,w_1,2), manAssignsScore(m_4,w_2,3), manAssignsScore(m_4,w_3,4), manAssignsScore(m_4,w_4,1),

womanAssignsScore(w_1,m_1,3), womanAssignsScore(w_1,m_2,4), womanAssignsScore(w_1,m_3,2), womanAssignsScore(w_1,m_4,1),
womanAssignsScore(w_2,m_1,1), womanAssignsScore(w_2,m_2,4), womanAssignsScore(w_2,m_3,3), womanAssignsScore(w_2,m_4,2),
womanAssignsScore(w_3,m_1,4), womanAssignsScore(w_3,m_2,2), womanAssignsScore(w_3,m_3,3), womanAssignsScore(w_3,m_4,1),
womanAssignsScore(w_4,m_1,3), womanAssignsScore(w_4,m_2,2), womanAssignsScore(w_4,m_3,4), womanAssignsScore(w_4,m_4,1)]).

test1 :-
solve([manAssignsScore(m_1,w_1,1), manAssignsScore(m_1,w_2,2),
manAssignsScore(m_2,w_1,1), manAssignsScore(m_2,w_2,2),

womanAssignsScore(w_1,m_1,2), womanAssignsScore(w_1,m_2,1),
womanAssignsScore(w_2,m_1,1), womanAssignsScore(w_2,m_2,1)]).

[ianphi...@googlemail.com]

Hi, Ian Gent here. Sorry for the delay replying (you did mail me privately and replying was on my to do list, but I had not got round to it.)

The example you have seems correct but I don't see why you say it does not have the channelling constraint.

In your example, man 1 marries woman 2, and woman 2 marries man 1 of course. Woman 1 is first choice for man 1, while man 1 is second choice for woman 2.

The definition of the x and y variables is that x_1i is true iff man 1 gets his i'th choice or worse, and y_1j is true iff woman 1 gets her jth choice or worse.

In your example therefore we should have:

x11 = True
x12 = False (because he gets his first choice)

y11 = True
y12 = True
y13 = False (because she gets her second choice.)

Therefore the channelling constraint you give is:

x11 = T & x12 = F -> y12 = T & y13 = F

and the values above satisfies this constraint.

So I can't see a problem with the constraint, so I don't know why you say it doesn't satisfy it.

I don't know if htis helps at all but now I have refreshed myself on this problem (it is more than 10 years ago!) I should be able to answer other questions more quickly.


A small point but the paper is actually by Gent and Prosser, not Gent Prosser Smith & Walsh. (We did thank Smith and Walsh in the acknowledgements!)

Best wishes

Ian