ネットで以下の問題を見つけたのでSWI-PrologのCLPFDライブラリで解いてみた
問題：水泳大会
水泳大会で、この４人が１位から４位を獲得しました（同順位はありません）。
スタート前の予想は下のとおりで、３人が当たり、１人が外れました。
誰が何位だったのでしょう？
ことり「私は１位」
なる 「私はすずより上位」
すず 「私は１位か２位」
あゆ 「私は１位か２位」
プログラム:
:-use_module(library(clpfd)).
solve_girl_order:-
GirlOrderLst = [KotoriOrder,NaruOrder,SuzuOrder,AyuOrder],
GirlOrderLst ins 1..4,
all_different(GirlOrderLst),
HatugenFlgLst = [KotoriHatugenFlg,NaruHatugenFlg,SuzuHatugenFlg,AyuHatugenFlg],
HatugenFlgLst ins 0..1,
appear_times(HatugenFlgLst,0,1),
KotoriHatugenFlg #<==> (KotoriOrder #= 1),
NaruHatugenFlg #<==> (NaruOrder #< SuzuOrder),
SuzuHatugenFlg #<==> (SuzuOrder #= 1 #\/ SuzuOrder #= 2),
AyuHatugenFlg #<==> (AyuOrder #= 1 #\/ AyuOrder #= 2),
label(GirlOrderLst),
label(HatugenFlgLst),
write(GirlOrderLst),
write(HatugenFlgLst).
% appear_times( Lst, Num, Times)
% [Num] appears [Times] times in [Lst]
appear_times(Lst,Num,Times):-
maplist(eq_b(Num),Lst,Bs),
sum(Bs,#=,Times).
eq_b(X,Y,B):-(X#=Y) #<==>B.
実行結果:
[1] 4 ?- girl_order.
[1,3,4,2][1,1,0,1]
true ;
false.
実行結果は
[ことり順位,なる順位,すず順位,あゆ順位]
[ことり発言,なる発言,すず発言,あゆ発言 (1:真実 0:嘘)]
プログラム作成に10分くらいかかった。
実行時間は瞬時ですか？
「３人が当たり、１人が外れました。」とありますが、
この制約はプログラムではどの部分で表現されていますか？
>>sugaさん
実行時間は瞬時で、今回は解が１つのみでしたが他に可能性のある順位の組み合わせも全部取得できます。
リスト HatugenFlgLst の各要素に各発言者の発言の真偽が入るのですが、
HatugenFlgLst ins 0..1 という文が「それぞれの要素が0(偽)または1(真)のみ」という制約で、
appear_times(HatugenFlgLst,0,1), という文が「HatugenFlgLstの中には0が1回出現する」という制約を表しています(残りの3つが1というのは変数が0か1しか取らないという制約があるので記載する必要が無い）
下のほうでappear_times述語を定義しているのですが、この説明は少し難しく、
まず中で使われている eq_b(X,Y,B)という述語の説明をすると、これはXとYとBの関係を表す制約なのですが、
eq_b(X,Y,B):-(X#=Y) #< ==>B という文で「 X=Y と B=1 という条件が互いに必要十分条件を満たす」という制約を表します(Bが1:True 0:False)
具体的には、以下の制約が満たされます
「X=Yであれば必ずB=1」
「B=1であれば必ずX=Y」
「X!=Yであれば必ずB=0」
「B=0であれば必ずX!=Y」
そして appear_times述語の説明ですが、
maplist というのは prolog でよく使われる述語でだいたい以下のような役割をしています
「述語にリストの各要素を引数として渡し、その結果を新しいリストに出力する」
appear_times(Lst,Num,Times):-
maplist(eq_b(Num),Lst,Bs),
上記の記述の場合は、eq_b の3つの引き数のうち、
「はじめの引き数にはNum固定、2番目にはLstの各要素を渡し、eq_bをLstの要素数回呼ぶ。Bsには各eq_b呼出し毎の戻り値がリストになって返ってくる」ことを意味しています。
(実際はPrologは引き数と戻り値の概念がなくもっと入出力双方向性があるのですが今回はこの解釈でよいです)
この時点でBsには各発言者の「発言が正しければ1、間違っていれば0」という制約がついた変数のリストが存在することになります。
そして
sum(Bs,#=,Times) で 「Bsの和がTimesと同じ(今回は1)」という制約を記述しています。
説明するときにPrologの文法か CLPFDライブラリの文法かを明確に分けなくてはいけないのですが、以下となります。
Prologの組み込み述語 … write,maplist
CLPFDライブラリの述語 … ins A..B , #< ==>, #=, label, sum, #<, #\/, all_different