制約論理プログラミング

制約論理プログラミング（せいやくろんりプログラミング、英: constraint logic programming）は制約プログラミングの一種で、制約という問題表現・解決の考え方を導入することによって論理プログラミングを拡張したプログラミングパラダイムである。論理プログラミングの持っている宣言的な表現力に制約の考え方を導入し、より一般化したものとも言うことができる。

概要

問題の対象間の関係を制約（例えば V=I*R ）という形で宣言的に記述する制約プログラミングの考え方は、述語という形で関係を宣言的に記述する論理プログラミングと多くの特徴を共有している。理論的に、論理プログラミングはエルブラン領域(Herbrand universe)という有限木で表される領域上でのユニフィケーションによる等号制約を扱う制約プログラミングと見なすことができ、制約論理プログラミングはその自然な拡張となっている。論理プログラミングの代表的な言語であるProlog処理系の多くには、何らかの制約論理プログラミングの機能やライブラリが用意されている。

制約論理プログラミングの応用分野は、スケジューリング、要員計画・輸送・資源割り当て、アナログ回路設計、トレーディングなどさまざまなものがある。

一般に、制約論理プログラムはPrologなどの論理プログラムと同様の形式で記述するが、節（clause）のボディ部に制約を含めることができる。以下の例では V = I*R などが制約である。手続型言語の代入文とは異なり、これらの式は関係を表現している。

register(V,I,R) :- V = I*R.     % オームの法則
parallel_register(V,I,R1,R2) :- I1+I2=I, register(V,I1,R1), register(V,I2,R2).  % 並列回路
serial_register(V,I,R1,R2)   :- V1+V2=V, register(V1,I,R1), register(V2,I,R2).  % 直列回路

例えば、上記のプログラムで ?- parallel_register(50,I,10,25). を実行すると I = 7 が結果として返る。

プログラムの実行は、論理プログラムと同じように、規則が順次呼び出されることで行われる。途中で現れた制約（例えば I1+I2=I ）は、いったんシステム内部の制約ストアと呼ばれる領域に格納され、順次内部の制約評価系でより単純な形に簡約化が行われる（例えば I1+I2=I & 50=I1*10 → 5+I2=I ）。

歴史

制約をソフトウェアに応用する試みは、初期の対話型グラフィックシステムであるSKETCHPAD(1963)にまでさかのぼることができる。 プログラミング言語への応用としては、Steeleらにより開発されたCONSTRAINTS(1980) があり、制約を変数間の関係の規則として記述し、局所制約伝播（local constraints propagation）により変数の値を順次決めていくことで、制限された範囲ではあるが制約を扱うことができた。

1972年にカルメラウアらにより開発されたPrologは、関係の宣言的な表現という視点を汎用プログラミング言語に持ち込むことに成功し、論理プログラミングという考え方をもたらした。しかしそれはエルブラン領域(Herbrand universe)を対象とした限定されたもので、実数や有理数など他の領域のデータの扱いは通常の関数型言語や手続型言語と変わりがなかった。Prologは、論理プログラミングの宣言的な性格を活かしつつ表現力や処理効率を上げるため、より多くの領域での一般的な制約を扱うように拡張された。カルメラウアによるProlog Ⅱ(1980)は制約という言葉を明示的に使用した最初の論理プログラミング言語である。 これはさらにProlog Ⅲ(1987)などの制約論理プログラミング言語に発展した。 IBMのJafferやLassezらは1987年に制約論理プログラミングスキーマCLP(X)を発表し、制約論理プログラミングの理論化を行った。CLP(X)に基づき実数領域の制約を扱うCLP(R)、有限領域を扱うCLP(FD)などの各種言語が開発された。また、CHIP(Constraint Handling In Prolog)やCALなど多くの制約論理プログラミング言語が開発された。また制約論理プログラミングの機能を持つProlog処理系も多数作成されている。 これらの制約論理プログラミングの研究と並行して、論理プログラミングの並行処理への応用として1980年代に研究された並行論理プログラミングも制約論理プログラミングの影響を受け、制約で並行処理を制御する並行制約プログラミングとして理論化が行われた。

