(57)【特許請求の範囲】
【請求項１】
制約および充足解の正しさの条件が、変数と定数の等号もしくは変数間の等号を原子とし、否定・連言・選言・含意の論理記号から構成される論理式でそれぞれ与えられ、さらにその制約を変換した解モデルの集合が与えられている場合における制約充足問題の正しさの検証をコンピュータを用いて行う方法であって、
当該コンピュータが、
入力装置から入力された充足解の正しさの条件を連言標準形の論理式に変換し、その論理式における節集合を記憶装置に出力して記憶させる変換ステップと、
入力装置から入力された解モデルの集合および記憶装置に記憶された節集合から全ての解モデルと全ての節に対する節の否定を含むリテラルの連言で表される新たな解モデルをそれぞれ作成して矛盾があるかどうかを調べ、矛盾していない新たな解モデルがあれば当該新たな解モデルの元になった解モデルを反例として制約が正しくないという結果を、また、全ての新たな解モデルが矛盾していれば制約が正しいという結果を表示装置に出力して表示する検査ステップとを実行する
ことを特徴とする制約充足の検証方法。
【請求項２】
請求項１に記載の制約充足の検証方法において、
前記検査ステップは、
入力装置から入力された解モデルの集合から解モデルを一つ取り出すとともに、記憶装置に記憶された節集合から節を一つ取り出し、これらから節の否定を含むリテラルの連言で表される新たな解モデルを一つ作成する第１のステップと、
前記作成した新たな解モデルが矛盾しているか否かを判定する第２のステップと、
前記判定結果が矛盾していなければ当該新たな解モデルの元になった解モデルを反例として制約が正しくないという結果を表示装置に出力して表示する第３のステップと、
前記判定結果が矛盾していれば取り出す解モデルまたは節を変えて第１および第２のステップを繰り返させる第４のステップと、
全ての新たな解モデルが矛盾しているという判定結果が得られたときに制約が正しいという結果を表示装置に出力して表示する第５のステップとを備える
ことを特徴とする制約充足の検証方法。
【請求項３】
コンピュータに、請求項１または２に記載の各ステップを実行させるためのプログラム。
【請求項４】
制約および充足解の正しさの条件が、変数と定数の等号もしくは変数間の等号を原子とし、否定・連言・選言・含意の論理記号から構成される論理式でそれぞれ与えられ、さらにその制約を変換した解モデルの集合が与えられている場合における制約充足問題の正しさの検証を行う装置であって、
入力装置および表示装置とともに、
連言標準形の論理式における節集合を記憶するための記憶装置と、
入力装置から入力された充足解の正しさの条件を連言標準形の論理式に変換し、その論理式における節集合を記憶装置に出力して記憶させる変換装置と、
入力装置から入力された解モデルの集合および記憶装置に記憶された節集合から全ての解モデルと全ての節に対する節の否定を含むリテラルの連言で表される新たな解モデルをそれぞれ作成して矛盾があるかどうかを調べ、矛盾していない新たな解モデルがあれば当該新たな解モデルの元になった解モデルを反例として制約が正しくないという結果を、また、全ての新たな解モデルが矛盾していれば制約が正しいという結果を表示装置に出力して表示する検査装置とを備える
ことを特徴とする制約充足の検証装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、人工知能の分野である制約充足を用いたソフトウェア開発におけるデバッグ技術に関する。
【背景技術】
【０００２】
制約充足は、変数の集合、各変数のドメイン（変域）の集合、および変数間の制約があったとき、制約を満たす変数の値の組み合せ（充足解）を自動的に求める技術である。様々な産業上の問題がこの制約充足技術で解決できることが知られている。つまり問題を変数の集合、ドメインの集合、制約という形式（制約充足問題）に定式化し、充足解を求めることで問題解決を行うことができる。このとき、制約は、一般的に論理式という形式で記述される。制約充足により問題解決を図る場合、前述したように制約充足問題に対して充足解は自動的に求めることができるため、人間は制約充足問題へ定式化する作業を行えば良い。この定式化において重要な点は、元の問題を忠実に制約充足問題として表現することである。制約充足問題が元の問題を忠実に表現していない場合、この制約充足問題から得られた充足解では元の問題の解決にならない可能性がある。
【０００３】
＜従来技術＞
上記の背景を踏まえ、制約充足問題が元の問題を忠実に表現していること（制約充足問題の正しさ）を検査する技術が既に提案されている。
【０００４】
この検査技術は現在、一般的に用いられている方法であり、制約充足問題から実際に充足解を求め、その充足解が元の問題の解決になり得ること（充足解の正しさ）を確認することで、制約充足問題の正しさを検査する方法である。しかし、制約充足問題における各変数のドメインのサイズが大きいと膨大な数の充足解が出力される場合があり、充足解の正しさを１つ１つ確認するのは不可能である。対策として、出力された充足解をサンプリングし、サンプリングされた充足解のみ正しさを確認する方法や、出力される充足解が少なくなるように調整されたテスト用のドメインで検査を行うこともできるが、この場合、検査の網羅性に欠け、厳密に制約充足問題の正しさを保証することはできない。
【０００５】
上記検査技術の問題点に対する解決策として、制約を解モデル集合に変換し、その解モデルの集合上で制約充足問題の正しさを確認する方法（非特許文献１）がある。解モデルは、充足解となる値の組み合わせのパターンを表現したものである。
【０００６】
例えば、変数ｘ，ｙ，ｚに対する制約（ｘ＝ｙ＝ｚ）∨（（ｘ＝６）∧（ｙ≠ｚ））が与えられた場合、解モデルの集合として２つの解モデル（ｘ，ｙ，ｚ）＝（｛α｝：：｛｝，｛α｝：：｛｝，｛α｝：：｛｝）および（ｘ，ｙ，ｚ）＝（｛６｝：：｛｝，｛α｝：：｛β｝，｛β｝：：｛α｝）が得られる。
【０００７】
解モデルにおける各変数の値は「肯定集合：：否定集合」という形式で記述され、肯定集合はその変数が取り得る値を表し、否定集合は取り得ない値を表す。例えば、前者の解モデルは、各変数の値の肯定集合は文字αを用いて「｛α｝」なので、ｘとｙとｚの値の等しい組み合わせが充足解であることを意味している。また、後者の解モデルの変数ｙとｚの否定集合はそれぞれ「｛β｝」，「｛α｝」となり、これらはそれぞれｚとｙの肯定集合なので、ｙとｚが等しくなくｘが６のときも充足解となることが読み取れる。
【０００８】
このように解モデルは、それが表現するパターンに合致する値の組み合わせの集合を意味している。これらの値の組み合わせで元の問題を解決することができるとき、解モデルが正しいと言う。解モデルの性質に「ある制約に対する充足解は、その制約から求めた各解モデルが表現するパターンのどれかに合致する」というものがある。従って、全ての解モデルが正しいことを確認することは、全ての充足解の正しさを確認するという網羅的な検査を実施することになる。このことから、制約から求めた全ての解モデルが正しいと判断できるとき、全ての充足解が正しい、即ち制約充足問題が正しいと厳密に判定することができる。但し、解モデルが正しいという判断に誤りがあった場合は、当然この限りではないことに注意されたい。
【０００９】
充足解の数は、各変数のドメインの要素数をＤ、変数の数をＮとしたとき、最悪ＤNとなる。一方、解モデルの数は、制約の論理式中の原子の数Ａに依存し、最悪２Aである。ドメインの要素数や変数の数が多く、制約の論理式の原子の数が少ない場合に全ての充足解の正しさを確認することは、充足解の数が膨大になるため、現実的には不可能である。それに対して解モデルの数は比較的に少ないため、全ての解モデルの正しさを確認することができる。
【非特許文献１】中島、大石、山村、「モデル生成にもとづく制約充足の検査手法」、人口知能学会第７３回知識ベースシステム研究会資料、ＳＩＧ−ＫＢＳ−Ａ５０４、ｐｐ．１３５−１４０、２００６
【発明の開示】
【発明が解決しようとする課題】
【００１０】
しかし、前述した解モデルを用いた制約充足問題の正しさを検査する方法では、解モデルの数が原子の数に対して指数関数的に増加するので、全ての解モデルの正しさを人手で確認するのに、大きなコストを要することが課題であった。
【課題を解決するための手段】
【００１１】
このため、本発明では、充足解の正しさの条件が論理式として与えられたとき、全ての充足解がその論理式を満たすことを、解モデルを使ってコンピュータで自動証明する。
【００１２】
今、制約充足問題における変数の集合が｛ν1，…，νn｝で与えられており、制約および充足解の正しさの条件が、変数と定数の等号もしくは変数間の等号を原子とし、否定（¬），連言（∧），選言（∨），含意（⇒）の論理記号から構成される論理式Ｃ（ν1，…，νn）およびＰ（ν1，…，νn）でそれぞれ与えられているものとする。
【００１３】
全ての充足解がその正しさの条件Ｐ（ν1，…，νn）を満たすことは、下記の述語論理式で表現することができる。
【００１４】
∀ν1…∀νn（Ｃ（ν1，…，νn）⇒Ｐ（ν1，…，νn））          …（１）
始めにこの論理式を証明するための方針を述べる。
【００１５】
（証明の方針）
制約Ｃ（ν1，…，νn）は下記のような選言標準形に変換が可能である。
【００１６】
ψ1（ν1，…，νn）∨ψ2（ν1，…，νn）∨…∨ψm（ν1，…，νn）
但し、ψi（ν1，…，νn）はリテラル、あるいはリテラルの連言である。リテラルとは原子、あるいは原子の否定のことであり、リテラルの連言とは２つ以上のリテラルを連言で結合した論理式のことである。今、原子は変数と定数の等号もしくは変数間の等号なので、例えばν1＝１，ν2＝ν3，ν4＝６が原子となる。この場合のリテラルは、それら原子自身と¬（ν1＝１），¬（ν2＝ν3），¬（ν4＝６）である。リテラルの連言は、例えば（ν1＝１）∧（ν2＝ν3），¬（ν1＝１）∧（ν2＝ν3）∧¬（ν4＝６）となる。ψi（ν1，…，νn）を単にψiと略記する場合もある。
【００１７】
一方、充足解の正しさの条件Ｐ（ν1，…，νn）は下記の連言標準形に変換が可能である。
【００１８】
φ1（ν1，…，νn）∧φ2（ν1，…，νn）∧…∧φl（ν1，…，νn）
但し、φi（ν1，…，νn）を節と呼び、リテラル、あるいはリテラルの選言である。リテラルの選言とは、２つ以上のリテラルを選言で結合した論理式のことである。例えば（ν1＝１）∨（ν2＝ν3），¬（ν1＝１）∨（ν2＝ν3）∨¬（ν4＝６）となる。φi（ν1，…，νn）を単にφiと略記する場合もある。
【００１９】
（１）の論理式で制約Ｃ（ν1，…，νn）を選言標準形に、充足解の正しさの条件Ｐ（ν1，…，νn）を連言標準形にそれぞれ置き換えると、下記のように変形できる。
【００２０】
∀ν1…∀νn（（ψ1∨…∨ψm）⇒（φ1∧…∧φl））
⇔  ∀ν1…∀νn（¬（ψ1∨…∨ψm）∨（φ1∧…∧φl））
⇔  ∀ν1…∀νn（（¬ψ1∧…∧¬ψm）∨（φ1∧…∧φl））
⇔  ∀ν1…∀νn（（¬ψ1∨（φ1∧…∧φl））∧…∧（¬ψm∨（φ1∧…∧φl）））
⇔  ∀ν1…∀νn（¬ψ1∨（φ1∧…∧φl））∧…∧∀ν1…∀νn（¬ψm∨（φ1∧…∧φl））
よって、１≦ｉ≦ｍの各ψi（ν1，…，νn）に対して下記の式が証明できれば、（１）の論理式を証明したことになる。
【００２１】
∀ν1…∀νn（¬ψi（ν1，…，νn）∨（φ1（ν1，…，νn）∧…∧φl（ν1，…，νn）））                                                          …（２）
（２）の論理式をさらに下記のように変形する。
【００２２】
∀ν1…∀νn（¬ψi∨（φ1∧…∧φl））
⇔  ∀ν1…∀νn（（¬ψi∨φ1）∧…∧（¬ψi∨φl））
⇔  ∀ν1…∀νn（¬ψi∨φ1）∧…∧∀ν1…∀νn（¬ψi∨φl）
⇔  ∀ν1…∀νn（（ψi∧¬φ1）⇒⊥）∧…∧∀ν1…∀νn（（ψi∧¬φl）⇒⊥）
なお、⊥は偽（矛盾）であることを表す。ここで、（ψi∧¬φ1），…，（ψi∧¬φl）はリテラルの連言で表現されることに注意されたい。リテラルをＬとしたとき、φjはＬあるいはリテラルの選言Ｌ1∨Ｌ2∨…で表現されるので、¬φjはリテラル¬Ｌあるいはリテラルの連言¬Ｌ1∧¬Ｌ2∧…で表現される。ψiはリテラルあるいはリテラルの連言なので、ψiと¬φjの連言はリテラルの連言になる。つまり（２）を証明するためには、リテラルの連言で表現される（ψi∧¬φ1），…，（ψi∧¬φl）が、全て矛盾になることを証明すれば良い。
【００２３】
非特許文献１によれば、解モデルは、リテラルの連言で表現される論理式から生成することができる。この論理式が矛盾となるならば、生成される解モデルも矛盾になる。解モデルが矛盾であるとは、以下の条件のどちらかを解モデルが満たすときに言う。
【００２４】
●解モデルの値において、その肯定集合の要素が２つ以上の定数から構成されるものが存在する。例えば、制約（ν1＝５）∧（ν1＝３）に対する解モデル（ν1）＝（｛５，３｝：：｛｝）は矛盾である。
【００２５】
●解モデルの値において、その肯定集合と否定集合に共通の要素を含むものが存在する。例えば、制約（ν1＝ν2）∧¬（ν1＝ν2）に対する解モデル（ν1，ν2）＝（｛α｝：：｛α｝，｛α｝：：｛α｝）は矛盾である。
【００２６】
よって、（ψi∧¬φ1），…，（ψi∧¬φl）から解モデルを作成し、その解モデルの全てが矛盾であれば、（２）が証明できたことになる。さらに、制約の選言標準形ψ1∨…∨ψmにおける各リテラルおよびリテラルの連言ψ1，…，ψmに対してこの方法で（２）を証明すれば、（１）を証明したことになる。このようにして、全ての充足解が正しさの条件を満たすことを証明することが可能になる。
【００２７】
（自動証明の方法）
非特許文献１の検査方法を実施して、既に制約Ｃ（ν1，…，νn）に対する解モデルの集合Ｓが得られているとき、その集合の要素の解モデルｓiは、Ｃ（ν1，…，νn）を選言標準形ψ1∨…∨ψmに変換した際の各ψiから求めたものである。解モデルの集合Ｓと充足解の正しさの条件Ｐ（ν1，…，νn）が与えられる場合に、コンピュータを用いて（１）の自動証明を行う方法を図１，２に従って説明する。
【００２８】
まず、図１；ｓ１の入力ステップにおいて、解モデルの集合Ｓと充足解の正しさの条件Ｐ（ν1，…，νn）が入力装置からコンピュータに入力される。次に、図１；ｓ２の変換ステップにおいて、Ｐ（ν1，…，νn）を連言標準形φ1∧φ2∧…∧φlに変換する。この変換を自動的に行う既知のアルゴリズムは存在する。そして、この変換で得られる節集合｛φ1，φ2，…，φl｝を記憶装置に書き込む。
【００２９】
次に、図１；ｓ３の検査ステップにおいて、全てのψiと全てのφjに対してψi∧¬φjの解モデルをそれぞれ作成し、全て矛盾しているかどうか調べ、その結果を表示装置に出力して表示する。このとき、既にψiに対する解モデルｓiが作成され入力されているので、ｓiの解モデルに差分である¬φjを反映させて、ψi∧¬φjの解モデルを求める。
【００３０】
この検査ステップを具体的に示したものが図２である。ここでは、まず解モデルの集合Ｓから解モデルを１つ取り出す（図２；ｓ３１）。取り出した解モデルをｓiとする。次に記憶装置の節集合｛φ1，φ2，…，φl｝をコピーし、コピーした集合をΦとする（図２；ｓ３２）。さらに、Φから要素を１つ取り出し、取り出した要素をφjとする（図２；ｓ３３）。これら解モデルｓiとφjから新しい解モデルを作成する（図２；ｓ３４）。この処理は、非特許文献１における図１のアルゴリズムを利用して求めることができる。つまり、非特許文献１における図１の２行目における初期の解モデルＭgをｓiとする。さらにφjに含まれるリテラルの集合を｛Ｌ1，Ｌ2，…｝とすると、その否定からなる集合｛¬Ｌ1，¬Ｌ2，…｝を非特許文献１における図１の１行目のＬの初期値として与えることで、ψi∧¬φjの解モデルを得ることが可能になる。
【００３１】
このようにして作成された解モデルが矛盾であるかを判定し（図２；ｓ３５）、矛盾でなければ（１）を満たさないことになるので、Ｆａｌｓｅという結果と解モデルｓjを表示装置に出力して表示する（図２；ｓ３８）。作成された解モデルが矛盾である場合は、Φが空集合であるかを判定し（図２；ｓ３６）、空集合になるまで図２のｓ３３からｓ３５の処理を繰り返す。Φが空集合である場合は、解モデルの集合Ｓ中の全ての解モデルに対して処理を行ったかを判定し（図２；ｓ３７）、行っていなければ残りの解モデルに対しても図２のｓ３１からｓ３６の処理を行い、全ての解モデルに対して処理を行っていればＴｒｕｅという結果を表示装置に出力して表示する（図２；ｓ３９）。
【００３２】
図２のｓ３８で出力される解モデルｓjのことを反例と呼ぶ。反例とは充足解の正しさの条件Ｐ（ν1，…，νn）を満たさない具体例のことである。この場合、ｓjが表すパターンに合致する充足解の中に、Ｐ（ν1，…，νn）を満たさないものが含まれていることになる。このような反例を元に、制約の誤りを修正することが可能になる。
【００３３】
本発明は、単に制約充足問題の正しさを検査して正しいあるいは正しくないという結果を返すだけでなく、制約の誤りを修正するときに有益な情報源となる反例を導出できる点が特徴の１つである。
【発明の効果】
【００３４】
本発明によれば、制約充足問題の正しさを解モデルによって検査する場合に、「制約に対する全ての充足解が与えられた充足解の正しさの条件を満たす」ことを自動的に証明可能になり、人手で解モデルを確認する労力を削減することができる。
【発明を実施するための最良の形態】
【００３５】
図３は本発明の制約充足の検証方法を実施する装置の実施の形態の一例、ここでは周知のコンピュータ上に実現した例を示すもので、図中、１は入力装置、２は表示装置、３はコンピュータである。
【００３６】
入力装置１は、キーボード、マウス等からなり、ユーザがコンピュータ３に所定の情報、ここでは解モデルの集合、および充足解の正しさの条件を入力するためのものである。表示装置２は、液晶ディスプレイ、ＣＲＴ等の画像表示装置からなり、コンピュータ３の所定の処理結果、ここでは検査結果をユーザに提示するためのものである。
【００３７】
コンピュータ３は、図１乃至図２に示した処理フローに対応する所定のプログラムに従い、各装置を制御するとともに、この際、記憶装置４、変換装置５および検査装置６を構成する。
【００３８】
記憶装置４は、変換装置５によって得られる節集合を記憶する。
【００３９】
変換装置５は、図１；ｓ２の処理を行い、入力装置１から入力された充足解の正しさの条件の論理式Ｐ（ν1，…，νn）を連言標準形φ1∧φ2∧…∧φlに変換し、節集合｛φ1，φ2，…，φl｝を記憶装置４に出力して記憶させる。
【００４０】
検査装置６は、入力装置１から入力された解モデルの集合および記憶装置４に記憶された節集合から、図１；ｓ３、つまり図２に示したフローの各処理を行い、検査結果を表示装置２に出力して表示する。
【００４１】
本装置により、制約充足問題の正しさを解モデルによって検査する場合に、「制約に対する全ての充足解が与えられた充足解の正しさの条件を満たす」ことを自動的に証明可能になる。
【００４２】
なお、前述した実施形態では、記憶装置４、変換装置５および検査装置６をコンピュータ上で実現した例を示したが、ハードウェアで実現しても良い。またこれら各装置が、適切な通信路で相互に接続された複数のハードウェア上に分散して存在し、相互に通信し合いながら実行することもできる。
【実施例１】
【００４３】
本発明による制約の誤り検出について例を挙げて説明する。
【００４４】
ユーザが制約「（ｘ＝ｙ＝ｚ）∨（（ｘ＝６）∧（ｙ≠ｚ））」の２つの解モデルからなる集合「（ｘ，ｙ，ｚ）＝（｛α｝：：｛｝，｛α｝：：｛｝，｛α｝：：｛｝），（｛６｝：：｛｝，｛α｝：：｛β｝，｛β｝：：｛α｝）」を入力し、さらに充足解の正しさ条件として（ｘ＝６）∨（¬（ｘ＝ｙ））を入力装置１から入力する。
【００４５】
コンピュータ３は図１のフローに従って、始めに変換装置５において図１；ｓ２の処理を行う。これによって記憶装置４には、節（ｘ＝６）∨（¬（ｘ＝ｙ））が記憶される。
【００４６】
次に、コンピュータ３は検査装置６において、図１；ｓ３、つまり図２のフローの処理を行う。本実施例では、解モデルとして（ｘ，ｙ，ｚ）＝（｛α｝：：｛｝，｛α｝：：｛｝，｛α｝：：｛｝）と（ｘ，ｙ，ｚ）＝（｛６｝：：｛｝，｛α｝：：｛β｝，｛β｝：：｛α｝）があるので、図２；ｓ３１乃至ｓ３４の処理で、始めに前者の解モデルと節（ｘ＝６）∨（¬（ｘ＝ｙ））から解モデルを作成する。このとき、作成される解モデルは、（ｘ，ｙ，ｚ）＝（｛α｝：：｛６｝，｛α｝：：｛６｝，｛α｝：：｛６｝）であり、図２；ｓ３５の処理の結果、矛盾ではないと判定される。よって図２；ｓ３８の処理で、Ｆａｌｓｅという結果と反例（ｘ，ｙ，ｚ）＝（｛α｝：：｛｝，｛α｝：：｛｝，｛α｝：：｛｝）が表示装置２に出力され、ユーザに提示（表示）される。
【図面の簡単な説明】
【００４７】
【図１】本発明の制約充足の検証方法全体の処理フローを示す図
【図２】検査工程の詳細な処理フローの一例を示す図
【図３】本発明の制約充足の検証装置の実施の形態の一例を示す構成図
【符号の説明】
【００４８】
１：入力装置、２：表示装置、３：コンピュータ、４：記憶装置、５：変換装置、６：検査装置。
【図１】
0004963445.tif 000002
【図２】
0004963445.tif 000003
【図３】
0004963445.tif 000004