制約論理とは、従来の述語論理の枠組みに制約と言う知識表現とその解消(充足)による問題解決の考え方を導入したものです。
このパラダイムを実現するために、AZ-Prologのユニフィケーションの仕組みを拡張しました。具体的には、変数が束縛(値を持つこと)された時に初めてゴールが起動される仕組み(遅延実行機構)や、束縛された際に変数が取り得る値領域(領域制約)に対するチェックがなされ結果がユニフィケーションの真偽に反映される仕組み等です。遅延実行ゴールや変数の値領域の設定には freeze/2 、 put_clp_area/2 等の組込述語が提供されています。その上にPrologによる制約解消系の構築を行いました。
制約解消系は未完成です。順次充実を図っていきますのでご協力ください。
処理系の制約論理拡張は 『制約論理プログラミング (知識情報処理シリーズ 別巻2)共立出版(株)』を参考にしました。
変数が値を持った時に起動される遅延実行ゴールを設定します。
詳細は述語リファレンスをご参照ください。
ある変数が値を持った時に実行されるゴールは、同一変数に対して順次 freeze/2 で追加することができますが、遅延実行時においては決定性、すなわちゴール(列)の最後にカットオペレータがついたものになります。
デバッグモードで起動し、ある変数が値をもったときtraceを開始させるspyの変形(下記の例)のように、制約解消系以外の用途でも使うことができます。
<例>
| ?-debug. || ?-freeze(X,trace),go(X). % go(X) の実行の経過で、X が値を持ったときにtrace が開始される
変数(第1引数に指定)に設定さている遅延実行ゴールを第2引数とユニファイします。遅延実行機構はこの述語により遅延実行ゴールを取得します。また設定内容の確認にも用いることができます。
詳細は述語リファレンスをご参照ください。
変数に値領域(領域制約)を設定します。既に値領域が設定されている場合はANDで追加されます。設定できる値は任意の項です。
第二引数はソートされていることが前提となる述語で、拡張ライブラリ組込述語「in /xfx」の下層述語(AZ-Prolog本体側に組み込まれた述語の意。単に領域制約を設定するだけで、ソートは上層側の責任において行う)となります。
<例>
| ?-put_clp_area(X,[1,2,5..7]),get_clp_area(X,L). X = X, L = [1,2,5..7] yes | ?-put_clp_area(X,[a,b,d,1,2,5..7]),put_clp_area(X,[b,2..6]),get_clp_area(X,L). X = X, L = [b,2,5,6] yes
既に値領域が設定されている変数から指定領域を取り除きます。
拡張ライブラリ組込述語「notin /xfx」の下層述語です。
<例>
| ?-put_clp_area(X,[1..9]),rm_clp_area(X,4..7),get_clp_area(X,L).
X = X,
L = [1..3,8,9]
yes
変数に値領域が設定されている場合、その設定領域を取得します。呼び出し時点で既に変数の値が決定している(既に変数ではない)場合は失敗します。
拡張ライブラリ組込述語「indomain/1」などの下層述語です。
<例>
| ?-X in 0..9,get_clp_area(X,L). X = X, L = [0..9] yes
「put_clp_area/2」の補助述語(汎用)で、2集合の共通部分を取得します。
<例>
| ?-clp_intersection([1,3..6,9..12],[2..11],L). L = [3..6,9..11] yes
「put_clp_area/2」「in /xfx」の補助述語で第一引数が第二引数のリストに含まれる場合成功します。
<例>
| ?- clp_is_member(a,[1..9,b,c(z)]). no | ?- clp_is_member(a,[1..9,a,c(z)]). yes | ?- clp_is_member(7,[1..9,a,c(z)]). yes
処理系で扱う整数の下限と上限を取得します。
<例>
| ?- system_get_min_max_int(MinInt,MaxInt). MinInt = -9223372036854775808, MaxInt = 9223372036854775807 yes
?- dlib_require(clp).system/ext/clp/clp.plにprologソースで提供していますので、コンサルトでも使うことができ、ユーザーが手を加えることも可能です。ソースには下記以外にも定義述語がありますのでご参照ください。
変数が取り得る値領域の制約(値のリスト)を与えます。
詳細は述語リファレンスをご参照ください。
変数が取り得ない値領域(値のリスト)の制約を与えます。
詳細は述語リファレンスをご参照ください。
引数リストに含まれる変数はすべて異なる値を持つという制約を与えます。
詳細は述語リファレンスをご参照ください。
制約変数の取りうる値を非決定的にユニファイします。
詳細は述語リファレンスをご参照ください。
与えられた制約に基づいて探索を行います。
詳細は述語リファレンスをご参照ください。
演算子の左右の数(式)の計算結果が等しいという制約を与えます。
演算子の左右の数(式)の計算結果が等しくないという制約を与えます。
演算子の右の数(式)の計算結果が左の数(式)の計算結果より大きいという制約を与えます。
演算子の左の数(式)の計算結果が右の数(式)の計算結果より大きいという制約を与えます。
演算子の右の数(式)の計算結果が左の数(式)の計算結果より大きいか等しいという制約を与えます。
演算子の左の数(式)の計算結果が右の数(式)の計算結果より大きいか等しいという制約を与えます。
[ _, 1, _, _, _, _, 2, _, 3, _, _, _, _, _, _, 4]なお、「sample/clp/sudoku.pl」には、通常の9x9は勿論、NxNマス(Nは正の整数の平方根を持つ数字)の解法に一般化した例題がありますので、合わせてご確認ください。
:- dlib_require(clp). % 拡張ライブラリをロードします go:- % 4x4の変数領域を作ります。マス目を左上から順に異なる変数で埋めます Vars = [X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11,X12, X13,X14, X15,X16], % ヒントとユニフィケーションして確定値を埋めます X2=1,X7=2,X9=3,X16=4, % 各変数は1から4までの数値が入るという制約を与えます Vars in 1..4 , % 各行に含まれる変数はすべて異なる値を持つという制約を与えます alldifferent([X1, X2, X3, X4]), alldifferent([X5, X6, X7, X8]), alldifferent([X9, X10, X11,X12]), alldifferent([X13,X14, X15,X16]), % 各列に含まれる変数はすべて異なる値を持つという制約を与えます alldifferent([X1,X5,X9,X13]), alldifferent([X2,X6,X10,X14]), alldifferent([X3,X7,X11,X15]), alldifferent([X4,X8,X12,X16]), % 各ブロックに含まれる変数はすべて異なる値を持つという制約を与えます alldifferent([X1,X2,X5,X6]), alldifferent([X3,X4,X7,X8]), alldifferent([X9,X10,X13,X14]), alldifferent([X11,X12,X15,X16]), % 以上の制約で探索を行います labeling(Vars), % 結果を表示します。 write([[X1,X2], [X3,X4]]),nl, write([[X5,X6], [X7,X8]]),nl,nl, write([[X9,X10], [X11,X12]]),nl, write([[X13,X14],[X15,X16]]),nl. | ?- go. [2,1] [4,3] [4,3] [2,1] [3,4] [1,2] [1,2] [3,4] yes
※「数独(スウドク)」はニコリの登録商標(第3327502号など)で、日本では「ナンバープレース」と呼ばれることも多い。日本以外の国ではSudokuという呼称が一般的。
魔方陣とは正方形に並んだマスに、各列(縦)/各行(横)/両対角線のいずれの合計も同じになるように数字が並んだものを言います。
ここでは3X3魔方陣の解法を説明します。
使われる制約組込述語は「in /xfx」「alldifferent/1」「labeling/1」「#= /xfx」の4述語です。
なお、「sample/clp/magic.pl」では、NxNマスの魔方陣が解けるようになっています。
比較のため、このファイルには通常のPrologコードの生成検査法によるプログラムも収められています。
生成検査法では、4X4魔方陣においては16の階乗=20兆とおりの組み合わせを試すことになり、最初の解を得るのでさえ相当の時間を要しますが、制約論理プログラミングでは、数分のうちに全解を求めることができます。
ただし、N=6以上では第一解でさえ相当の時間を要します。
:- dlib_require(clp). % 拡張ライブラリをロードします go:- Vars = [X1,X2,X3, % 変数領域を設定します X4,X5,X6, X7,X8,X9], Vars in 1..9, % 各変数は1から9までの数値が入るという制約を与えます alldifferent(Vars), % 各変数はすべて異なる値をとるという制約を与えます 15 #= X1+X2+X3, % 第1行のマスの合計値が15になるという制約を与えます 15 #= X4+X5+X6, % 第2行のマスの合計値が15になるという制約を与えます 15 #= X7+X8+X9, % 第3行のマスの合計値が15になるという制約を与えます 15 #= X1+X4+X7, % 第1列のマスの合計値が15になるという制約を与えます 15 #= X2+X5+X8, % 第2列のマスの合計値が15になるという制約を与えます 15 #= X3+X6+X9, % 第3列のマスの合計値が15になるという制約を与えます 15 #= X1+X5+X9, % 左上右下対角線のマスの合計値が15になるという制約を与えます 15 #= X3+X5+X7, % 右上左下対角線のマスの合計値が15になるという制約を与えます labeling(Vars), % 以上の制約で探索を行います write([X1,X2,X3]),nl, % 結果を表示します。 write([X4,X5,X6]),nl, write([X7,X8,X9]),nl. | ?-go. [2,7,6] [9,5,1] [4,3,8] yes
:- dlib_require(clp). % 拡張ライブラリをロードします go:- Vars = [S,E,N,D,M,O,R,Y], % 変数領域を設定します Vars in 0..9, % 各変数は0から9までの数値が入るという制約を与えます alldifferent(Vars), % 各変数はすべて異なる値をとるという制約を与えます S #¥= 0, % S は0ではないという制約を与えます M #¥= 0, % M は0ではないという制約を与えます S*1000+E*100+N*10+D % SEND+MORE=MONEY であるという制約を与えます +M*1000+O*100+R*10+E #= M*10000+O*1000+N*100+E*10+Y, labeling(Vars), % 以上の制約で探索を行います write(Vars),nl. % 結果を表示します。 | ?-go. [9,5,6,7,1,0,8,2] yes
|?-listing. turukame(Turu,Kame,Foot,Head) :- Turu in 0..Head, Kame in 0..Head, Foot#=Turu*2+Kame*4, Head#=Turu+Kame. yes |?-trace. yes ||?-turukame(X,Y,14,5). [1] 0 Try : turukame(X_7,Y_9,14,5) ? Match : turukame(X_7,Y_9,14,5) :- X_7 in 0..5, Y_9 in 0..5, 14#=X_7*2+Y_9*4, 5#=X_7+Y_9. [2] 1 Try : X_7 in 0..5 ? i % Iコマンド Foot = 14 % 定義節の変数:Foot は 14に束縛されています Head = 5 % 定義節の変数:Head は 5に束縛されています [2] 1 Try : X_7 in 0..5 ? << BUILTIN CALL >> [2] 1 Succ : _30 in 0..5 [2] 1 Try : Y_9 in 0..5 ? i % Iコマンド Turu = _30 { [0..5]::true } % 定義節の変数:Turu は 0..5 に制約されています Foot = 14 Head = 5 [2] 1 Try : Y_9 in 0..5 ? << BUILTIN CALL >> [2] 1 Succ : _46 in 0..5 [2] 1 Try : 14#=_30*2+_46*4 ? i % Iコマンド Turu = _30 { [0..5]::true } Kame = _46 { [0..5]::true } Foot = 14 Head = 5 [2] 1 Try : 14#=_30*2+_46*4 ? << BUILTIN CALL >> [2] 1 Succ : 14#=_30*2+_46*4 [2] 1 Try : 5#=_30+_46 ? i <== Iコマンド Turu = _30 { [1,3,5]::$clp_area_propagation(7,[1,2],[_30,_46]),! } % 制約が狭まりました Kame = _46 { [1..3]::$clp_area_propagation(7,[1,2],[_30,_46]),! } % 制約が狭まりました Foot = 14 Head = 5 [2] 1 Try : 5#=_30+_46 ? <> [2] 1 Succ : 5#=3+2 % この制約で値が求まりました << LAST CALL >> [1] 0 Succ : turukame(3,2,14,5) X = 3, Y = 2 yes