領域

制約論理プログラミングにおける制約は何らかの特定の領域（Domain）に関するものである。対象とする領域ごとに制約の指定方法や処理方法は異なる。制約論理プログラミングでの一般的な領域としては、論理プログラミングの基本的な計算領域である木以外に、有限領域、ブール領域、有理数や実数などを扱う算術領域がある。

木（tree）

論理プログラミングでは任意の有限木(tree)を表す項（term）を基本データとしているため、制約論理プログラミングでも木は基本的な計算領域として扱うことができる。ユニフィケーションによる等号制約（＝）が基本的な制約である。項は以下の再帰的な定義で表される。

• 任意の定数 c は項である。
• 任意の変数 X は項である。
• 任意の関数記号 f と複数の項からなる複合項 f(t₁, .. ,t_n) は項である。

例えば、f(X,g(a,b,h(Y))) は項である。データの並びを表すリスト（例： [1,2,3] ）も先頭要素と残りの要素の2つの引数からなる項の特別な表現方法と見なすことができる。

制約論理プログラミング言語のProlog Ⅲは無限木の等号制約と不等号制約を扱うことができる。

有限領域

有限領域（Finite Domains）は、有限集合について制約を扱う領域である。多くの制約充足問題はこの領域で表現することができる。変数の値として有限領域の要素をとるもので、特定の範囲内の整数などがその代表である。個々の変数について、例えば1から5までの整数であれば X::[1..5] （あるいは X::[1,2,3,4,5] ）のように領域が指定される。数値以外であれば X::[george,mary,john] のような形になる。 有限領域での制約としては算術式による制約や記号的制約などが使われ、言語により指定方法は異なる。以下は古典的な覆面算 SEND+MORE=MONEY を解くプログラムの例である。

sendmore(Digits) :-
    Digits = [S,E,N,D,M,O,R,Y],        % 変数生成
    Digits :: [0..9],                  % 変数の領域を定義
    S #\= 0,                           % 制約: S, M は 0 ではない
    M #\= 0,
    alldifferent(Digits),              % 制約: 要素はそれぞれ異なった値となる
    1000*S+100*E+10*N+D + 1000*M+100*O+10*R+E
      #= 10000*M+1000*O+100*N+10*E+Y,  % 制約: SEND+MORE=MONEY
    labeling(Digits).                  % 探索開始

有限領域では、制約の一貫性チェックにより各変数の取りえる領域が変化した場合、その変化を制約伝播により他の関連する変数の領域に反映し、解の範囲を順次狭めていくことで最終的な解を求めることが多い。全体の一貫性が取れなくなった場合はバックトラックを行い途中からやり直す。

算術領域

算術領域（Arithmetic Domain）は、整数領域、有理数領域、実数領域などがある。扱える制約は代数式で表される代数制約で、大きく以下の2種類に分かれる。

• 線型制約　：線型代数方程式／不等式
• 非線型制約：非線型代数方程式／不等式

線型制約はシンプレックス法などにより効率的に解け、多くの制約論理プログラミング言語でサポートされている。非線型制約は一般的な解法が無いため、遅延評価により非線型の式が線型になった後（例えば、 X*Y+Y*Y=-3 & Y=2 → 2*X+4=-3 ）に評価したり、代数方程式をより扱いやすくするためブッフバーガーアルゴリズムで求めたグレブナー基底（Gröbner basis）で正規化した式で評価するなどの方法がとられる。 以下は実数領域での非線型制約を扱う制約論理プログラミング言語CLP(R)のプログラム例である。

zmul(R1, I1, R2, I2, R3, I3) :-
    R3 = R1*R2 - I1*I2,
    I3 = R1*I2 + R2*I1.

以下はプログラムの実行例で、具体的な値が求まればその値が、そうでなければ各値の方程式が結果として返る。

?- zmul(1, 2, 3, 4, R3, I3).
  R3 = -5
  I3 = 10
  *** Yes
