制約論理プログラミング

制約論理プログラミングは制約プログラミングの一種で、論理プログラミングが制約充足の概念を含むように拡張されています。制約論理プログラムは、節の本体に制約を含む論理プログラムです。制約を含む節の例は です。この節では、 は制約であり、、 、 は通常の論理プログラミングと同様にリテラルです。この節は、ステートメントが成り立つ 1 つの条件を述べています。は 0 より大きく、 と の両方がtrue です。 A(X,Y) :- X+Y>0, B(X), C(Y)X+Y>0A(X,Y)B(X)C(Y)A(X,Y)X+YB(X)C(Y)

通常の論理プログラミングと同様に、プログラムは目標の証明可能性について照会されます。目標自体には、リテラルに加えて制約が含まれる場合があります。目標の証明は、充足可能な制約と、他の節を使用して証明できるリテラルである節で構成されます。実行はインタープリタによって行われ、インタープリタは目標から開始して節を再帰的にスキャンし、目標を証明しようとします。このスキャン中に遭遇した制約は、制約ストアと呼ばれるセットに配置されます。このセットが充足不可能であることが判明した場合、インタープリタはバックトラックし、他の節を使用して目標を証明しようとします。実際には、制約ストアの充足可能性は不完全なアルゴリズムを使用してチェックされる場合がありますが、このアルゴリズムでは必ずしも矛盾が検出されるわけではありません。

形式的には、制約論理プログラムは通常の論理プログラムと似ていますが、節の本体には、通常の論理プログラミングリテラルに加えて、制約を含めることができます。例として、X>0は制約であり、次の制約論理プログラムの最後の節に含まれています。

B ( X , 1 ) :-  X < 0。B ( 
X , Y ) :- X = 1 、Y > 0。A ( X , Y ):- X > 0 、B ( X 、Y )。  
  

通常の論理プログラミングと同様に、 などの目標を評価するには、A(X,1)最後の節の本体を で評価する必要がありますY=1。 通常の論理プログラミングと同様に、これには目標 を証明する必要がありますB(X,1)。 通常の論理プログラミングとは対照的に、これには制約 も満たされる必要があります。つまり、最後の節の本体の制約です。 (通常の論理プログラミングでは、X が完全に基底項X>0にバインドされていない限り、X>0 は証明できず、そうでない場合はプログラムの実行が失敗します。)

制約が満たされているかどうかは、制約に遭遇したときに必ずしも判断できるわけではありません。たとえば、この場合、 の値はX最後の節が評価されるときに決定されません。結果として、X>0この時点では制約は満たされることも違反されることもありません。 の評価に進みB(X,1)、その後 の結果の値がX正であるかどうかを確認するのではなく、インタープリタは制約を保存してX>0から の評価に進みます。このようにして、インタープリタはの評価中にB(X,1)制約違反を検出し、違反している場合は の評価が完了するのを待たずにすぐにバックトラックすることができます。 X>0B(X,1)B(X,1)

一般に、制約論理プログラムの評価は、通常の論理プログラムと同様に進行します。ただし、評価中に遭遇する制約は、制約ストアと呼ばれるセットに配置されます。たとえば、目標の評価は、A(X,1)最初の節の本体を で評価することによって進行しますY=1。この評価はX>0制約ストアに追加され、目標B(X,1)が証明されることを要求します。この目標を証明しようとしている間、最初の節が適用されますが、その評価はX<0制約ストアに追加されます。この追加により、制約ストアは満たされなくなります。次に、インタープリタはバックトラックし、制約ストアから最後の追加を削除します。2 番目の節の評価では、X=1と がY>0制約ストアに追加されます。制約ストアは満たされ、証明する他のリテラルは残っていないため、インタープリタはソリューション で停止しますX=1, Y=1。

制約ロジック プログラムのセマンティクスは、実行中にペアを維持する仮想インタープリターの観点から定義できます。このペアの最初の要素は現在の目標と呼ばれ、2 番目の要素は制約ストアと呼ばれます。現在の目標には、インタープリターが証明しようとしているリテラルが含まれ、満たそうとしている制約も含まれる場合があります。制約ストアには、インタープリターがこれまでに満たせると想定したすべての制約が含まれます。 ${\displaystyle \langle G,S\rangle }$

