(57)【要約】【課題】制約充足における制約が、変数と定数との間の等号もしくは変数と変数との間の等号を原子とし、命題論理記号からなる論理式で与えられた場合において、変数の集合及び制約の集合のみを入力として実施可能で、かつ網羅性が保証された制約充足の試験を実現すること。【解決手段】入力装置から入力された制約の集合を等価な選言標準形の論理式に変換し（ｓ１１，ｓ１２）、入力装置から入力された変数の集合とともに、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求め（ｓ１１，ｓ１３，ｓ１４）、解モデルデータベースに出力して記憶させ（ｓ１５，ｓ１６）、入力装置から入力された検索条件で解モデルデータベースを検索し、その結果の解モデルを表示装置に表示する（ｓ１７，ｓ１８）。【選択図】図１
2007241491.tif 000002
【特許請求の範囲】
【請求項１】
制約が、変数と定数との間の等号もしくは変数と変数との間の等号を原子とし、命題論理記号からなる論理式で与えられた場合における制約充足の試験をコンピュータを用いて行う方法であって、
当該コンピュータが、
入力装置から入力された制約の集合を等価な選言標準形の論理式に変換し、入力装置から入力された変数の集合とともに、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求め、解モデルデータベースに出力して記憶させる解モデル出力処理ステップと、
入力装置から入力された検索条件で解モデルデータベースを検索し、その結果の解モデルを表示装置に表示する検索表示処理ステップとを実行する
ことを特徴とする制約充足の試験方法。
【請求項２】
解モデル出力処理ステップは、
入力装置から入力された制約の集合を等価な選言標準形の論理式に変換するステップと、
入力装置から入力された変数の集合から解モデルの初期値を作成し、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求めるステップと、
求めた解モデルを整形処理するステップと、
整形後の解モデルを解モデルデータベースに出力して記憶させるステップとを備える
ことを特徴とする請求項１記載の制約充足の試験方法。
【請求項３】
制約が、変数と定数との間の等号もしくは変数と変数との間の等号を原子とし、命題論理記号からなる論理式で与えられた場合における制約充足の試験装置であって、
入力装置及び表示装置とともに、
解モデルを記憶するための解モデルデータベースと、
入力装置から入力された制約の集合を等価な選言標準形の論理式に変換し、入力装置から入力された変数の集合とともに、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求め、解モデルデータベースに出力して記憶させる解モデル出力処理装置と、
入力装置から入力された検索条件で解モデルデータベースを検索し、その結果の解モデルを表示装置に表示する検索表示処理装置とを備える
ことを特徴とする制約充足の試験装置。
【請求項４】
解モデル出力処理装置は、
入力装置から入力された制約の集合を等価な選言標準形の論理式に変換するＤＮＦ変換手段と、
入力装置から入力された変数の集合から解モデルの初期値を作成し、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求める解モデル出力手段と、
求めた解モデルを整形処理する整形手段と、
整形後の解モデルを解モデルデータベースに出力して記憶させるＤＢ出力手段とを備える
ことを特徴とする請求項３記載の制約充足の試験装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、人工知能の分野である制約充足を用いたソフトウェア開発の試験技術に関する。
【背景技術】
【０００２】
制約充足は、解決したい問題を変数の集合、各変数の値の集合（ドメイン）及び変数間の制約の集合という形で定式化し、制約を満たす変数の値の組み合わせを求める技術である。制約充足の特徴は、問題を正しく定式化できれば、処理手続きを与えずとも正しい解を出力できることにある。従って、正しい解を得るためには、定式化が問題を正しく表現していることを確認する必要がある。しかし、解決したい問題が複雑な場合、制約の数も多くなり複雑になるため、その確認は容易ではない。
【０００３】
この種の従来の試験技術である、制約型問題解決システム（特許文献１参照）、Ｅｘｐｌａｎａｔｉｏｎ  Ｓｏｌｖｅｒ（非特許文献１参照）、宣言的デバッグシステム（非特許文献２参照）はいずれも、変数の集合、制約の集合及び各変数に対するドメインを入力し、充足解を出力させ確認を行うものであった。
【特許文献１】特開平５−２１６６７５号公報
【非特許文献１】N.Jussien, V.Barichard "The PaLM system: explanation-based constraint programming", Proc. of Techniques for Implementing Constraint Programming System, 2000
【非特許文献２】L.Naish "A Declarative Debugging Scheme", The Journal of Functional and Logic Programming, 1997
【非特許文献３】田山、山村「制約充足アプローチによる運用多様化に対応した設備選定アルゴリズムの提案」信学技報、Vol.１３０、No.５７３、２００４年、pp.８５〜９０
【発明の開示】
【発明が解決しようとする課題】
【０００４】
しかし、前述した従来の試験方法では、ドメインが与えられない場合には試験を行うことできず、制約の集合が正しいことを変数の集合及び制約の集合のみから試験することが不可能であった。そのため、ドメインの入力処理部分（のプログラム）の開発が、変数及び制約の入力処理部分（のプログラム）の開発より遅れると、その開発が終わるまで試験を行うことができず、開発期間の長期化を招くことになる。
【０００５】
さらに、従来の試験方法では、テスト用のドメインで充足解が多数出力された場合、それらを個別に確認し、正しい解のみ出力されているか否かを確認することが困難であった。対策として、出力された解をサンプリングし、サンプリングされた解のみ確認する方法や、出力される解が少なくなるように調整されたテスト用のドメインを入力して試験を行う方法もあるが、この場合、試験の網羅性に欠け、誤りを発見できなくなる可能性が高くなるという問題があった。また従来の試験方法では、テスト用のドメインで出力された充足解が全て正しいことを確認できたとしても、テスト用ではない別のドメインのもとで正しい充足解が出力される保証を得ることができなかった。
【０００６】
このため、本発明では、制約充足における制約が、変数と定数との間の等号もしくは変数と変数との間の等号を原子とし、命題論理記号からなる論理式で与えられた場合において、変数の集合及び制約の集合のみを入力として実施可能で、かつ網羅性が保証された制約充足の試験を実現することを目的とする。
【課題を解決するための手段】
【０００７】
上記目的を達成するために、本発明では、充足解を包含した解モデルを出力する処理を具備し、変数の集合及び制約の集合のみの入力で解モデルの出力を可能とし、充足解ではなく解モデルを確認することで網羅性が保証された試験を可能とする。
【０００８】
解モデルとは、変数と定数との間の等号もしくは変数と変数との間の等号を原子とし、論理記号の連言と否定からなる論理式を満たす変数の値の組み合わせを記号の組み合わせで表現したものである。但し、対象とする論理式の中で原子の否定は許されるが、原子以外の論理式を否定することは許されない。このような論理式を解モデルが出力可能な論理式と呼ぶ。以下に解モデルを出力可能な論理式と出力できない論理式の例を挙げる。
【０００９】
●出力可能な論理式  （ｘ＝１）∧¬（ｙ＝ｘ）
●出力できない論理式  ¬（（ｘ＝１）∧（ｙ＝ｘ））
上記の２つの論理式の原子はともにｘ＝１とｙ＝ｘであり、論理記号の連言と否定からなっている。しかし、後者の論理式を対象としないのは、前者の論理式においてはｙ＝ｘという原子を否定しているのに対して、後者は（ｘ＝１）∧（ｙ＝ｘ）という原子ではない論理式を否定しているためである。
【００１０】
解モデルの例として、変数ｘ，ｙ，ｚに対し、制約としてｚ＝５∧ｘ＝ｙという論理式が与えられている場合を考える。この場合、制約を満たすｘ，ｙ，ｚの値の組み合わせとしては、（ｘ，ｙ，ｚ）＝（１，１，５），（２，２，５），…（ａ，ａ，５），（ＮＵＬＬ，ＮＵＬＬ，５）など、ｚの値が５であり、かつｘとｙの値が等しいものが挙げられる。但し、これらの全てが制約充足の充足解となり得るわけではなく、充足解は変数のドメインを考慮して求められる。つまり、ｘ，ｙのドメインが整数の場合は（ａ，ａ，５）や（ＮＵＬＬ，ＮＵＬＬ，５）のような解は充足解とはならない。解モデルは、そのような変数のドメインの条件がなかった場合の制約を満たす値の組み合わせを表現する。
【００１１】
つまり、ｘとｙの値を変数αや□等で表し、ｚを５とした（α，α，５）や（□，□，５）がこの場合の解モデルとなる。解モデル中の変数は制約充足の変数とは異なるので注意されたい。
【００１２】
このようにすることで、解モデルから充足解の可能性がある値の組み合わせを類推することができる。つまり、解モデル中の変数には何らかの値が代入できるので、例えば（α，α，５）の場合は、（１，１，５）や（２，２，５）等、αに適当な値を代入したものが充足解となることが容易に類推できる。解モデル中の制約充足の変数に対応する値を値モデルと呼ぶ。例えば、制約充足の変数ｘ，ｙに対して解モデル（ｘ，ｙ）＝（α，β）の場合、α，βがそれぞれｘ，ｙの値モデルとなる。値モデル中の変数は、制約充足の変数と区別して、これ以降ではギリシャ文字を用いることとする。
【００１３】
前述したように、解モデルを出力可能な論理式は原子及び原子の否定を連言とした論理式なので、原子及び原子の否定をリテラルと呼び、Ｌi（１≦ｉ≦ｎ）で表すと、一般的には下記のように表現できる。
【００１４】
Ｌ1∧Ｌ2∧…∧Ｌn-1∧Ｌn
解モデル中の値モデルはリテラルの内容に応じて決定する。先にも述べたようにリテラルに変数と定数との間の等号の原子がある場合は、その変数の値モデルは定数で表現され、変数間の等号の原子の場合は、両変数の値モデルは等しい変数で表現される。
【００１５】
しかし、原子の否定、つまり変数と定数が等しくない、あるいは変数間が等しくないというリテラルに対して値モデルをうまく定めることができない。これは今まで説明してきた値モデルがある値をとらないといったことを表現できないためである。従って、原子の否定に対して値モデルをうまく定めるには「値がαでない」なども表現できる必要がある。また、これまでの値モデルは１つの変数もしくは定数で表されてきたが、それでは¬（ｘ＝５）∧¬（ｘ＝３）のような「値が５でなく、かつ３でない」ことを表現できない。そこで、これ以降の値モデルは２つの変数と定数の集合、肯定集合と否定集合の組み合わせで表現されるものとする。
【００１６】
肯定集合の要素はこれまでと同様、その値モデルと対応する制約充足の変数が充足解としてとるべき値を意味する。例えば「５」という定数が肯定集合の要素の場合、「値が５である」ことを表している。否定集合の要素は、その制約充足の変数が充足解として取り得ない値を意味し、「５」という定数が否定集合の要素の場合、「値が５でない」ことを表すものとする。
【００１７】
制約が（ｘ＝ｙ）∧¬（ｙ＝ｚ）∧（ｚ＝３）の場合の解モデルは、値モデルを「肯定集合::否定集合」と書く場合、（ｘ，ｙ，ｚ）＝（｛α｝::｛３｝，｛α｝::｛３｝，｛３｝::｛α｝）が解モデルとなる。
【００１８】
上記までの解モデルは解モデルが出力可能な論理式を対象としてきたが、入力される制約は、命題論理記号のあらゆる組み合わせが可能なので、連言・選言や含意、それに否定などの自由な組み合わせが記述される。そのような制約の集合と変数の集合とをコンピュータに入力して解モデルを求める処理のフローを図１、図２、図３、図４に示す。
【００１９】
まず、入力装置から入力された制約の集合（図１；ｓ１１）について、それらの要素である論理式の連言を論理式Ｓとした場合、Ｓを選言標準形ＳDNFに変換する（図１；ｓ１２）。ＳDNFは原子とその否定の連言からなる項の選言の形をした論理式になる。つまりＳDNFを連言項ｇの集合Ｇで表現すると下記のように表現できる。
【００２０】
【数１】
2007241491.tif 000003
任意の命題論理式に対して選言標準形は必ず一意に決まり、Ｓも原子を原子命題とする命題論理式と考えられるので、Ｓは必ずＳDNFに変換可能である。また連言項ｇはリテラルの連言の論理式なので、解モデルが出力可能である。つまり、各連言項ｇに対してそれぞれ解モデルを求めれば良い。
【００２１】
上記で表現されるｇの解モデルの導出処理を述べる（図１；ｓ１３、図２）。始めに解モデルの値モデル（初期値）を下記のように置く（図２；ｓ２１）。
【００２２】
●肯定集合…全ての値モデルで要素数を１とする。またその要素は、各値モデルの肯定集合の要素間で異なる変数を置く。
【００２３】
●否定集合…一様に空集合とする。
【００２４】
例えば、変数がｘ，ｙ，ｚの場合、それぞれの値モデルの肯定集合は｛α｝，｛β｝，｛γ｝とし、否定集合は一様に空集合としたものを解モデルの初期値とする。
【００２５】
次に、ｇに出現する各リテラルの種類に応じて（図２；ｓ２２，ｓ２３）以下の処理を行い、解モデルを更新していく。
【００２６】
●リテラルが「変数＝定数」の場合（図２；ｓ２４）、変数に対応する値モデルの肯定集合の要素数で場合分けをする（図３；ｓ３１）。
【００２７】
◇変数に対応する値モデルの肯定集合の要素数が１の場合、その要素が定数かそうでないか（変数か）で場合分けを行う（図３；ｓ３２）。
【００２８】
☆定数である場合（図３；ｓ３３）は、初期値としておいた肯定集合の要素の変数にその定数が既に代入された状態である。従って、リテラルの定数をリテラルの変数と対応する値モデルの肯定集合に加える。尚、このとき、加えた定数と元々の肯定集合の要素の定数が異なる場合は、更新後の肯定集合の要素数は２となり、これはｇに充足解が存在しないことを意味する。
【００２９】
☆定数でない場合（図３；ｓ３４）、リテラルはまだ値が決まっていない変数を定数で置き換えることを意味するので、肯定集合の変数をリテラルの定数で置き換える。このとき、対象としている肯定集合中の変数だけを置き換えるのではなく、解モデル中の他の部分にその変数が出現しているならそれらも定数で置き換える。
【００３０】
◇変数に対応する値モデルの肯定集合の要素数が１でない場合、上記理由により既にこのｇでは充足解が存在しないことが判明しているので、特に処理を行わない。
【００３１】
●リテラルが「¬（変数＝定数）」の場合（図２；ｓ２５）、変数と対応する値モデルの否定集合に定数を加える。
【００３２】
●リテラルが「変数＝変数」の場合（図２；ｓ２６）は、両辺の変数に対応する値モデルの肯定集合を共通のものにする処理を行う。まず両変数に対応する値モデルの肯定集合の要素数で場合分けをする（図４；ｓ４１）。
【００３３】
◇両変数に対応する値モデルの肯定集合の要素数が１の場合、さらに両変数に対応する値モデルの肯定集合の要素の種類で場合分けをする（図４；ｓ４２）。
【００３４】
☆両変数の肯定集合の要素が共に定数だった場合は、それぞれの肯定集合の和を新しい肯定集合とする（図４；ｓ４３）。
【００３５】
☆一方の変数の肯定集合の要素が変数で他方が定数の場合は、解モデル中に出現するその変数を定数で置き換える（図４；ｓ４４）。
【００３６】
☆両方の肯定集合の要素が変数の場合は、解モデル中に出現する一方の変数を他方の変数で全て置き換える（図４；ｓ４５）。
【００３７】
◇どちらかの変数に対応する値モデルの肯定集合の要素数が１でない場合、上記理由により既にこのｇでは充足解が存在しないことが判明しているので、特に処理を行わない。
【００３８】
●リテラルが「¬（変数＝変数）」の場合（図２；ｓ２７）、両変数は異なる値を持つ必要があるので、右辺の変数に対応する値モデルの肯定集合の要素を左辺の変数に対応する値モデルの否定集合に加える。さらに左辺の変数に対しても同様の処理、つまり左辺の変数に対応する値モデルの肯定集合の要素を右辺の変数に対応する値モデルの否定集合に加える処理を行う。
【００３９】
これらの処理を全てのリテラルに対して行い解モデルを求める（図２；ｓ２８）。上記処理によって求められる解モデルは、ｇを満たす充足解が存在しない場合は、解モデルの値モデル中に肯定集合の要素数が２のものが存在するか、肯定集合と否定集合の共通部分が存在するものになる。このような解モデルを「矛盾を意味する解モデル」と呼ぶ。また充足解が存在して、ｇに変数間が等しいという制約がある場合の解モデルは、それらの変数に対応する値モデルの肯定集合が等しくなる。逆に変数間が等しくない制約がある場合の解モデルは、両変数の値モデルに対して、一方の変数の値モデルの肯定集合の要素が他方の変数の値モデルの否定集合に存在している。
【００４０】
最後に見易さの観点から整形処理を行って解モデルとする（図１；ｓ１４）。以下に整形処理の例を挙げる。
【００４１】
●上記処理のみでは、変数間が等しいという制約がリテラル中にあった場合、その変数に対応する値モデルが常に等しいとは限らない（但し、値モデル中の肯定集合はｇに矛盾がなければ必ず等しい）。具体例で述べると、ｇのリテラルの集合が｛α＝ｂ，¬（ｂ＝１）｝だったとき（α，ｂは変数）の整形処理前の解モデルは、値モデルを「肯定集合::否定集合」と書くと、（ａ，ｂ）＝（｛α｝::｛１｝，｛α｝::｛１｝）ではなく、（α，ｂ）＝（｛α｝::｛｝，｛α｝::｛１｝）というａ，ｂの値モデルが異なる解モデルを出力する。肯定集合を比較すれば、ａ＝ｂであることがわかるのだが、値モデルは等しくないためａ＝ｂではないと勘違いさせる可能性がある。その場合は、肯定集合の等しい値モデルらの否定集合の和集合をそれら値モデルの否定集合とする変形処理を行うことで、前者の解モデルを出力できる。
【００４２】
●リテラルの集合に出現しなかった変数は充足解において自由な値の組み合わせが許される。そこで、そのような変数は他の変数と関係がないことを明確化するため、例えば“−”など特殊な記号で変数の値モデルを置き換える。
【００４３】
上記のような処理によって求められた解モデルは、所定のデータベース、例えば解モデルデータベースに出力され記憶される（図１；ｓ１５）。連言項の集合Ｇの全ての要素それぞれに対して解モデルを求め（図１；ｓ１６）、検索表示処理を行う。即ち、入力装置から入力された値モデルの検索条件（図１；ｓ１７）で解モデルデータベースを検索し、検索条件に見合う解モデルを表示装置に表示する（図１；ｓ１８）。検索機能（検索条件）としては次のものを備える。
【００４４】
●全解モデル表示
●矛盾となる値モデルを含まない解モデルの表示
●矛盾となる値モデルを含む解モデルの表示
●値モデルに条件を与えそれを満たす値モデルを含む解モデルの表示
●変数を与え解モデル中のその変数に対応する値モデルの表示
従来の試験方法では、例えば、テスト用の変数のドメインを与えて充足解が得られなかった場合、制約に矛盾があるために充足解がないのか、それともテスト用のドメインでたまたま充足解がなかったのか判定できなかった。しかし、本発明の解モデルでは論理式に矛盾があろうとなかろうと解モデルを導出でき、前述のように肯定集合の要素数もしくは肯定集合と否定集合の共通部分を調べれば矛盾を意味する解モデルを容易に判別できる。また、テストで充足解が得られてもその個数が少ないと、変数のドメインを変更した場合にどのような充足解が得られるのか類推できない。充足解が多数になってしまうと、一つ一つ正しい充足解なのか確認するのが困難である。しかし、本発明では充足解は必ず解モデルのいずれかと対応がとれ、解モデルの個数は高々連言項の個数であるため、解モデルをチェックすれば網羅的な試験が可能である。
【発明の効果】
【００４５】
本発明により、制約充足を用いたシステム開発において、変数のドメインを与えなくとも変数と制約のみから試験を行うことが可能となり、試験を早期に実施できるため開発期間の短縮効果を生じる。また、充足解は必ず解モデルと対応がとれることから、連言項と等しい数の解モデルを全て検査すれば網羅的な試験が可能となり、誤りのないシステムを開発し易くなる効果を生じる。
【発明を実施するための最良の形態】
【００４６】
図５は本発明の制約充足の試験方法を実施する装置の実施の形態の一例、ここでは周知のコンピュータ上に実現した例を示すもので、図中、１は入力装置、２は表示装置、３はコンピュータである。
【００４７】
入力装置１は、キーボード、マウス等からなり、オペレータ（検査者）がコンピュータ３に所定の情報、ここでは変数の集合及び制約の集合とともに検索条件を入力するためのものである。表示装置２は、液晶ディスプレイ、ＣＲＴ等の画像表示装置からなり、コンピュータ３における所定の処理結果、ここでは検索条件に合致した解モデルをオペレータに提示するためのものである。
【００４８】
コンピュータ３は、図１乃至図４に示した処理フローに対応する所定のプログラムに従って各部を制御するとともに、この際、解モデルデータベース４、解モデル出力処理部（装置）５及び検索表示処理部（装置）６を構成する。
【００４９】
解モデルデータベース４は、ハードディスク等の記憶装置からなり、解モデル出力処理部５によって得られる解モデルを記憶する。
【００５０】
解モデル出力処理部５は、ＤＮＦ変換手段（モジュール）５１、解モデル出力手段（モジュール）５２、整形手段（モジュール）５３、データベース（ＤＢ）出力手段（モジュール）５４及び制御手段（モジュール）５５を備え、図１に示した処理フローのステップｓ１１からステップｓ１６までに対応する機能、即ち入力装置１から入力された制約の集合を等価な選言標準形の論理式に変換し、入力装置１から入力された変数の集合とともに、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求め、解モデルデータベース４に出力して記憶させる機能を有する。
【００５１】
詳細には、ＤＮＦ変換手段５１は、入力装置１から入力された制約の集合を等価な選言標準形の論理式に変換する。解モデル出力手段５２は、入力装置１から入力された変数の集合から解モデルの初期値を作成し、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求める。整形手段５３は、前記求めた解モデルを整形処理する。ＤＢ出力手段５４は、整形後の解モデルを解モデルデータベース４に出力して記憶させる。制御手段５５は、前述した各手段（モジュール）における動作を、図１に示した処理フローに従い管理・制御する。
【００５２】
検索表示処理部６は、図１に示した処理フローのステップｓ１７からステップｓ１８までに対応する機能、即ち入力装置１から入力された検索条件で解モデルデータベース４を検索し、その結果の解モデルを表示装置２に表示する機能を有する。
【００５３】
本装置により、制約が、変数と定数との間の等号もしくは変数と変数との間の等号を原子とし、命題論理記号からなる論理式で表現される場合に限り、変数の集合及び制約の集合のみで制約充足の定式化の試験を行うことが可能になる。
【００５４】
なお、前述した実施の形態では、解モデルデータベース、解モデル出力処理装置及び検索表示処理装置をコンピュータ上で実現した例を示したが、それぞれハードウェアで構成しても良いことはいうまでもない。また、請求項及び実施の形態において、変数の集合及び制約の集合や検索条件を入力装置から入力するとしたが、この点については、これらの情報を通信媒体を介して他の装置から入力する、あるいは、予めこれらの情報を入力装置もしくは通信媒体を介して他の装置から入力して記憶媒体に記憶しておき、これを読み出して入力する場合も含まれるものとする。
【実施例】
【００５５】
以下、本発明による制約充足の試験について具体的な問題、ここでは非特許文献３に記載された「光ファイバを利用するサービスを提供するために設備を割当てる（選定する）問題（正確には、その一部改変した問題）」を例に挙げて説明する。
【００５６】
前記問題の制約充足の定式化の変数及び制約は下記のようなものである。
１．変数
・ユーザ情報…Ｕａ，Ｕｂ，Ｔ，Ｃ
・所外ファイバ…Ｏａ，Ｏｂ，Ｏｃ，Ｏｄ
・所内ファイバ（所内側）…Ｉｏａ，Ｉｏｂ，Ｉｏｃ，Ｉｏｄ，Ｉｏｅ，Ｉｏｆ，Ｉｏｇ，Ｉｏｈ
・所内ファイバ（装置側）…Ｉｅａ，Ｉｅｂ，Ｉｅｃ，Ｉｅｄ，Ｉｅｅ
・装置情報…Ｅａ，Ｅｂ，Ｅｃ
２．制約
・（Ｐ１）：Ｕｂ，＝Ｏｂ
・（Ｐ２）：Ｏｃ＝Ｉｏｂ∧（Ｏｄ＝Ｉｏｃ∨Ｏｄ＝ＮＵＬＬ∨Ｉｏｃ＝ＮＵＬＬ）
・（Ｐ３）：Ｃ＝Ｉｏｅ
・（Ｐ４）：Ｉｏｇ＝Ｉｅｂ∧（Ｉｏｈ＝Ｉｅｃ∨Ｉｏｈ＝ＮＵＬＬ∨Ｉｅｃ＝ＮＵＬＬ）
・（Ｐ５）：Ｉｏｇ＝Ｅｂ∧（Ｉｅｅ＝Ｅｃ∨Ｉｅｅ＝ＮＵＬＬ）
・（Ｐ６）：Ｔ＝Ｅａ
（Ｐ１）から（Ｐ６）までの制約の集合は、入力装置１から入力され、解モデル出力処理部５でそれらの入力から解モデルを出力する。解モデル出力処理部５では、図２乃至図４の処理フローに従い、まず（Ｐ１）から（Ｐ６）の論理式の連言をＤＮＦ変換手段５１で選言標準形に変換し、下記の連言項を生成する。
【００５７】
(1) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝Ｉｏｃ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝Ｉｅｃ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(2) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝Ｉｅｃ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(3) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｉｏｃ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝Ｉｅｃ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(4) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝Ｉｏｃ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(5) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(6) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｉｏｃ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(7) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝Ｉｏｃ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｅｃ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(8) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｅｃ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(9) Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｉｏｃ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｅｃ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝Ｅｃ∧Ｔ＝Ｅａ
(10)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝Ｉｏｃ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝Ｉｅｃ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(11)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝Ｉｅｃ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(12)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｉｏｃ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝Ｉｅｃ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(13)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝Ｉｏｃ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(14)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(15)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｉｏｃ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｏｈ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(16)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝Ｉｏｃ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｅｃ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(17)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｏｄ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｅｃ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
(18)Ｕｂ＝Ｏｂ∧Ｏｃ＝Ｉｏｂ∧Ｉｏｃ＝ＮＵＬＬ∧Ｃ＝Ｉｏｅ∧
Ｉｏｇ＝Ｉｅｂ∧Ｉｅｃ＝ＮＵＬＬ∧Ｉｅｄ＝Ｅｂ∧Ｉｅｅ＝ＮＵＬＬ∧Ｔ＝Ｅａ
次に、(1)から(18)の論理式それぞれの解モデルを解モデル出力手段５２で出力する。解モデル出力手段５２では、解モデルの初期値を下記のようにおいて(1)の場合の解モデルを求める。但し、この例の解モデルでは、常に肯定集合の要素数は１であり、否定集合は空集合なので省略して、値モデルは肯定集合の要素のみ記述する。
【００５８】
（Ｕａ，Ｕｂ，Ｔ，Ｃ，
Ｏａ，Ｏｂ，Ｏｃ，Ｏｄ，
Ｉｏａ，Ｉｏｂ，Ｉｏｃ，Ｉｏｄ，Ｉｏｅ，Ｉｏｆ，Ｉｏｇ，Ｉｏｈ，
Ｉｅａ，Ｉｅｂ，Ｉｅｃ，Ｉｅｄ，Ｉｅｅ，
Ｅａ，Ｅｂ，Ｅｃ）
＝（α，β，γ，δ，
ε，ζ，η，θ，
ι，κ，λ，μ，ν，ξ，ο，π，
ρ，σ，τ，υ，φ，
χ，ψ，ω）
(1)の場合、リテラルの集合は｛Ｕｂ＝Ｏｂ，Ｏｃ＝Ｉｏｂ，Ｏｄ＝Ｉｏｃ，Ｃ＝Ｉｏｅ，Ｉｏｇ＝Ｉｅｂ，Ｉｏｈ＝Ｉｅｃ，Ｉｅｄ＝Ｅｂ，Ｉｅｅ＝Ｅｃ，Ｔ＝Ｅａ｝となるので、まずＵｂ＝Ｏｂから解モデルの更新処理を行う。つまり、Ｕｂの値モデルの肯定集合の要素の変数とＯｂの値モデルの肯定集合の要素の変数が等しいので、解モデル中に出現する変数ζを変数βで置き換える。後は各リテラルに対して同様の処理を行うと、(1)の解モデルとして下記が得られ、ＤＢ出力手段５４により解モデルデータベース４に出力され記憶される。但し、下記の解モデルは整形手段５３により整形処理済みとする。
【００５９】
（Ｕａ，Ｕｂ，Ｔ，Ｃ，
Ｏａ，Ｏｂ，Ｏｃ，Ｏｄ，
Ｉｏａ，Ｉｏｂ，Ｉｏｃ，Ｉｏｄ，Ｉｏｅ，Ｉｏｆ，Ｉｏｇ，Ｉｏｈ，
Ｉｅａ，Ｉｅｂ，Ｉｅｃ，Ｉｅｄ，Ｉｅｅ，
Ｅａ，Ｅｂ，Ｅｃ）
＝（−，β，γ，δ，
−，β，η，θ，
−，η，θ，−，δ，−，ο，π，
−，ο，π，υ，φ，
γ，υ，φ）
このような解モデルを他の(2)から(18)の連言項に対して求める。解モデル出力手段５２が出力する(1)から(18)の解モデル（但し、前記同様整形処理済み）の全てを下記の表１に示す。列が各連言項に対する解モデルであり、ＮはＮＵＬＬという定数を表しているとする。
【００６０】
【表１】
2007241491.tif 000004
最後に、入力装置１から検査者からの問合せ（検索条件）が入力され、検索表示処理部６でその条件に合致する解モデルを探し出し、表示装置２に表示する。例えば、「ＩｏｈがＮＵＬＬの解」という問い合わせに対しては、(3)(4)(9)(10)(15)(16)の解モデルを表示する。また「ＵａとＥａの値モデルのみ表示させる」の場合、それらの値モデルはみな等しいので、Ｕａ＝−，Ｅａ＝γと表示する。
【００６１】
このように検査者は条件を入力し、解モデルを確認することで制約の誤りを発見する。本来の設備選定では、サービス種別Ｕａと装置種別Ｅａは対応する値にならなければいけない。しかし、それらの値モデルの肯定集合はそれぞれ｛−｝，｛γ｝と関連のない変数を要素としている。そのため充足解のＵａとＥａに対応する値はなんら関係のない値が解となってしまうことがわかる。このように解モデルの情報から制約の誤りを発見できる。
【図面の簡単な説明】
【００６２】
【図１】本発明の制約充足の試験方法全体の処理フローを示す図
【図２】解モデル出力処理工程の詳細な処理フローの一例を示す図
【図３】解モデル出力処理工程の詳細な処理フローの一例を示す図
【図４】解モデル出力処理工程の詳細な処理フローの一例を示す図
【図５】本発明の制約充足の試験装置の実施の形態の一例を示す構成図
【符号の説明】
【００６３】
１：入力装置、２：表示装置、３：コンピュータ、４：解モデルデータベース、５：解モデル出力処理部（装置）、６：検索表示処理部（装置）、５１：ＤＮＦ変換手段（モジュール）、５２：解モデル出力手段（モジュール）、５３：整形手段（モジュール）、５４：ＤＢ出力手段（モジュール）、５５：制御手段（モジュール）。
【図１】
2007241491.tif 000005
【図２】
2007241491.tif 000006
【図３】
2007241491.tif 000007
【図４】
2007241491.tif 000008
【図５】
2007241491.tif 000009