?- zmul(1, 2, R2, I2, R3, I3).
  I2 = 0.2*I3 - 0.4*R3
  R2 = 0.4*I3 + 0.2*R3
  *** Yes

制約が矛盾しなかった場合は解と"Yes"を、矛盾すれば"No"を結果として返すが、非線型のままの制約が残ってしまいYes/Noとも判定できない場合もあり、その場合は残った制約の式と"maybe"を結果として返すようになっている。

ブール領域

ブール領域（Boolean Domain）は真偽値の制約だけを扱う領域である。制約は一般的な論理演算子で構成される等式として表現される。制約処理方法としては、Booleの変数除去に基づいたブーリアン・ユニフィケーションやSL-導出（SL-resolution）のブール式への応用など様々なものがある。Prolog ⅢやCHIP(Constraint Handling In Prolog)などの処理系ではブール領域の制約を扱うことができる。

セマンティック

制約論理プログラミングの論理的意味や操作的意味、不動点意味論上の分析はIBMのJafferやLassezらにより与えられている。以下では操作的意味について扱う。

操作的意味

制約論理プログラミングを状態遷移システムとしてとらえた場合の操作的意味は状態 $\langle A,C,S\rangle$ の遷移として表現できる。 A は原子論理式や制約の多重集合、 C 、 S は制約の多重集合を表す。 C と S とは制約を格納する制約ストアを表し、システム内部の制約評価系の処理対象となる。 A はまだ見えていない原子論理式や制約の集まりを表し、Prologなどの論理プログラミング言語でのゴールの集合にあたる。 C は能動的な(利用可能な)制約の集まりで、 S はまだ利用できない受動的な制約の集まりである。例えば、制約評価系が線型連立方程式のみを扱える場合、 x*y=z のような非線型な式は利用できないため S に格納されるが、もし x＝2 の制約が追加された場合は線型な式 2*y=z に変わるため能動的な制約の集まりである C に格納され、制約評価系で簡約化が行われる。 実行の最初のゴール$G$は、システムの初期状態 $\langle G,\emptyset ,\emptyset \rangle$ で表される。導出が成功した場合、最後の状態は $\langle \emptyset ,C,S\rangle$ であり、 C と S が実行結果となる。

状態遷移システムの遷移は以下のように表現できる。

• $\langle A\cup a,C,S\rangle \rightarrow _{r}\langle A\cup B,C,S\cup (a=h)\rangle$

A 内の原子論理式 a （$L(t_{1},\ldots ,t_{n})$）について、ルール $h\leftarrow B$ があり、ヘッド部 h （$L(t_{1}',\ldots ,t_{n}')$）が変数の書き換えで同じにできる場合。この場合は原子論理式 a を書き換える。ここで $\left(a=h\right)$ は $t_{1}=t_{1}',\ldots ,t_{n}=t_{n}'$ を表す。

• $\langle A\cup a,C,S\rangle \rightarrow _{r}fail$

原子論理式 a を書き換え可能なルール $h\leftarrow B$ がない場合。失敗（fail）する。

• $\langle A\cup c,C,S\rangle \rightarrow _{c}\langle A,C,S\cup c\rangle$

A 内に制約 c があれば制約ストアに移動する。

• $\langle A,C,S\rangle \rightarrow _{i}\langle A,C',S'\rangle$

制約ストア内の制約を制約評価系で簡約化する（$\left(C',S'\right)=infer\left(C,S\right)$）。まだ利用できない受動的な制約の集まり S で利用可能なものがあれば C に移し、利用可能な制約の集まり C はより単純な制約に簡約化する。

• $\langle A,C,S\rangle \rightarrow _{s}\langle A,C,S\rangle$

能動的な制約の集まり C の一貫性チェック $consistent\left(C\right)$ に問題がない場合。そのまま遷移を続ける。

• $\langle A,C,S\rangle \rightarrow _{s}fail$

能動的な制約の集まり C の一貫性チェックが成立しない場合（$\neg consistent(C)$）。失敗（fail）する。