最初は、現在の目標が目標であり、制約ストアは空です。インタープリタは、現在の目標から最初の要素を削除して分析することで処理を進めます。この分析の詳細は以下で説明しますが、最終的にこの分析によって正常終了または失敗が発生する可能性があります。この分析には、再帰呼び出しと、現在の目標への新しいリテラルの追加、および制約ストアへの新しい制約の追加が含まれる場合があります。失敗が発生した場合、インタープリタはバックトラックします。現在の目標が空で、制約ストアが満たされている場合、正常終了が生成されます。

ゴールから削除されたリテラルの分析の詳細は次のとおりです。このリテラルをゴールの先頭から削除した後、それが制約であるかリテラルであるかがチェックされます。制約である場合は、制約ストアに追加されます。リテラルである場合、ヘッドがリテラルと同じ述語を持つ節が選択されます。節は、その変数を新しい変数 (ゴールに出現しない変数) に置き換えることによって書き換えられます。結果は節の新しいバリアントと呼ばれます。節の新しいバリアントの本体は、次にゴールの先頭に配置されます。リテラルの各引数と新しいバリアント ヘッドの対応する引数の等価性も、ゴールの先頭に配置されます。

これらの操作中にいくつかのチェックが行われます。特に、制約ストアは、新しい制約が追加されるたびに一貫性がチェックされます。原則として、制約ストアが満たされない場合、アルゴリズムはバックトラックできます。ただし、各ステップで満たされないかどうかをチェックするのは非効率的です。このため、代わりに不完全な満足可能性チェッカーを使用できます。実際には、満足可能性は制約ストアを単純化するメソッドを使用してチェックされます。つまり、制約ストアを同等だが解決しやすい形式に書き換えます。これらのメソッドは、満たされない制約ストアの満たされない可能性を証明できる場合もありますが、常に証明できるとは限りません。

現在の目標が空で、制約ストアが満たされないことが検出されない場合、インタープリタは目標を証明しています。実行の結果は、現在の (簡略化された) 制約のセットです。このセットには、変数を特定の値に強制する制約などが含まれる場合がありますが、特定の値を与えずに変数のみをバインドする 制約も含まれる場合があります。${\displaystyle X=2}$${\displaystyle X>2}$

正式には、制約論理プログラミングのセマンティクスは導出によって定義されます。遷移 は、 と記されるゴール/ストアのペアのことです。このようなペアは、状態 から状態 に移行する可能性を示します。このような遷移は、次の 3 つの場合に可能です。 ${\displaystyle \langle G,S\rangle \rightarrow \langle G',S'\rangle }$${\displaystyle \langle G,S\rangle }$${\displaystyle \langle G',S'\rangle }$

