制約論理プログラミング

制約論理プログラミングは、制約充足の概念を取り入れるように論理プログラミングを拡張した制約プログラミングの一形態です。制約論理プログラムとは、節の本体に制約を含む論理プログラムです。制約を含む節の例は です。この節では、は制約であり、、、 およびは通常の論理プログラミングと同様にリテラルです。この節は、がゼロより大きく、 および の両方が真であるという、ステートメントが成り立つ条件を 1 つ示しています。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。

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

初期状態では、現在の目標は目標であり、制約ストアは空です。インタプリタは、現在の目標から最初の要素を削除して解析することで処理を進めます。この解析の詳細は後述しますが、最終的にこの解析は正常終了または失敗となる可能性があります。この解析には、再帰呼び出しや、現在の目標への新しいリテラルの追加、制約ストアへの新しい制約の追加が含まれる場合があります。失敗が発生した場合は、インタプリタはバックトラックします。正常終了は、現在の目標が空であり、制約ストアが充足可能である場合に発生します。

目標から削除されたリテラルの分析の詳細は以下のとおりです。目標の先頭からこのリテラルを削除した後、それが制約かリテラルかを確認します。制約の場合は、制約ストアに追加されます。リテラルの場合は、そのリテラルと同じ述語を持つヘッドを持つ節が選択されます。その節は、その変数を新しい変数（目標に存在しない変数）に置き換えることで書き換えられます。この結果は、節の新しいバリアントと呼ばれます。次に、節の新しいバリアントの本体が目標の先頭に配置されます。リテラルの各引数と新しいバリアントのヘッドの対応する引数との等価性も、目標の先頭に配置されます。

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

現在の目標が空で、制約ストアが充足不能と検出されない場合、インタプリタは目標を証明したことになります。実行結果は、現在の（簡略化された）制約のセットです。このセットには、次のような制約が含まれる場合があります。${\displaystyle X=2}$変数を特定の値に強制するだけでなく、次のような制約も含まれる場合があります。${\displaystyle X>2}$それは、変数に特定の値を与えることなく、単に変数を束縛するだけです。

形式的には、制約論理プログラミングのセマンティクスは導出の観点から定義される。遷移は、目標/ストアのペアのペアであり、${\displaystyle \langle G,S\rangle \rightarrow \langle G',S'\rangle }$このようなペアは、ある状態から別の状態へ移行する可能性を示しています。${\displaystyle \langle G,S\rangle }$述べる${\displaystyle \langle G',S'\rangle }$このような移行は、以下の3つの場合に起こり得る。

• 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'}$Gは​${\displaystyle L(t_{1},\ldots ,t_{n})}$に置き換えられました${\displaystyle t_{1}=t_{1}',\ldots ,t_{n}=t_{n}',B}$、 そして${\displaystyle S'=S}$言い換えれば、リテラルは、ヘッドに同じ述語を持つ節の新しいバリアントの本体で置き換えることができ、新しいバリアントの本体と上記の項の等価性を目標に追加します。
• Sと${\displaystyle S'}$特定の制約意味論に従って同等である

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

実際のインタープリタは、目標要素を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の制約が格納されます。これらの制約は単一化によって単純化され、 の形式の制約になります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、かつ局所的な一貫性によって変数のドメインが単一の値に縮小される場合にのみ値が割り当てられます。一部の変数にラベリングリテラルを適用すると、これらの変数が強制的に評価されます。つまり、ラベリングリテラルが考慮された後、すべての変数に値が割り当てられます。

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

solve ( X ):- constraints ( X ), labeling ( X ) constraints ( 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種類あります。1つ目のルールは、与えられた条件下で、ある制約セットが別の制約セットと等価であることを指定します。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評価される順序と同じです。このアルゴリズムは、リテラルを真または偽に割り当てる選択のための句と、伝播を指定するための制約処理ルールを使用して実装できます。これらのルールは、ストアから が続く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)、トップダウン戦略では次のような導出結果が得られます。

A ( 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)、これらは既に結果のセットに含まれています。結果として、アルゴリズムは停止します。

上記の例では、使用された事実はグラウンドリテラルのみでした。一般に、本文に制約のみを含む節はすべて事実とみなされます。たとえば、節も事実とみなされます。事実のこの拡張定義では、構文的に等しくなくても同等の事実が存在する場合があります。たとえば、はと同等であり、両方ともと同等です。この問題を解決するために、事実はヘッドがすべて異なる変数のタプルを含む正規形に変換されます。2 つの事実は、ヘッドの変数に関して本文が同等である場合、つまり、これらの変数に制限した場合の解の集合が同じである場合に同等です。A(X):-X>0,X<10A(q)A(X):-X=qA(X):-X=Y,Y=q

前述のとおり、ボトムアップアプローチには、既に導き出された結果を考慮しないという利点があります。しかし、既に導き出された結果から必然的に導かれる結果を導き出す可能性があり、それらの結果と等しくない場合もあります。例として、次のプログラムのボトムアップ評価は無限大になります。

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プロローグ（別名CLP(BNR)）
• 制約処理ルール
• チャオ
• CLP(R)
• 配給されたオズ・モーツァルト
• ECLiPSe
• GNU Prolog
• SWI-Prolog

• デクター、リナ（2003）。制約処理。モーガン・カウフマン。ISBN 1-55860-890-7。ISBN 1-55860-890-7
• アプト、クリストフ（2003）。制約プログラミングの原理。ケンブリッジ大学出版局。ISBN 0-521-82583-0。ISBN 0-521-82583-0
• マリオット、キム、ピーター・J・スタッキー（1998）。制約付きプログラミング入門。MIT Press。ISBN 0-262-13341-5
• Frühwirth, Thom; Slim Abdennadher (2003).制約プログラミングの基礎. Springer. ISBN 3-540-67623-6。ISBN 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 .
• コルメラウアー、アラン（1987）。「プロローグIIIユニバースの開拓」。バイト。8月。