ここで$infer\left(C,S\right)$は制約評価の関数、$consistent\left(C\right)$は制約の一貫性チェック述語を表し、制約の領域ごとに異なる。 多くの制約論理プログラミングシステムの操作的意味は $\rightarrow _{r}\rightarrow _{i}\rightarrow _{s}$ と $\rightarrow _{c}\rightarrow _{i}\rightarrow _{s}$ の遷移の組み合わせで表される。

また、 A からの原子論理式や制約の取り出しと追加はLIFOの順番に行われることが多い。この場合はPrologと同様の深さ優先探索の動作になり、途中で失敗（fail）した場合はバックトラックが行われる。

処理系

以下に制約論理プログラミング言語の例を挙げる:

• B-Prolog （Prologベース、プロプライエタリ）
• CHIP V5 （Prologベース、C++/C言語のライブラリも含む、プロプライエタリ）
• Ciao Prolog （Prologベース、フリーソフトウェア: GPL/LGPL）
• ECLiPSe （Prologベース、オープンソース）
• GNU Prolog（Prologベース、フリーソフトウェア）
• Mozart（Oz言語の処理系、フリーソフトウェア）
• SICStus Prolog （Prologベース、プロプライエタリ）
• YAP Prolog（Prologベース、オープンソース）
• CAL （非線型代数方程式等を対象。ICOTで開発。オープンソース）
• CHAL （階層制約論理型言語。ICOTで開発。オープンソース）
• GDCC （並列制約論理型言語。ICOTで開発。オープンソース）
• Cu Prolog （ICOTで開発。オープンソース）

並行制約プログラミング

詳細は「並行制約プログラミング 」を参照

並行制約プログラミング(Concurrent Constraint Programming)は、制約論理プログラミングの研究と並行論理プログラミングの研究とから生まれた、並行プログラミングのためのパラダイムである。並行制約プログラミングでは並行論理プログラミングをより一般化し、制約の出力(追加, tell)と入力(観測, ask)を行う複数のプロセス（エージェント）でプログラミングを行う。 並行制約プログラミングは、制約充足系（constraint solver）の記述ではなく、複数のプロセス（エージェント）の制御やプロセス間通信の記述を目的としている。

Constraint Handling Rules

詳細は「Constraint Handling Rules 」を参照

Constraint Handling Rules（CHR）は1991年にThom Frühwirthが発表した、ユーザ定義の制約が書けるように設計された宣言型プログラミング言語である 。 多重集合の書換え規則に基づく制約処理モデルを特徴とし、ルールにより制約をより単純な制約に書き換えることで、さまざまな制約下での解を求める。CHRはチューリング完全だが、 独立した言語としてではなく既存言語の拡張機能として、主にPrologなどのホスト言語上に実装されたライブラリとして提供される。 CHRの特徴は以下の通りである。

• 頭部にゴール（制約）の多重集合が書ける
• 多重集合書換えに基づく言語の中では強力
• 多くの応用プログラムがある

CHRは単純化規則（Simplification rule）と伝播規則（Propagation rule）、およびそれらの組み合わせである単純化伝播規則（"Simpagation" rule）からなる。

単純化規則（Simplification rule）は、複数の制約を論理的に等価なより単純な制約に変換する。(例えば、X≦Y, Y≦X ⇔ X=Y. や X≦X ⇔ true.)

伝播規則（Propagation rule）は、論理的には冗長だが単純化に結び付くような制約を新しく追加する。(例えば、X≦Y, Y≦Z ⇒ X≦Z.)

関連項目

• 論理プログラミング
• 制約プログラミング
• 並行制約プログラミング
• 並行論理プログラミング
• 形式手法
• プログラミングパラダイム

参考文献

• Jaffar, J., and Maher, M.J., Constraint Logic Programming: A Survey. in Journal of Logic Programming, Volume 19/20, pp.503-581, 1994.
• Frühwirth T, et al. Constraint Logic Programming An Informal Introduction. Technical Report ECRC-93-5, ECRC. February 1993.
• 相場 亮, 制約論理プログラミングシステム. コンピュータソフトウェア, Vol.9, No.6 pp.461-473 1992.

外部リンク

• 制約プログラミングのページ