ゼブラパズル(Zebra Puzzle)を制約論理プログラミングで解く

以下のパズル（ゼブラパズルというらしい）を制約論理プログラミングで解いてみた。

問題：
1.家が３軒あります。その３軒の家はそれぞれ赤・青・緑で塗られています。そしてその住人は、それぞれ異なる国籍で、それぞれ異なるペットを買っています。
2.イギリス人は赤い家に住んでいます。
3.スペイン人は犬を飼っています。
4.日本人は、猫を飼っている人の右側に住んでいます。
5.猫を飼っている人は青色の家の左に住んでいます。

誰がシマウマを飼っているでしょうか？

プログラム

:-use_module(library(clpfd)).

zebra_prob:-

% left  ------> right
House=[Color1,Color2,Color3],
Pet=[Pet1,Pet2,Pet3],
Race=[Race1,Race2,Race3],

% Race  1:Japanese 2:English 3:Spanish
% Color 1:Red 2:Blue 3:Green
% Pet   1:Cat 2:Dog 3:Zebra

all_different(House), %それぞれ異なる色の家
all_different(Pet),   %それぞれ異なるペット
all_different(Race),  %それぞれ異なる国籍

House ins 1..3,
Pet ins 1..3,
Race ins 1..3,

%イギリス人(2)は赤い家(1)
Color1 #= 1 #<==> Race1 #= 2,
Color2 #= 1 #<==> Race2 #= 2,
Color3 #= 1 #<==> Race3 #= 2,

%スペイン人(3)は犬(2)を飼っている
Race1 #= 3 #<==> Pet1 #= 2,
Race2 #= 3 #<==> Pet2 #= 2,
Race3 #= 3 #<==> Pet3 #= 2,

%日本人(1)は、猫(1)を飼っている人の右側
Pet1 #= 1 #<==> Race2 #= 1,
Pet2 #= 1 #<==> Race3 #= 1,
Race1 #\= 1, %日本人は一番左ではない

%猫(1)を飼っている人は青色の家(2)の左に住んでいます。
Pet1 #= 1 #<==> Color2 #= 2,
Pet2 #= 1 #<==> Color3 #= 2,
Pet3 #\= 1, %猫は一番右ではない

label(House),
label(Pet),
label(Race),
write('house:'),write(House),nl,
write('pet:'),write(Pet),nl,
write('race:'),write(Race). 

実行結果

1 ?- zebra_prob.
house:[1,2,3]
pet:[1,3,2]
race:[2,1,3]
true ;
house:[3,1,2]
pet:[2,1,3]
race:[3,2,1]
true.

解説
Race 1:Japanese 2:English 3:Spanish
Color 1:Red 2:Blue 3:Green
Pet 1:Cat 2:Dog 3:Zebra
PetがZebra(3)と同じ要素番号のRaceは必ず1(日本人)
よってシマウマは日本人が飼っている。
家、ペット、国籍 の並びの組み合わせは上記2パターンある。

※　「～の右に」という文章を「１軒右」と解釈しています。
　　（２軒右も含むというコードに変更するのも簡単です）