• Gの要素は制約Cであり、およびである。言い換えれば、制約はゴールから制約ストアに移動できる。${\displaystyle G'=G\backslash \{C\}}$${\displaystyle S'=S\cup \{C\}}$
• Gの要素がリテラル である場合、新しい変数を使用して書き直すと となる節が存在し、集合はがに置き換えられ、となる。言い換えれば、リテラルは、同じ述語をヘッドに持つ節の新しい変種の本体に置き換えることができ、新しい変種の本体と上記の項の等式を目標に追加します。${\displaystyle L(t_{1},\ldots,t_{n})}$${\displaystyle L(t_{1}',\ldots ,t_{n}')\mathrel {{:}{-}} B}$${\displaystyle G'}$${\displaystyle L(t_{1},\ldots,t_{n})}$${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B}$${\displaystyle S'=S}$
• SとSは特定の制約セマンティクスに従って同等である。${\displaystyle S'}$

遷移のシーケンスは導出です。ゴールG は、何らかの充足可能な制約ストアSについてからへの導出が存在する場合に証明できます。このセマンティクスは、処理するゴールのリテラルとリテラルを置き換える節を任意に選択するインタープリタの可能な進化を形式化します。言い換えると、リテラルと節の選択肢のシーケンス（おそらく多数の中から）が存在し、そのシーケンスが空のゴールと充足可能なストアにつながる場合、このセマンティクスの下でゴールが証明されます。 ${\displaystyle \langle G,\emptyset \rangle }$${\displaystyle \langle \emptyset ,S\rangle }$

実際のインタープリタは、目標要素をLIFO順序で処理します。つまり、要素は先頭に追加され、先頭から処理されます。また、記述された順序に従って 2 番目のルールの句を選択し、制約ストアが変更されたときにそれを書き換えます。

3 つ目の遷移の種類は、制約ストアを同等のものに置き換えることです。この置き換えは、制約伝播などの特定の方法によって行われるものに限定されます。制約論理プログラミングのセマンティクスは、使用される制約の種類だけでなく、制約ストアを書き換える方法にも依存します。実際に使用される特定の方法は、制約ストアをより簡単に解決できるものに置き換えます。制約ストアが満たされない場合、この単純化によってこの満たされないことが検出される場合もありますが、常に検出されるとは限りません。

制約ロジック プログラムに対して目標を評価した結果は、目標が証明された場合に定義されます。この場合、最初のペアから目標が空のペアへの派生が存在します。この 2 番目のペアの制約ストアは、評価の結果と見なされます。これは、制約ストアに、目標を証明するために満たすことができると想定されるすべての制約が含まれているためです。言い換えると、これらの制約を満たすすべての変数評価に対して目標が証明されます。

2 つのリテラルの引数のペアワイズ等価性は、多くの場合、 によって簡潔に表されます。これは、制約 の省略形です。制約論理プログラミングのセマンティクスの一般的なバリエーションは、目標ではなく制約ストアに直接追加されます。 ${\displaystyle L(t_{1},\ldots,t_{n})=L(t_{1}',\ldots,t_{n}')}$${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'}$${\displaystyle L(t_{1},\ldots,t_{n})=L(t_{1}',\ldots,t_{n}')}$

用語の異なる定義が使用され、ツリー、実数、または有限領域上の異なる種類の制約論理プログラミングが生成されます。常に存在する制約の一種は、用語の等価性です。このような制約が必要なのは、リテラルが、ヘッドがである節の新しいバリアントの本体に置き換えられるt1=t2たびに、インタープリターが目標に追加するためです。 P(...t1...)P(...t2...)

ツリー項を使用した制約論理プログラミングは、制約ストアに制約として置換を保存することで、通常の論理プログラミングをエミュレートします。項は、他の項に適用される変数、定数、および関数シンボルです。考慮される制約は、項間の等式と不等式のみです。等式は特に重要です。なぜなら、次のような制約はインタープリタによって生成されることが多いからです。項の等式制約は、統一t1=t2によって簡略化、つまり解決できます。

両方の項が他の項に適用された関数記号である場合、制約t1=t2を簡略化できます。 2 つの関数記号が同じで、サブ項の数も同じである場合、この制約はサブ項のペアワイズ等式に置き換えることができます。 項が異なる関数記号で構成されている場合、または同じ関数であっても項の数が異なる場合、制約は満たされません。

2 つの項のうちの 1 つが変数である場合、その変数が取ることができる唯一の許容値は、もう 1 つの項です。その結果、もう 1 つの項は、現在の目標と制約ストア内の変数を置き換えることができるため、実質的にその変数は考慮の対象から除外されます。変数がそれ自体と等しいという特定のケースでは、制約は常に満たされているため、削除できます。

この形式の制約充足では、変数の値は項です。

実数を使用した制約論理プログラミングでは、項として実数式を使用します。関数シンボルが使用されていない場合、項は実数に対する式であり、変数が含まれる場合もあります。この場合、各変数は値として実数のみを取ることができます。

正確に言うと、項は変数と実定数に関する式です。項間の等価性は、インタープリタが実行中に項の等価性を生成するため、常に存在する一種の制約です。たとえば、現在の目標の最初のリテラルが でA(X+1)、インタープリタが の節を に書き換えた後に が変数であると選択した場合A(Y-1):-Y=1、現在の目標に追加される制約はX+1=Y-1とです。関数シンボルに使用される簡略化の規則は明らかに使用されていません。最初の式が を使用して構築され、2 番目の式が を使用して構築されているからといって、 が満たされないわけではありません。 ${\displaystyle Y=1}$X+1=Y-1+-

実数と関数記号を組み合わせることができ、実数に対する式である項と、他の項に適用された関数記号になります。正式には、変数と実定数は、他の式に対する算術演算子と同じように式です。変数、定数 (ゼロ引数関数記号)、および式は、項に適用された関数記号と同じように項です。つまり、項は式に対して構築され、式は数値と変数に対して構築されます。この場合、変数は実数と項にわたっています。つまり、変数は値として実数を取ることができ、別の変数は項を取ることができます。

2 つの項のどちらも実数式でない場合は、2 つの項の等式はツリー項の規則を使用して簡略化できます。たとえば、2 つの項の関数記号とサブ項の数が同じである場合、それらの等式制約はサブ項の等式に置き換えることができます。

制約論理プログラミングで使用される 3 番目の制約クラスは、有限ドメインの制約です。この場合、変数の値は有限ドメイン (多くの場合、整数 )から取得されます。各変数に対して、異なるドメインを指定できます。X::[1..5]たとえば、 は、 の値がと のX間であることを意味します。変数のドメインは、変数が取ることのできるすべての値を列挙することによっても指定できます。したがって、上記のドメイン宣言は と書くこともできます。この 2 番目のドメイン指定方法では、 などの整数で構成されていないドメインを使用できます。変数のドメインが指定されていない場合は、言語で表現可能な整数の集合であると見なされます。 のような宣言を使用して、変数のグループに同じドメインを与えることができます。 15X::[1,2,3,4,5]X::[george,mary,john][X,Y,Z]::[1..5]

変数のドメインは、実行中に縮小される場合があります。実際、インタープリタが制約ストアに制約を追加すると、制約の伝播が実行され、ローカル一貫性の形式が強制され、これらの操作によって変数のドメインが縮小される場合があります。変数のドメインが空になると、制約ストアに一貫性がなくなり、アルゴリズムはバックトラックします。変数のドメインがシングルトンになると、その変数にはそのドメイン内の一意の値を割り当てることができます。通常強制される一貫性の形式は、アーク一貫性、ハイパーアーク一貫性、および境界一貫性です。変数の現在のドメインは、特定のリテラルを使用して検査できます。たとえば、は変数のdom(X,D)現在のドメインを調べます。 DX

実数の定義域と同様に、関数は整数の定義域でも使用できます。この場合、項は整数に対する式、定数、または他の項に対する関数の適用になります。変数は、その定義域が整数または定数のセットとして指定されていない場合、任意の項を値として取ることができます。

制約ストアには、現在充足可能であると想定されている制約が含まれます。これは、通常の論理プログラミングの現在の置換と考えることができます。ツリー項のみが許可されている場合、制約ストアには という形式の制約が含まれます。t1=t2これらの制約は統合によって簡略化され、 という形式の制約になりますvariable=term。このような制約は置換と同等です。

t1!=t2ただし、項間の差が許される場合、制約ストアには という形式の制約も含まれることがあります。実数または有限領域上の制約が許される場合、制約ストアにはなどの !=領域固有の制約も含まれることがあります。X+2=Y/2

制約ストアは、現在の置換の概念を 2 つの方法で拡張します。まず、リテラルを節の新しいバリアントのヘッドと等しくすることから得られる制約だけでなく、節の本体の制約も含まれます。次に、フォームの制約だけでなくvariable=value、考慮されている制約言語の制約も含まれます。通常のロジック プログラムの評価が成功した結果は最終的な置換ですが、制約ロジック プログラムの結果は最終的な制約ストアであり、これにはフォームの制約variable=valueだけでなく任意の制約も含まれる場合があります。

ドメイン固有の制約は、節の本体から、およびリテラルを節のヘッドと等しくすることの両方から制約ストアにもたらされる場合があります。たとえば、インタープリタが、A(X+2)新しいバリアント ヘッドが である節でリテラルを書き換えるとA(Y/2)、制約がX+2=Y/2制約ストアに追加されます。変数が実数または有限ドメインの式に現れる場合、その変数は実数または有限ドメインの値のみを取ることができます。このような変数は、他の項に適用された関数で構成された項を値として取ることはできません。変数が特定のドメインの値と項に適用された関数の両方を取るようにバインドされている場合、制約ストアは満たされません。

制約が制約ストアに追加されると、制約ストアに対していくつかの操作が実行されます。実行される操作は、考慮されるドメインと制約によって異なります。たとえば、有限ツリー等式には統合が使用され、実数上の多項式方程式には変数消去が使用され、有限ドメインのローカル一貫性の形式を強制するには制約伝播が使用されます。これらの操作は、制約ストアの充足可能性のチェックと解決をより簡単にすることを目的としています。

これらの操作の結果、新しい制約を追加すると、古い制約が変更される場合があります。インタープリタがバックトラックするときにこれらの変更を元に戻せることが重要です。最も単純な方法は、インタープリタが選択を行うたびに (目標を書き換える節を選択するたびに) ストアの完全な状態を保存することです。制約ストアを以前の状態に戻すためのより効率的な方法があります。特に、2 つの選択ポイント間で行われた制約ストアの変更 (古い制約に対する変更を含む) を保存するだけで済みます。これは、変更された制約の古い値を保存するだけで実行できます。この方法は、トレーリングと呼ばれます。より高度な方法は、変更された制約に対して行われた変更を保存することです。たとえば、線形制約は係数を変更することで変更されます。古い係数と新しい係数の差を保存することで、変更を元に戻すことができます。この 2 番目の方法は、制約の古いバージョンだけでなく、変更の意味が保存されるため、 セマンティック バックトラッキングと呼ばれます。

ラベル付けリテラルは、有限ドメイン上の変数に対して、制約ストアの充足可能性または部分充足可能性をチェックし、満足できる割り当てを見つけるために使用されます。ラベル付けリテラルは の形式でありlabeling([variables])、引数は有限ドメイン上の変数のリストです。インタープリタがこのようなリテラルを評価するときは常に、リストの変数のドメインを検索して、関連するすべての制約を満たす割り当てを見つけます。通常、これはバックトラッキングの形式によって行われます。つまり、変数は順番に評価され、それぞれに可能なすべての値を試し、不一致が検出されるとバックトラッキングが行われます。

ラベル付けリテラルの最初の用途は、制約ストアの充足可能性または部分充足可能性を実際にチェックすることです。インタープリタが制約ストアに制約を追加すると、その制約ストアに対してローカル一貫性の形式のみが強制されます。この操作では、制約ストアが充足不可能な場合でも不整合が検出されない場合があります。変数セットに対するラベル付けリテラルは、これらの変数に対する制約の充足可能性チェックを強制します。その結果、制約ストアで言及されているすべての変数を使用すると、ストアの充足可能性がチェックされます。

ラベル付けリテラルの 2 つ目の用途は、制約ストアを満たす変数の評価を実際に決定することです。ラベル付けリテラルがない場合、制約ストアに形式の制約が含まれておりX=value、ローカル一貫性によって変数のドメインが単一の値に縮小される場合にのみ、変数に値が割り当てられます。一部の変数に対するラベル付けリテラルは、これらの変数を強制的に評価します。つまり、ラベル付けリテラルが考慮された後、すべての変数に値が割り当てられます。

通常、制約ロジック プログラムは、制約ストアに可能な限り多くの制約が蓄積された後にのみラベル付けリテラルが評価されるように記述されます。これは、ラベル付けリテラルによって検索が強制され、満たすべき制約が多いほど検索が効率的になるためです。制約充足問題は、通常、次の構造を持つ制約ロジック プログラムによって解決されます。

解決( X ):-制約( X )、 ラベル付け( X )
制約( X ) :-  ( CSPのすべての 制約 )  

インタープリタが目標 を評価するとsolve(args)、最初の節の新しい変形の本体が現在の目標に配置されます。最初の目標は であるためconstraints(X')、2 番目の節が評価され、この操作によってすべての制約が現在の目標に移動し、最終的には制約ストアに移動します。次に、リテラルlabeling(X')が評価され、制約ストアのソリューションの検索が強制されます。制約ストアには元の制約充足問題の制約が正確に含まれているため、この操作によって元の問題のソリューションが検索されます。

与えられた制約論理プログラムは、効率を改善するために再定式化される場合があります。最初のルールは、ラベル付けリテラルは、ラベル付けリテラルに対する制約が制約ストアにできるだけ蓄積された後に配置する必要があるということです。理論上は はと同等ですが、インタープリタがラベル付けリテラルに遭遇したときに実行される検索は、制約 を含まない制約ストアに対して行われます。その結果、 などのソリューションが生成される可能性がありますが、後でこの制約を満たさないことがわかります。一方、2 番目の定式化では、制約がすでに制約ストアにある場合にのみ検索が実行されます。その結果、検索は、追加の制約によって検索空間が縮小されるという事実を利用して、それと一致するソリューションのみを返します。 A(X):-labeling(X),X>0A(X):-X>0,labeling(X)X>0X=-1

効率を上げることができる 2 つ目の書き直しは、節の本体で制約をリテラルの前に置くことです。 と は、この場合も原理的には同等です。 ただし、最初の方法ではより多くの計算が必要になる場合があります。 たとえば、制約ストアに制約 が含まれている場合、最初のケースではインタープリタが再帰的に評価します。評価に成功した場合は、 を追加するときに制約ストアに矛盾があることがわかります。 2 つ目のケースでは、その節を評価するときに、インタープリタは最初に制約ストアに を追加し、次に を評価する可能性があります。 を追加した後の制約ストアに矛盾があることが判明したため、 の再帰評価はまったく実行されません。 A(X):-B(X),X>0A(X):-X>0,B(X)X<-2B(X)X>0X>0B(X)X>0B(X)

効率性を高めることができる 3 つ目の再定式化は、冗長な制約の追加です。プログラマーが (どのような方法でも) 問題の解決が特定の制約を満たすことを知っていれば、その制約を含めて、できるだけ早く制約ストアの不整合を引き起こすことができます。たとえば、 の評価B(X)により の値が正になることが事前にわかっている場合X、プログラマーはX>0が発生する前にを追加できますB(X)。たとえば、A(X,Y):-B(X),C(X)は目標 で失敗しますA(-2,Z)が、これはサブ目標 の評価中にのみ判明しますB(X)。一方、上記の節が に置き換えられた場合、インタープリターはの評価が開始される前に制約が制約ストアに追加されるとすぐにバックトラックします。 A(X,Y):-X>0,A(X),B(X)X>0B(X)

制約処理ルールは、当初は制約ソルバーを指定するためのスタンドアロン形式として定義され、後に論理プログラミングに組み込まれました。制約処理ルールには 2 種類あります。最初の種類のルールは、特定の条件下で、制約セットが別の制約セットと同等であることを指定します。2 番目の種類のルールは、特定の条件下で、制約セットが別の制約セットを意味することを指定します。制約処理ルールをサポートする制約論理プログラミング言語では、プログラマーはこれらのルールを使用して、制約ストアの可能な書き換えと制約ストアへの可能な制約の追加を指定できます。次にルールの例を示します。

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

最初のルールは、B(X)がストアによって含意される場合、制約はA(X)と書き直すことができることを示していますC(X)。たとえば、ストアが を意味する場合、 はN*X>0と書き直すことができます。 記号は論理の等価性に似ており、最初の制約が後者と同等であることを示しています。実際には、これは最初の制約を後者に 置き換えることができることを意味します。X>0N>0<=>

2 番目のルールでは、中間の制約が制約ストアによって伴われる場合、後者の制約が最初の制約の結果であると指定します。結果として、がA(X)制約ストアにあり、B(X)制約ストアによって伴われる場合、をC(X)ストアに追加できます。同等の場合とは異なり、これは追加であり、置き換えではありません。新しい制約が追加されますが、古い制約はそのまま残ります。

同値性により、いくつかの制約をより単純なものに置き換えることで制約ストアを単純化できます。特に、同値性ルールの 3 番目の制約が でtrue、2 番目の制約が伴う場合、最初の制約は制約ストアから削除されます。推論により、新しい制約を追加できます。これにより、制約ストアの矛盾が証明される可能性があり、一般に、その充足可能性を確立するために必要な検索の量を減らすことができます。

制約処理規則と組み合わせた論理プログラミング節は、制約ストアの充足可能性を確立するための方法を指定するために使用できます。方法のさまざまな選択を実装するために、さまざまな節が使用されます。制約処理規則は、実行中に制約ストアを書き換えるために使用されます。例として、次のように単位伝播によるバックトラッキングを実装できます。 はholds(L)命題節を表します。この命題節では、リスト内のリテラルはL評価される順序と同じになります。このアルゴリズムは、リテラルを true または false に割り当てる選択の節と、伝播を指定する制約処理規則を使用して実装できます。これらの規則は、ストアから が続くholds([l|L])場合は を削除できること、ストアから が続く場合はのように書き換えられることを指定します。同様に、は に置き換えることができます。この例では、変数の値の選択は論理プログラミングの節を使用して実装されていますが、これは、選言制約処理規則または CHR ^∨と呼ばれる拡張機能を使用して制約処理規則にエンコードできます。 l=trueholds(L)l=falseholds([l])l=true

論理プログラムを評価する標準的な戦略は、トップダウンと深さ優先です。つまり、目標から、目標を証明できる可能性のあるいくつかの節が識別され、その本体のリテラルに対して再帰が実行されます。別の戦略は、事実から始めて節を使用して新しい事実を導き出すことです。この戦略はボトムアップと呼ばれます。単一の目標を証明するのではなく、特定のプログラムのすべての結果を生成することが目的である場合、トップダウンよりも優れていると考えられています。特に、標準的なトップダウンと深さ優先の方法でプログラムのすべての結果を見つけることは終了しない可能性がありますが、ボトムアップの評価戦略は終了します。

ボトムアップ評価戦略では、評価中にこれまでに証明された事実のセットが維持されます。このセットは最初は空です。各ステップで、既存の事実にプログラム句を適用することで新しい事実が導出され、セットに追加されます。たとえば、次のプログラムのボトムアップ評価には 2 つのステップが必要です。

A(q)。
B(X):-A(X)。

結果のセットは最初は空です。最初のステップでは、A(q)は本体が証明できる唯一の節であり (空であるため)、A(q)したがって現在の結果のセットに追加されます。2 番目のステップでは、A(q)が証明されているため、2 番目の節が使用でき、 がB(q)結果に追加されます。 から他の結果が証明できないため{A(q),B(q)}、実行は終了します。

ボトムアップ評価がトップダウン評価よりも優れている点は、導出の循環によって無限ループが発生しないことです。これは、すでに結果が含まれている現在の結果セットに結果を追加しても効果がないからです。たとえば、上記のプログラムに 3 番目の節を追加すると、トップダウン評価で導出の循環が生成されます。

A(q)。
B(X):-A(X)。
A(X):-B(X)。

たとえば、目標に対するすべての回答を評価する際にA(X)、トップダウン戦略では次の導出が生成されます。

あ(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q)、B(q):-A(q)、A(q):-B(q)、B(q):-A(q)、A(q)

言い換えれば、A(q)最初に唯一の結果が生成されますが、その後、アルゴリズムは他の答えを生成しない導出を循環します。より一般的には、トップダウン評価戦略は、他の導出が存在する可能性がある場合、可能な導出を循環する場合があります。

ボトムアップ戦略には同じ欠点はありません。すでに導出された結果は効果がないからです。上記のプログラムでは、ボトムアップ戦略はA(q)結果のセットへの追加を開始します。2 番目のステップでは、B(X):-A(X)を使用して を導出しますB(q)。3 番目のステップでは、現在の結果から導出できる唯一の事実は と ですA(q)がB(q)、これらはすでに結果のセットに含まれています。その結果、アルゴリズムは停止します。

上記の例では、使用されたファクトはグラウンド リテラルのみです。一般に、本体に制約のみを含む節はすべてファクトと見なされます。たとえば、節A(X):-X>0,X<10もファクトと見なされます。この拡張されたファクトの定義では、構文的には等しくなくても、いくつかのファクトが等価である場合があります。たとえば、 はA(q)と等価でありA(X):-X=q、両方とも と等価ですA(X):-X=Y, Y=q。この問題を解決するために、ファクトは、ヘッドにすべて異なる変数のタプルが含まれる通常の形式に変換されます。2 つのファクトの本体がヘッドの変数に対して等価である場合、つまり、これらの変数に制限されたときにそれらのソリューション セットが同じである場合、2 つのファクトは等価です。

説明したように、ボトムアップ アプローチには、すでに導出された結果を考慮しないという利点があります。ただし、すでに導出された結果のいずれとも等しくない結果によって必然的に生じる結果が依然として導出される可能性があります。たとえば、次のプログラムのボトムアップ評価は無限です。

A ( 0 )。
A ( X ):- X > 0。A 
( X ):- X = Y + 1 、A ( Y ) 。 

ボトムアップ評価アルゴリズムは、まず がおよびA(X)に対して真であることを導出します。2 番目のステップでは、3 番目の節を持つ最初の事実により を導出できます。3 番目のステップでは、が導出されます。などとなります。ただし、これらの事実は、 が任意の非負 に対して真であることを導出するという事実によって既に含意されています。この欠点は、現在の結果セットに追加される含意事実をチェックすることで克服できます。新しい結果が既にセットによって含意されている場合は、追加されません。事実は節として保存され、場合によっては「ローカル変数」も含まれるため、含意はそれらのヘッドの変数に制限されます。 X=0X>0A(1)A(2)A(X)X

制約論理プログラミングの並行バージョンは、制約充足問題を解決するのではなく、並行プロセスをプログラミングすることを目的としています。制約論理プログラミングの目標は並行して評価されます。したがって、並行プロセスは、インタープリタによる目標の評価としてプログラムされます。

構文的には、並行制約論理プログラムは非並行プログラムに似ていますが、唯一の例外は、節にガード (いくつかの条件下では節の適用をブロックする制約) が含まれることです。意味的には、並行制約論理プログラミングは、目標評価が問題の解決策を見つけることではなく、並行プロセスを実現することを目的としているため、非並行バージョンとは異なります。最も顕著なのは、この違いが、複数の節が適用可能な場合のインタープリタの動作に影響することです。非並行制約論理プログラミングはすべての節を再帰的に試行しますが、並行制約論理プログラミングは 1 つだけを選択します。これは、インタープリタの意図された方向性の最も明白な効果であり、インタープリタは以前に選択した選択を修正することはありません。これによるその他の効果は、評価全体が失敗しない間に証明できない目標を持つ意味上の可能性、および目標と節のヘッドを等しくする特定の方法です。

制約論理プログラミングは、自動スケジューリング、^[1] 型推論、^[2] 土木工学、機械工学、デジタル回路検証、航空管制、金融など、多くの分野に応用されてきました。 ^[要出典]

制約論理プログラミングは、1987年にJaffarとLassezによって導入されました。^{[3]彼らは、} Prolog IIの項方程式と項分離が制約の特定の形式であるという観察を一般化し、このアイデアを任意の制約言語に一般化しました。この概念の最初の実装は、Prolog III、CLP(R)、およびCHIPでした。^{[引用が必要]}

• B-プロローグ
• BNR Prolog (別名 CLP(BNR))
• 制約処理ルール
• チャオ
• CLP(R)
• 配布されたオズモーツァルト
• 日食
• GNUプロローグ
• SWI-プロローグ

• デヒター、リナ（2003）。制約処理。モーガン・カウフマン。ISBN 1-55860-890-7。  1-55860-890-7出版年月日
• Apt, Krzysztof (2003)。制約プログラミングの原理。ケンブリッジ大学出版局。ISBN 0-521-82583-0。  0-521-82583-0出版年月日
• Marriott, Kim; Peter J. Stuckey (1998)。制約付きプログラミング: 入門。MIT プレス。  0-262-13341-5出版年月日
• Frühwirth, Thom; Slim Abdennadher (2003).制約プログラミングの基礎. Springer. ISBN 3-540-67623-6。  3-540-67623-6出版年月日
• Jaffar, Joxan; Michael J. Maher (1994). 「制約論理プログラミング: 概観」. Journal of Logic Programming . 19/20: 503–581. doi : 10.1016/0743-1066(94)90033-7 .
• Colmerauer, Alain (1987)。「Prolog III ユニバースの開拓」。Byte 、 8 月。