(57)【要約】【課題】データベース検索に於いて、複数の制約条件全てを満たしている全ての組合せ解を高速に求める充足可能解列挙システムを提供することを目的とする。【解決手段】制約条件の全ての項の中の式の数が２つ以下であった場合に変数を固定することによって依存関係グラフを作成して解を求める処理Ａ、制約条件の一つの項の中の変数が１種類である項があった場合に処理対象としなくて良い変数の要素を決定する処理Ｂ、制約条件の項で式が３つ以上且つ変数が２種類以上である場合に項の中の変数を一つ固定することによって処理Ａ又は処理Ｂが行えるまで項の中の制約条件の分岐を再帰的に行う処理Ｃ、制約条件の一つの項の中へ変数が２種類であって且つ片方に関する式が一つの場合に変数を固定することによって依存関係グラフを作成することで、処理を行わなくて良い変数の要素を決定する処理Ｄを有する充足可能解算出手段を有する充足可能解列挙システムである。【選択図】  図１
2004280523.tif 000002
【特許請求の範囲】
【請求項１】
複数の制約条件全てを満たしている全ての組合せ解を求める充足可能解列挙システムであって、
前記制約条件の全ての項の中の式の数が２つ以下であった場合に、変数を固定することによって依存関係グラフを作成して解を求める処理Ａからなる充足可能解算出手段を
有することを特徴とする充足可能解列挙システム。
【請求項２】
前記処理Ａは、
前記固定した変数から示すベクトルが前記依存関係グラフに於いて存在しない場合に、前記固定した変数を前記依存関係グラフから削除した依存関係グラフを再作成して再度変数を固定することによって解を求める
ことを特徴とする請求項１に記載の充足可能解列挙システム。
【請求項３】
前記充足可能解算出手段は、
前記制約条件の一つの項の中の変数が１種類である項があった場合には処理対象としなくて良い変数の要素を決定する処理Ｂを
有することを特徴とする請求項１又は請求項２に記載の充足可能解列挙システム。
【請求項４】
前記充足可能解算出手段は、
前記制約条件の項で式が３つ以上且つ変数が２種類以上である場合に、該項の中の変数を一つ固定することによって、前記処理Ａ又は処理Ｂが行えるまで項の中の制約条件の分岐を再帰的に行う処理Ｃを
有することを特徴とする請求項１から請求項３のいずれかに記載の充足可能解列挙システム。
【請求項５】
前記充足可能解算出手段は、
前記制約条件の一つの項の中へ変数が２種類であって且つ片方に関する式が一つの場合、変数を固定することによって依存関係グラフを作成することで、処理を行わなくて良い変数の要素を決定する処理Ｄを
有することを特徴とする請求項１から請求項４のいずれかに記載の充足可能解列挙システム。
【請求項６】
前記充足可能解列挙システムは、
前記制約条件の入力を受け付ける又は受信する制約条件受信手段と、
前記制約条件を連言標準形で生成する連言標準形生成手段とを
有することを特徴とする請求項１から請求項５のいずれかに記載の充足可能解列挙システム。
【請求項７】
前記制約条件が、
製品の構成要素の組合せである
ことを特徴とする請求項１から請求項６のいずれかに記載の充足可能解列挙システム。
【請求項８】
前記制約条件を構成する制約式の数が４１個以上である
ことを特徴とする請求項１から請求項７のいずれかに記載の充足可能解列挙システム。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、データベース検索に於いて、複数の制約条件全てを満たしている全ての組合せ解を高速に求める充足可能解列挙システムに関する。
【０００２】
【従来の技術】
工業製品には多数の部品を組み合わせて構成するものがあり、その設計は様々な部品仕様の組合せを考慮して目的の製品に叶った構成となるように行う。製品を構成する部品には各々仕様があり、部品を組み合わせて用いる場合には一定の制約がある。このような製品の設計を行う場合に、製品を構成する部品のうち、組合せ不可能なものを省き、予め組合せ可能なもののみを全て列挙しておけば非常に効率的な設計が可能となる。
【０００３】
又工業製品の組合せ以外にも、多数の複雑な制約条件の下でその制約条件全てを満たす組合せ解の全てを検索しなければならない場合もある。
【０００４】
このような組合せ可能解を算出する為に、従来はリレーショナルデータベースを用いて、ＳＱＬ等の検索言語に与えられた制約条件を記述することによって、検索を行うことが一般的である。
【０００５】
又複雑な制約条件下でそれを満たす全ての解の算出を高速に行う従来からの技術として、下記公報に示したように一番最初に不充足要求の列挙を順番付けし、その中から一の項目を選択し、再帰的に処理を不充足要求の処理を行うことで解の算出を行うシステムが存在している。
【０００６】
【特許文献１】
特表２００２−５１００９８号公報
【０００７】
【発明が解決しようとする課題】
上記のようにリレーショナルデータベースに於けるＳＱＬ言語等を用いた検索方法の場合、コンピュータ内部のメモリ空間に巨大な表を作成して計算を行う為、巨大なメモリを必要とし、又検索する次元の増加（制約条件の複雑さ）に伴い莫大な検索時間が必要となる問題点がある。更にリレーショナルデータベースでは、ＳＱＬ言語等の検索言語上の制約（記述できる制約条件の複雑さ、クエリーバッファ等）により複雑な条件を一度には設定することが出来ない。
【０００８】
又複雑な制約条件を数学的に算出する為の一般的方法の一つとして、分割法と呼ばれる方法がある。この方法は、例えばその制約条件を、
Ｘ＝｛ｘ１，ｘ２，…，ｘｎ｝  ｘｉ∈｛０，…，ｋｉ｝
（ｉ＝１，２，…，ｎ）
とした場合、制約条件は連言標準形を用いて表現すると、
（ｘ１１＝ｊ１１∪ｘ１２＝ｊ１２∪・・・∪ｘ１｜１＝ｊ１｜１）
∩（ｘ２１＝ｊ２１∪ｘ２２＝ｊ２２∪・・・∪ｘ２｜２＝ｊ２｜２）
・
・
∩（ｘｍ１＝ｊｍ１∪ｘｍ２＝ｊｍ２∪・・・∪ｘｍ｜ｍ＝ｊｍ｜ｍ）
として表現される。この制約条件から分割法に基づいてに基づいて該当する結果を抽出する為には以下の処理を行えばよい。即ち、
処理：ｘｉ＝ｊｉとして固定することにより制約条件をｘｉ＋１，…，ｘｎの式にする。
▲１▼ｘｉ＋１，…，ｘｎが全てｘｉ＋１＝ｊｉ＋１，…，ｘｎ＝ｊｎに決まった場合
ｘ１＝ｊ１，ｘ２＝ｊ２，…，ｘｎ＝ｊｎは解。
ｊｉ＝ｊｉ＋１として処理へ
▲２▼条件が満たされなくなった場合
それ以下の再帰は中断。
ｉ＝１，ｊ１＝ｊ１＋１として処理へ
▲３▼それ以外の場合
ｉ＝ｉ＋１，ｊｉ＝０として処理へ
【０００９】
上記のようにして、複雑な制約条件の下でそれを全て満たす解（充足可能解）の算出が可能であるが、このような従来の分割法だけでは、今探索している枝（分岐）の末端が解であるか否かを判定する為に不要な処理が必要となる場合がある。
【００１０】
上記公報（特表２００２−５１００９８号公報）では、上記のような不要な処理を省く為に、先に不充足要求の列挙を順番付けし、再帰的に処理を行うことによって、その解決を図っているが、一番最初に不充足要求の順番付を行う必要がある為に、複雑な制約条件になればなるほど、その処理に時間を要し、高速化の要求を充分に満足するものではない。
【００１１】
【課題を解決するための手段】
そこで本願発明者は、組合せを検索する為の条件を充足可能解の列挙問題として定式化し、条件分岐によって生成される探索ツリーを深さ優先探索し、探索の浅いレベルで探索の必要性を調査し、不要な枝を早い段階で削減することによって探索を効率化する。又複雑な制約条件を単純な制約条件に帰着させるような分岐を行い、単純な制約条件の集合になった際に依存関係グラフによって高速に解を求めることで上記問題点を解決する充足可能解列挙システムを発明した。
【００１２】
請求項１の発明は、
複数の制約条件全てを満たしている全ての組合せ解を求める充足可能解列挙システムであって、前記制約条件の全ての項の中の式の数が２つ以下であった場合に、変数を固定することによって依存関係グラフを作成して解を求める処理Ａからなる充足可能解算出手段を有する充足可能解列挙システムである。
【００１３】
請求項２の発明は、
前記処理Ａは、前記固定した変数から示すベクトルが前記依存関係グラフに於いて存在しない場合に、前記固定した変数を前記依存関係グラフから削除した依存関係グラフを再作成して再度変数を固定することによって解を求める充足可能解列挙システムである。
【００１４】
請求項１及び請求項２の発明によって、変数を固定することによって再帰的に依存関係グラフを作成することが可能となり、これによって、不必要な処理を行わずに、制約条件全てを満たす組合せの解全てを算出することが可能となる。
【００１５】
請求項３の発明は、
前記充足可能解算出手段は、前記制約条件の一つの項の中の変数が１種類である項があった場合には処理対象としなくて良い変数の要素を決定する処理Ｂを有する充足可能解列挙システムである。
【００１６】
請求項３の発明によって、処理対象としなくても良い変数の要素を決定することが可能となり、これによって無駄な処理を無くし従来よりも高速に処理が可能となる。
【００１７】
請求項４の発明は、
前記充足可能解算出手段は、前記制約条件の項で式が３つ以上且つ変数が２種類以上である場合に、該項の中の変数を一つ固定することによって、前記処理Ａ又は処理Ｂが行えるまで項の中の制約条件の分岐を再帰的に行う処理Ｃを有する充足可能解列挙システムである。
【００１８】
請求項４の発明によって、制約条件の項の中の式の数が２つ以下又は変数が１種類である必要がなくなり、汎用性のある充足可能解列挙システムとすることが可能となる。
【００１９】
請求項５の発明は、
前記充足可能解算出手段は、前記制約条件の一つの項の中へ変数が２種類であって且つ片方に関する式が一つの場合、変数を固定することによって依存関係グラフを作成することで、処理を行わなくて良い変数の要素を決定する処理Ｄを有する充足可能解列挙システムである。
【００２０】
請求項５の発明によって、上記条件を満たす場合に例外処理として処理Ｄを行うことが可能となり、処理対象としなくても良い変数の要素を決定することが可能となる。これによって、従来よりも高速に処理が可能となる。
【００２１】
請求項６の発明は、
前記充足可能解列挙システムは、前記制約条件の入力を受け付ける又は受信する制約条件受信手段と、前記制約条件を連言標準形で生成する連言標準形生成手段とを有する充足可能解列挙システムである。
【００２２】
制約条件は、連言標準形で算出することが好ましい。従って請求項７の発明によって一般的な形で制約条件を受信しても、連言標準形に変換してから処理が可能となる。
【００２３】
請求項７の発明は、
前記制約条件が、製品の構成要素の組合せである充足可能解列挙システムである。
【００２４】
工業製品には多数の部品を組み合わせて構成するものがあるが、通常それらは複雑な制約条件の下で多数の部品を組み合わせなければならない。従来は、製品全体の部品構成を把握している熟練した設計者が判断していたが、間違いが発生する可能性があり、又経験がなければこのような組合せを判断することは困難であった。従って本発明を製品の構成要素の組合せに用いることによって、そのような経験が無くても誰でも容易にこの複雑な組合せを全て算出することが可能となる。
【００２５】
請求項８の発明は、
前記制約条件を構成する制約式の数が４１個以上である充足可能解列挙システムである。
【００２６】
従来、一般に流通しているリレーショナルデータベースでは、制約条件を構成する制約式の数が４０個までしか受け付けなかった。つまりデータベース検索を行う際の条件に制限があった。その為、極端に複雑な制約条件でデータベース検索を行う場合には、制約条件を別の論理式に変換しその個数の範囲内に納める、或いは制約条件を分割し複数回の検索を行う等の方法が行われていた。しかし本発明を用いることによって、制約条件の数が無制限となり、どんなに複雑な制約条件であっても高速にデータベース検索が出来ることとなる。尚、本明細書に於いて制約条件とは制約式の組合せであって、制約式とは制約条件に於ける項、即ち論理演算子と値との組合せを言う。例えば制約条件が以下のようである場合、
（ｘ１１＝ｊ１１∪ｘ１２＝ｊ１２∪・・・∪ｘ１｜１＝ｊ１｜１）
∩（ｘ２１＝ｊ２１∪ｘ２２＝ｊ２２∪・・・∪ｘ２｜２＝ｊ２｜２）
・
・
∩（ｘｍ１＝ｊｍ１∪ｘｍ２＝ｊｍ２∪・・・∪ｘｍ｜ｍ＝ｊｍ｜ｍ）
各々の括弧内（例えば（ｘ１１＝ｊ１１∪ｘ１２＝ｊ１２∪・・・∪ｘ１｜１＝ｊ１｜１））が制約式となる。
【００２７】
【発明の実施の形態】
本発明の実施態様のシステム構成の一例を図１のシステム構成図を用いて説明する。充足可能解列挙システム１は、制約条件受信手段２と連言標準形生成手段３と充足可能解算出手段４と出力手段５とデータベース６とを有している。尚、以下の実施例１及び実施例２に於いては説明の簡略化の為、制約条件との表現は、制約条件又は制約式を示すものとする。
【００２８】
データベース６は、検索対象となるデータを格納しているデータベース６である。
【００２９】
制約条件受信手段２は、データベース６を検索する為の制約条件の入力を受け付ける又はコンピュータネットワークを介して受信する手段である。コンピュータネットワークには、インターネット等のオープンネットワーク、ＬＡＮ等のクローズドネットワーク、これらの組合せであるイントラネット等の何れであっても良く、有線・無線の別も問わない。
【００３０】
連言標準形生成手段３は、制約条件受信手段２が受信した制約条件を連言標準形で生成する手段である。制約条件は論理式で示され全ての論理式は連言標準形で示されることが公知である。ここで連言標準形とは、［（Ａ  ｏｒ  Ｂ）  ａｎｄ  （Ａ  ｏｒ  Ｃ）  ａｎｄ  ・ａｎｄ  ・  ａｎｄ  ・］で示される論理式を言う。
【００３１】
例えば制約条件受信手段２で受信した制約条件が、Ｘ＝｛ｘ１，ｘ２，・・・，ｘｎ｝ｘｉ∈｛０，・・・，ｋｉ｝（ｉ＝１，２，・・・，ｎ）である時、連言標準形生成手段３は、制約条件を
（ｘ１１＝ｊ１１∪ｘ１２＝ｊ１２∪・・・∪ｘ１｜１＝ｊ１｜１）
∩（ｘ２１＝ｊ２１∪ｘ２２＝ｊ２２∪・・・∪ｘ２｜２＝ｊ２｜２）
・
・
∩（ｘｍ１＝ｊｍ１∪ｘｍ２＝ｊｍ２∪・・・∪ｘｍ｜ｍ＝ｊｍ｜ｍ）
として示されるように連言標準形を生成する。
【００３２】
充足可能解算出手段４は、制約条件の全ての項の中の式の数が２つ以下となった場合に、依存関係グラフを作成して解の存在性を高速に判別する処理Ａを有する手段である。
【００３３】
処理Ａは、例えば制約条件受信手段２で受信した制約条件がｘ１＝｛０，１｝、ｘ２＝｛０，１｝、ｘ３＝｛０，１，２｝、ｘ４＝｛０，１｝である場合、連言標準形生成手段３で生成する連言標準形は、
（ｘ１＝０∪ｘ２＝１）
∩（ｘ２＝１∪ｘ４＝１）
∩（ｘ３＝１∪ｘ１＝１）
として生成される。この生成された連言標準形を連言標準形生成手段３から受信して、充足可能解算出手段４で制約条件の判別を行うと、制約条件の全ての項の中の式の数が２つ以下であるので処理Ａを行う為の条件を満たしている。
【００３４】
又制約条件は、
（ｘ１＝０∪ｘ２＝１）  ：ｘ１≠０→ｘ２＝１、ｘ２≠１→ｘ１＝０
（ｘ２＝１∪ｘ４＝１）  ：ｘ２≠１→ｘ４＝１、ｘ４≠１→ｘ２＝１
（ｘ３＝１∪ｘ１＝１）  ：ｘ３≠１→ｘ１＝１、ｘ１≠１→ｘ３＝１
を意味していることが明らかであるので、これに基づいて図６に示す依存関係グラフを作成する。当然の事ながら図６に示した依存関係グラフは概念図であり、実際の充足可能解列挙システム１上では、リスト処理、マトリックス処理、ハッシュ等を用いて表現されていることは言うまでもない（本明細書に於いては以下同様である）。
【００３５】
ここで作成した依存関係グラフに於いて、各変数を固定して充足可能解算出手段４の処理Ａは解を算出する。例えば前記の連言標準形では、ｘ２＝０として固定した場合に、ｘ２を始点とするベクトルは図６から分かるように、ｘ１＝０、ｘ３＝１，ｘ４＝１である。従ってｘ２＝０として固定した場合の解は、
ｘ２＝０→ｘ１＝０、ｘ３＝１，ｘ４＝１
となる。
【００３６】
次にｘ２＝１を固定した場合、ｘ２を始点とするベクトルは存在しないので、ｘ２＝１となる解は決まらない。従ってｘ２を除いた依存関係グラフを更に作成し解を算出する（依存関係グラフを再帰的に呼び出して作成する）。図７にこの場合の依存関係グラフを示す。ここでｘ１＝０に注目し変数を固定すると、ここを始点とするベクトルはｘ３＝１であり、ｘ４に関しては制約がないのでｘ４＝０，１両方の値を取りうる。従ってｘ２＝１を固定した場合の解は、
ｘ２＝１，ｘ１＝０→ｘ３＝１、ｘ４＝０又はｘ３＝１，ｘ４＝１
となる。
【００３７】
又図７の依存関係グラフに於いてｘ１＝１として変数を固定した場合、ここを始点とするベクトルはないので、ｘ１＝１とする解は決まらない。従って図７の依存関係グラフから更にｘ１を除いた依存関係グラフを作成する。図８にこの場合の依存関係グラフを示す。図８の依存関係グラフでは制約が存在しないので、ｘ２＝１，ｘ１＝１の場合、ｘ３，ｘ４は全ての値を取り得て解となる。
【００３８】
以上のようなことから上記例では
（ｘ１，ｘ２，ｘ３，ｘ４）＝（０，０，１，１），（０，１，１，０），
（０，１，１，１），（１，１，０，０），
（１，１，０，１），（１，１，１，０），
（１，１，１，１）
が処理Ａの算出する解となる。
【００３９】
以上のように充足可能解算出手段４は、制約条件の全ての項の中の式の数が２つ以下となった場合に依存関係グラフを作成して解の存在性を高速に判別する。又固定した変数から示すベクトルが存在しない場合には、当該変数を前記作成した依存関係グラフから削除した依存関係グラフを作成し変数を固定することによって解を求める。このように再帰的に依存関係グラフを再作成し（依存関係グラフを再帰的に呼び出す）変数を固定することによって解を算出することで、不必要な処理を行わずに条件を満たす全ての解の算出が可能となる。
【００４０】
又処理Ａを行うには、全ての項の中の式の数が２つ以下になる必要があるが、制約条件の一つの項の中の変数が１種類である項があった場合には処理対象としなくて良い変数の要素を決定することも出来る。この決定処理を処理Ｂとする。従って充足可能解算出手段４は更に処理Ｂを有していても良い。
【００４１】
処理Ｂは、制約条件の任意の項が１種類のみである場合、例えばｘ１＝｛０，１，２，３｝であって（ｘ１＝０∪ｘ１＝１）の制約条件である場合に、依存関係グラフを作成することによって、処理対象としなくて良い変数の要素を決定することが可能となる。このｘ１の例では、依存関係グラフは図９のように作成できる。従ってｘ１＝２，３を処理対象としなくて良いことは明らかである。
【００４２】
処理Ａ、処理Ｂを行う為に少なくとも式が２つ以下又は変数が１種類である必要がある。しかし一般的には制約条件が複雑（式が３つ以上且つ変数が２種類以上）であり、上記条件を満たさない場合が多い。そのような場合に処理Ａと処理Ｂのみでは処理が行えないので、従来の方法で分割法を行う以外に、高速に処理を行わせる為に充足可能解算出手段４は、更に処理Ｃを設けてもよい。
【００４３】
処理Ｃは、制約条件の項に於いて、式が３つ以上且つ変数２種類以上である場合（即ち処理Ａ、処理Ｂが使えない場合）、処理Ａ又は処理Ｂに帰着させる為の処理を行う手段である。即ち式が３つ以上且つ変数が２種類以上の項の中の変数を一つ固定することによって、処理Ａ又は処理Ｂの処理が行えるまで項の中の制約条件の分岐を再帰的に行う手段である。
【００４４】
例えば制約条件が
ｘ１＝０∪ｘ２＝０∪ｘ３＝０∪ｘ４＝０
であった場合、
最初にｘ１＝０として変数を固定すると、この制約条件は必ず成立する。次にｘ１＝１として変数を固定するとこの制約条件は、
ｘ２＝０∪ｘ３＝０∪ｘ４＝０
として示され式の数を減らすことが出来る。
【００４５】
このように処理Ａ又は処理Ｂを用いるには、項の中の式の数が２つ以下又は変数が１種類である必要があるので、項の中の式の数が３以上である場合には処理が行えない。このような場合に処理Ｃを用いてこの中の式の数を減らし（即ち変数を固定することによって制約条件を分岐することとなる）解の判定を高速に行うことが可能となる。
【００４６】
又この項の中の制約条件を分岐する方法は、再帰処理を使うことが好適である。
【００４７】
又処理Ａ、処理Ｂ、処理Ｃを行う前に更に、一つの項の中へ変数が２種類であって且つ片方に関する式が一つだけの場合、変数を一つ固定することによって依存関係グラフからいくつかの変数が自動的に固定される。この処理を処理Ｄとする。従って上記条件を満たす場合にこの処理Ｄを行うことによって、更に高速に処理を行うことが可能となる。
【００４８】
例えば制約条件が
（ｘ１＝０∪ｘ１＝１∪ｘ１＝２∪ｘ２＝０）
の場合には、図１０に示す依存関係グラフとなる。
【００４９】
以上のように、充足可能解算出手段４は処理Ａを行うことを基本とするが、処理Ａに処理Ｂを加えて行うことで高速に処理が可能である。又処理Ａ、処理Ｂを行う場合には式が２つ以下又は変数１種類以上である場合にしか処理が出来ないので処理Ｃを行うことで処理Ａ又は処理Ｂに帰着させることが可能となる。従って処理Ａと処理Ｃ、処理Ａと処理Ｂと処理Ｃとを充足可能解算出手段４が有していても良い。又処理Ａ、処理Ｂ、処理Ｃの処理に加えて処理Ｄを行うことで、処理を行わなくても良い変数の要素を決定し、処理の高速化を図ることも可能となる。即ち処理Ａと処理Ｄ、処理Ａと処理Ｂと処理Ｄ、処理Ａと処理Ｃと処理Ｄ、処理Ａと処理Ｂと処理Ｃと処理Ｄとを充足可能解算出手段４が有していても良い。
【００５０】
出力手段５は、充足可能解算出手段４で算出した解に基づいて、データベース６の中から算出した解以外の解を検索し、検索結果として表示する手段である。
【００５１】
【実施例】
次に本発明のプロセスの流れの一例を図２のフローチャート図及び図１のシステム構成図を用いて詳細に説明する。尚本実施例では充足可能解算出手段４が処理Ａ、処理Ｂ、処理Ｃ、処理Ｄを有している場合を説明するが、前述のように処理Ａのみ、処理Ａと処理Ｂ、処理Ａと処理Ｃ、処理Ａと処理Ｂと処理Ｃ、処理Ａと処理Ｃと処理Ｄを有している場合でも良い。又図２のＳ１２０に於ける充足可能解算出の概略を示したフローチャート図を図３６に示す。更に図３６に示したフローチャート図の詳細を、図３から図５のフローチャート図に示す。
【００５２】
複雑な条件（制約条件）を満たす全ての組合せ解をデータベース６から求めるユーザは、データベース６から検索する為の制約条件を入力する。入力された制約条件を制約条件受信手段２が受け付け又はコンピュータネットワークを介して受信する（Ｓ１００）。ここで受信した制約条件の概念図を図１１に示す。図１１では、各条件のアンド条件（且つ。論理記号では∩）を「○」印の交差で示してある。例えば条件Ａのｘ０＝０∩ｘ１＝０∩ｘ２＝０がそのうちの一つである。
【００５３】
連言標準形生成手段３が、制約条件受信手段２が受信した制約条件を連言標準形で生成する（Ｓ１１０）。例えば図１１に示した制約条件の場合、条件Ａを論理式で示すと、
（ｘ０＝０∩ｘ１＝０∩ｘ２＝０）∪（ｘ０＝１∩ｘ１＝０∩ｘ２＝１）
∪（ｘ０＝０∩ｘ１＝０∩ｘ２＝２）∪（ｘ０＝１∩ｘ１＝０∩ｘ２＝２）
∪（ｘ０＝１∩ｘ１＝１∩ｘ２＝０）∪（ｘ０＝２∩ｘ１＝１∩ｘ２＝０）
∪（ｘ０＝３∩ｘ１＝１∩ｘ２＝１）∪（ｘ０＝０∩ｘ１＝１∩ｘ２＝２）
でありこれを連言標準形生成手段３が連言標準形を生成すると、
≡（ｘ０＝０∪ｘ１＝１∪ｘ２＝１∪ｘ２＝２）
∩（ｘ０＝１∪ｘ１＝１∪ｘ２＝０∪ｘ２＝２）
∩（ｘ０＝０∪ｘ０＝１∪ｘ１＝１∪ｘ２＝０∪ｘ２＝１）
∩（ｘ０＝１∪ｘ０＝２∪ｘ１＝０∪ｘ２＝１∪ｘ２＝２）
∩（ｘ０＝３∪ｘ１＝０∪ｘ２＝０∪ｘ２＝２）
∩（ｘ０＝０∪ｘ１＝０∪ｘ２＝０∪ｘ２＝１）
となる。
【００５４】
同様に連言標準形生成手段３が条件Ｂから連言標準形を生成すると、
（ｘ３＝１∩ｘ２＝０）∪（ｘ３＝０∩ｘ２＝１）
∪（ｘ３＝２∩ｘ２＝１）∪（ｘ３＝０∩ｘ２＝２）
≡（ｘ３＝１∪ｘ２＝１∪ｘ２＝２）
∩（ｘ３＝０∪ｘ３＝２∪ｘ２＝０∪ｘ２＝２）
∩（ｘ３＝０∪ｘ２＝０∪ｘ２＝１）
となる。更に条件Ａと条件Ｂとを全て満たす解を求める必要があるので、条件Ａと条件Ｂとのアンド条件を連言標準形生成手段３が生成する。
【００５５】
条件Ａ∩条件Ｂ：
（ｘ０＝０∪ｘ１＝１∪ｘ２＝１∪ｘ２＝２）
∩（ｘ０＝１∪ｘ１＝１∪ｘ２＝０∪ｘ２＝２）
∩（ｘ０＝０∪ｘ０＝１∪ｘ１＝１∪ｘ２＝０∪ｘ２＝１）
∩（ｘ０＝１∪ｘ０＝２∪ｘ１＝０∪ｘ２＝１∪ｘ２＝２）
∩（ｘ０＝３∪ｘ１＝０∪ｘ２＝０∪ｘ２＝２）
∩（ｘ０＝０∪ｘ１＝０∪ｘ２＝０∪ｘ２＝１）
∩（ｘ３＝１∪ｘ２＝１∪ｘ２＝２）
∩（ｘ３＝０∪ｘ３＝２∪ｘ２＝０∪ｘ２＝２）
∩（ｘ３＝０∪ｘ２＝０∪ｘ２＝１）
となる。従って制約条件の連言標準形は上記論理式となり、連言標準形生成手段３はこの論理式を生成することとなる。この際の連言標準形で示される制約条件を基本制約条件とする。
【００５６】
連言標準形生成手段３で生成した制約条件に基づいて、これら全てを満たす解の組合せを充足可能解算出手段４が算出する（Ｓ１２０）。
【００５７】
充足可能解算出手段４では、連言標準形生成手段３で生成した制約条件に対して処理Ａ、処理Ｂ、処理Ｃ、処理Ｄを用いて高速に解算出を行う。図１１の制約条件に於ける解の算出の説明を図３から図５のフローチャート図を用いて行う。
【００５８】
まず深さを１に設定する（Ｓ２００）。ここで深さとは、充足可能解を算出するにあたって、その再帰的処理をどのレベル（深さ）まで行っているかを示すものであって、深さ１は再帰処理を行っていない状態、深さ２は再帰処理を１回行っている状態を示す。
【００５９】
次に深さに於ける項の数を１に設定する（Ｓ２１０）。これは現在処理対象としている深さに於ける、項の処理数を示しているものである。従って当初の制約条件（即ち基本制約条件）では、深さが１であって項の数が１である。
【００６０】
次に現在処理中の深さに於いて全ての変数の要素が決定しているか否かの判別を行い（Ｓ２２０）、決定されている場合には当該深さに於ける解が全て算出できているので「ＹＥＳ」の処理、即ち実際に解を算出し、深さが１に於ける次の項の処理を行わせる。決定されていない場合には解の算出が行えないので「ＮＯ」の処理、即ち解を求める処理を行う。図１１に示した制約条件では、まだ基本制約条件の深さと項の数とを設定したのみであるので、当然に「ＮＯ」の処理を行うこととなる。
【００６１】
次に当該深さに於ける制約条件の項に於いて、式が３つ以上且つ変数が２種類以上の項▲１▼と、式が２つ以下又は変数が１種類の項▲２▼との判別を行う（Ｓ２３０）。即ち各項が処理Ａ又は処理Ｂを行う為の条件を満たしているか否かの判別を行うこととなる。
【００６２】
Ｓ２３０の判別の結果、未処理の項▲２▼が存在している場合には処理Ａ又は処理Ｂが行えるので、「ＹＥＳ」へ、ない場合には「ＮＯ」の処理（即ち処理Ｃを行う）を行うこととなる（Ｓ２４０）。
【００６３】
基本制約条件の深さ１に於いては、基本制約条件の各項はいずれも項▲１▼（式が３つ以上且つ変数が２種類以上）であるので、「ＮＯ」へ進み、一つの項の変数が２種類で片方に関する式が一つであるか否かの判別（即ち処理Ｄが行えるか否かの判別）を行う（Ｓ３４０）。
【００６４】
この場合は該当しないので「ＮＯ」へ進み、現在処理中の深さ（この場合には深さ１）に於ける制約条件で多く含まれている変数を抽出する（Ｓ３９０）。深さ１の制約条件、即ち基本制約条件に於いて多く含まれている変数はｘ２なのでｘ２を抽出することとなる。
【００６５】
Ｓ３９０で抽出した変数の要素を固定することによって、制約条件の分岐処理を行わせる（Ｓ４００）。当然のことながら全ての変数の要素は固定していないのでＳ３９５は「ＮＯ」へ進む。ここでｘ２の要素は、図１１の制約条件よりｘ２＝｛０，１，２｝であるので、ｘ２＝０として固定する。ｘ２を固定した場合の制約条件の概念図を図１２に示す。ここで変数の要素を固定することは、深さを１段階深くすることなので（Ｓ４１０）、深さを２に変更する。又深さを深くした際に、その変数の要素を固定した場合の制約条件を同時に作成する。この場合の制約条件は、
（ｘ０＝０∪ｘ１＝１）
∩（ｘ０＝１∪ｘ０＝２∪ｘ１＝０）
∩（ｘ３＝１）
となる。この際の制約条件を制約条件２と呼ぶこととする。この制約条件２は、基本制約条件にｘ２＝０を代入すると一意的に導出される。
【００６６】
深さを深くしたと言うことは、再帰的に制約条件の処理を行っていることなので、Ｓ２１０に戻る。
【００６７】
Ｓ２１０では、深さ２に於ける項の数を１に設定する。深さ２に於いて全ての変数は決定していないので（Ｓ２２０）、「ＮＯ」の処理を行うこととなる。深さ２に於ける制約条件２では、第１項と第３項が項▲２▼で第２項が項▲１▼であるので（Ｓ２３０）、Ｓ２４０では「ＹＥＳ」に進む（Ｓ２４０）。本発明の再帰処理では深さ優先探索であるのでいずれの項から処理を開始しても構わないが、本実施例では制約条件２の第３項の処理を行った後に、第１項の処理を行うものとする。勿論逆であっても構わない。
【００６８】
次に当該処理対象となる項（この場合は制約条件２の第３項）が、一つの項の中の変数が１種類であるか否かの判別（即ち処理Ｂが行えるか否かの判別）を行う（Ｓ２５０）。第３項はｘ３＝１であるので条件を満たしており、「ＹＥＳ」へ進む。
【００６９】
第３項に対して処理Ｂを行い（Ｓ２６０）、ｘ３＝１は、ｘ２＝０として固定した際の解の要素として決定する。ｘ３＝１として決定した場合の制約条件の概念図を図１３に示す。
【００７０】
次に依存関係グラフのｘ３＝１が従前に決定した解の要素と矛盾するか否かの判別を依存関係グラフを重ね合わせることによって行うが（Ｓ２８０）、この場合は、まだ最初の解であるので矛盾はなく（Ｓ２９０）、Ｓ３１０に進む。第３項の処理が終了したので、次の項の処理へ進む（Ｓ３１０）。この際に当該深さに於ける項の処理数を１増やす。この場合には深さ２に於ける項の処理数を２にする。
【００７１】
当該深さに於ける全ての項の処理が終了しているか否かの判別を行い（Ｓ３２０）、この場合は深さ２に於ける項の処理数が２であり、深さ２に於ける項の数が３であるのでまだ全ての項の処理が終了していないことが分かる。従って「ＮＯ」へ進み、次の項（制約条件２の第１項）の処理、即ちＳ２４０に戻る。
【００７２】
制約条件２の第１項は、未処理の項▲２▼であるので、「ＹＥＳ」に進み、一つの項の中の変数が１種類であるか否かの判別（即ち処理Ｂが行えるか否かの判別）を行う（Ｓ２５０）。第１項は条件を満たしていないので、「ＮＯ」へ進む。即ち処理Ａを行う（Ｓ２７０）。
【００７３】
制約条件２の第１項は、ｘ０＝０∪ｘ１＝１であるので処理Ａより依存関係グラフを作成すると、図１４になる。つまりｘ０≠０→ｘ１＝１，ｘ１≠１→ｘ０＝０という解の要素が求まる。
【００７４】
Ｓ２７０で求まった解の要素を、先程算出した解の要素（深さ２，処理数１の時の解の要素）ｘ３＝１と依存関係グラフを重ね合わせ（Ｓ２８０）、矛盾の判断を行う（Ｓ２９０）。ｘ０とｘ１，ｘ３の間には依存関係ないので、矛盾ではない。
【００７５】
従って深さ２に於ける次の項の処理を行う（Ｓ３１０）。この際に当該深さに於ける項の処理数を１増やす。この場合には深さ２に於ける項の処理数を３にする。
【００７６】
当該深さに於ける全ての項の処理が終了しているか否かの判別を行い（Ｓ３２０）、この場合は深さ２に於ける項の処理数が３であり、深さ２に於ける項の数が３であるのでまだ全ての項の処理が終了していない（項の処理数が項の数より多くなった場合が全ての項の処理が終了したことを意味する）ことが分かる。従って「ＮＯ」の処理を行い、次の項（制約条件２の第２項）の処理、即ちＳ２４０に戻る。
【００７７】
次に制約条件２に於いて、第１項と第３項の処理は終了したので処理していない項は、第２項のみである。第２項は項▲１▼であるので、Ｓ２４０の判別で「ＮＯ」に進む。
【００７８】
次に、処理Ｄを用いることが出来るか否かの判別を行う（Ｓ３４０）。即ち処理Ｄを行う為の条件である、一つの項の変数が２種類で片方に関する式が一つである項が存在するか否かの判別を制約条件２の第２項に対して行う。
【００７９】
Ｓ３４０の判別の結果、第２項は（ｘ０＝１∪ｘ０＝２∪ｘ１＝０）であり、当該条件を満たしているので、処理Ｄを行うことによって（Ｓ３５０）、依存関係グラフからいくつかの変数が自動的に固定される。第２項の依存関係グラフを図１５に示す。
【００８０】
Ｓ３５０によって作成した第２項の依存関係グラフとそれ以前の同じ深さの異なる項の依存関係グラフ（この場合は、第１項と第３項）の依存関係グラフを重ね合わせることによって（Ｓ３６０）矛盾の判別を行う（Ｓ３７０）。重ね合わせた依存関係グラフを図１６に示す。
【００８１】
Ｓ３６０で重ね合わせた依存関係グラフから明らかなように、ｘ０＝３の時にはｘ１に関して矛盾が発生しているのでｘ０＝３に関する解は存在しないことが分かる。この場合の概念図は図１７となる。従ってｘ０＝３に関する処理は、今後ｘ２＝０として固定した場合には行わなくても良いこととなり、矛盾する変数の要素（この場合はｘ０＝３）は処理しないことの決定をする（Ｓ３８０）。
【００８２】
又第２項は、項▲１▼でもあるので当該深さに於ける制約条件で多く含まれる変数を抽出する（Ｓ３９０）。深さ３の制約条件、即ち制約条件２に於いて多く含まれている変数はｘ０なのでｘ０を抽出することとなる。
【００８３】
Ｓ３９０で抽出した変数の要素を固定することによって、制約条件の分岐処理を行わせる（Ｓ４００）。当然のことながら全ての変数の要素は固定していないのでＳ３９５は「ＮＯ」へ進む。ここでｘ０の要素は、図１１の制約条件よりｘ０＝｛０，１，２，３｝である（但しｘ０＝３は処理Ｄによって処理しなくて良いことが判別済み）ので、ｘ０＝０として固定する。ここで変数の要素を固定することは、深さを１段階深くすることなので（Ｓ４１０）、深さを３に変更する。又深さを深くした際に、その変数の要素を固定した場合の制約条件を同時に作成する。この場合の制約条件は、（ｘ１＝０）となる。この際の制約条件を制約条件３と呼ぶこととする。この制約条件３は、制約条件２にｘ０＝０を代入すると一意的に導出される。
【００８４】
深さを深くしたと言うことは、再帰的に制約条件の処理を行っていることなので、Ｓ２１０に戻る。深さ３に於ける全ての変数は決定していないのでＳ２２０の「ＮＯ」に進み、制約条件３は項▲２▼であり（ｘ０＝０）は未処理であるので、（Ｓ２４０）、Ｓ２５０に進む。Ｓ２５０の判別では、項の中の変数が１種類であるので、処理Ｂからｘ１＝０が解の要素として決定する（Ｓ２６０）。この際の依存関係グラフを重ねると（Ｓ２８０）、矛盾は発生しないので（Ｓ２９０）次の項の処理へ進む。
【００８５】
ところが、制約条件３は一つの項からなっているので、Ｓ３２０に於いては全ての項の処理が終了したこととなり、深さを１段階戻すこととなる（Ｓ３３０）。従って深さを２に戻し、Ｓ３９５に戻る。
【００８６】
深さ２を２に戻したことは、再帰を一つ戻したことになるので、制約条件２の第２項の処理のｘ０＝０として固定した場合の次の要素、即ちｘ０＝１として次の要素の処理を行う。
【００８７】
又変数の要素をｘ０＝１として固定したので、深さを１段階深くし（Ｓ４１０）、再度深さを３に変更する。又深さを深くした際に、その変数の要素を固定した場合の制約条件を同時に作成する。この場合の制約条件は、（ｘ１＝１）となる。この際の制約条件を制約条件４と呼ぶこととする。この制約条件４は、制約条件２にｘ０＝１を代入すると一意的に導出される。
【００８８】
深さを深くしたと言うことは、再帰的に制約条件の処理を行っていることなので、Ｓ２１０に戻る。深さ３に於ける全ての変数は決定していないのでＳ２２０の「ＮＯ」に進み、制約条件４は項▲２▼であり（ｘ０＝１）は未処理であるので、（Ｓ２４０）、Ｓ２５０に進む。Ｓ２５０の判別では、項の中の変数が１種類であるので、処理Ｂからｘ１＝１が解の要素として決定する（Ｓ２６０）。この際の依存関係グラフを重ねると（Ｓ２８０）、矛盾は発生しないので（Ｓ２９０）次の項の処理へ進む。
【００８９】
ところが、制約条件４は一つの項からなっているので、Ｓ３２０に於いては全ての項の処理が終了したこととなり、深さを１段階戻すこととなる（Ｓ３３０）。従って深さを２に戻し、Ｓ３９５に戻る。
【００９０】
深さ２を２に戻したことは、再帰を一つ戻したことになるので、制約条件２の第２項の処理のｘ０＝０，１として固定した場合の次の要素、即ちｘ０＝２として次の要素の処理を行う。
【００９１】
又変数の要素をｘ０＝２として固定したので、深さを１段階深くし（Ｓ４１０）、再度深さを３に変更する。又深さを深くした際に、その変数の要素を固定した場合の制約条件を同時に作成する。この場合の制約条件は、（ｘ１＝１）となる。この際の制約条件を制約条件５と呼ぶこととする。この制約条件５は、制約条件２にｘ０＝２を代入すると一意的に導出される。
【００９２】
深さを深くしたと言うことは、再帰的に制約条件の処理を行っていることなので、Ｓ２１０に戻る。深さ３に於ける全ての変数は決定していないのでＳ２２０の「ＮＯ」に進み、制約条件５は項▲２▼であり（ｘ０＝２）は未処理であるので、（Ｓ２４０）、Ｓ２５０に進む。Ｓ２５０の判別では、項の中の変数が１種類であるので、処理Ｂからｘ１＝１が解の要素として決定する（Ｓ２６０）。この際の依存関係グラフを重ねると（Ｓ２８０）、矛盾は発生しないので（Ｓ２９０）次の項の処理へ進む。
【００９３】
ところが、制約条件５は一つの項からなっているので、Ｓ３２０に於いては全ての項の処理が終了したこととなり、深さを１段階戻すこととなる（Ｓ３３０）。従って深さを２に戻し、Ｓ３９５に戻る。
【００９４】
Ｓ３９５の判別で、制約条件２の第２項の全ての変数の要素の固定したので、「ＹＥＳ」へ進み、深さを１段階戻す。又全ての変数の要素が固定し終わったと言うことは、その項の処理を全て終わったことなので、この項の解の要素が判明したこととなる。即ちこの場合は、制約条件２の第２項の解の要素が判明したこととなる。この場合の解の要素の概念図を図１８に示す。
【００９５】
更に深さが２に戻ったので、深さ２の時の全ての変数の要素が決定しているか否かの判別を行い、この場合は制約条件２の第１項、第２項、第３項全ての解の要素が判明したので、Ｓ２２０を「ＹＥＳ」へ進み、深さ２の際の充足可能解を算出する。この場合はｘ２＝０として固定した場合の解を算出することとなり、（ｘ０，ｘ１，ｘ２，ｘ３）＝（０，０，０，１），（１，１，０，１），（２，１，０，１）となる。この場合の解の要素の概念図を図１９に示す。
【００９６】
次に深さ１の基本制約条件のｘ２＝０として固定した場合の処理が終了したのみであるので、Ｓ４３０は「ＮＯ」へ進みＳ３９５へ戻る。
【００９７】
深さが１の全ての変数の要素の固定は終了していないので（Ｓ３９５）、深さ１のｘ２の要素をｘ２＝１として次に固定し（Ｓ４００）、ｘ２＝１として固定して再度再帰処理を行う。このように上記と同様に処理Ａ又は処理Ｂに帰着させる再帰処理を複数回反復することによって、ｘ２＝１として固定した場合の解の要素を算出することが可能となり、この場合の解は、（ｘ０，ｘ１，ｘ２，ｘ３）＝（１，０，１，０），（１，０，１，２），（３，１，１，０），（３，１，１，２）となる。この場合の解の要素の概念図を図２０に示す。
【００９８】
ｘ２＝１の解は全て算出できたので、同様にｘ２＝２として再度Ｓ４００で固定し、再帰処理を行う。上記と同様に処理Ａ又は処理Ｂに帰着させる再帰処理を複数回反復することによって、ｘ２＝２として固定した場合の解の要素を算出することが可能となり、この場合の解は、（ｘ０，ｘ１，ｘ２，ｘ３）＝（０，０，２，０），（０，１，２，０），（１，０，２，０）となる。この場合の解の要素の概念図を図２１に示す。
【００９９】
又Ｓ４２０でｘ２＝２として固定した場合の解の算出が行われ、Ｓ４３０では全ての変数の固定が終了したので、Ｓ４３０は「ＹＥＳ」へ進むこととなる。即ち基本制約条件の全ての解が算出できたこととなる。全ての解は上記から、（ｘ０，ｘ１，ｘ２，ｘ３）＝（０，０，０，１）、（０，０，２，０），（０，１，２，０），（１，０，１，０），（１，０，１，２），（３，１，１，０），（３，１，１，２），（０，０，２，０），（０，１，２，０），（１，０，２，０）となる。
【０１００】
以上のようにすれば不必要な解の要素の処理を行わずに高速に処理可能となる。又本発明の再帰処理では深さ優先探索であるので、どの項の処理から処理を開始しても構わない。更に処理Ｄについては、どのプロセスで行うかは任意に設定して良い。
【０１０１】
充足可能解算出手段４で全ての充足可能解を算出したので、出力手段５が当該解をデータベース６から抽出し（Ｓ１３０）、検索結果として出力を行う。
【０１０２】
【実施例２】
次に本発明の充足可能解列挙システム１を用いて自転車の部品の仕様設計を行う場合の説明を行う。当然のことながら自転車は一例に過ぎず、自動車、飛行機、オートバイ等の複数の部品からなり、それらを組み合わせる場合には使用できることは言うまでもない。更に部品の仕様設計を行う場合のみならず、複雑な条件を指定してその条件全てを満たす（充足する）ものを列挙するものであれば使用できる。
【０１０３】
本実施例では、自転車の生産計画に於ける部品の組合せを想定し、それぞれのオプション仕様の組合せに車種コードを与える。車種コード毎に、生産予定とするグレードを設定する。ここで設定した自転車群のオプション仕様に基づいて、適合する自転車の部品の仕様設計を行う。オプション仕様の概念図を図２２に示す。
【０１０４】
又各自転車は使用できる部品の使用が設定されており、それら全てが制約条件となる。この場合のオプション仕様の制約条件の一例を図２３に示す。本実施例では３２種類のオプション仕様が存在している場合を想定する。又オプション仕様は、セットオプションとして扱われることがある。セットオプションは、例えば代表仕様項目として「ランプ」、メンバー仕様項目として「レンズ」、「ランプケース」、「ランプ留め金」、「発電機」とのように、ランプを構成する各部品を示す。即ち代表仕様項目はメンバー仕様項目からなる。
【０１０５】
検索を行う者は、その制約条件を充足可能解列挙システム１の制約条件受信手段２から入力を行う。例えば図２４に示す設定選択パネルから各オプション仕様項目の制約条件の入力を行う。
【０１０６】
例えば設定選択パネルの「ランプ」を選択することによって、ランプ設定パネルが開き、「ランプ」の制約条件の入力が行える。図２５にランプ設定パネルの一例を示す。このランプ設定パネルから各マス目を選択することによって制約条件の存在の有無の入力となる。又代表者仕様項目から更に所定の操作によってメンバー仕様項目の制約条件の設定パネルを開き入力することが可能である。図２６にメンバー仕様項目「レンズ」のレンズ設定パネル、図２７にメンバー仕様項目「ランプケース」のランプケース設定パネル、図２８にメンバー仕様項目「ランプ留め金」のランプ留め金設定パネル、図２９にメンバー仕様項目「発電機」の発電機設定パネルの一例を示す。
【０１０７】
上記のように、各オプション仕様項目全てに対して制約条件を設定する。このようにして得られた制約条件の相互関係の一例を図３０に示す。図３０は、縦のオプション仕様と横のオプション仕様との間で制約条件があるか否かを示している画面である。例えば仕向地との間で制約条件があるオプション仕様は「ランプ」、「ハンドル」、「サドル」、「ベル」、「スタンド」である。又メンバー仕様項目は、代表者仕様項目を経由して車種仕様やグレード等のオプション仕様によって制約条件の影響を受けている。例えばメンバー仕様「レンズ」、「ランプケース」、「ランプ留め金」、「発電機」は代表者仕様項目「ランプ」と制約条件が存在し、代表者仕様項目「ランプ」は「仕向地」「フレーム」との間で制約条件が存在していることが判別できる。この概念を示したのが図３１である。
【０１０８】
制約条件を設定後、制約条件受信手段２が当該入力された制約条件を受信する（Ｓ１００）。検索を行う者が図２４に示した設定選択パネルの「充足可能解展開計算」ボタンを選択することによって、Ｓ１００で受信した制約条件に基づいて、連言標準形生成手段３が当該制約条件の連言標準形の生成を行う（Ｓ１１０）。
【０１０９】
連言標準形生成手段３で生成した連言標準形で示される制約条件に基づいて充足可能解算出手段４が、当該制約条件を満たす全ての解の組合せを算出する（Ｓ１２０）。全ての解の組合せを算出するプロセスは実施例１に示したとおりである。
【０１１０】
充足可能解算出手段４で算出した解の組合せに基づいて、出力手段５がデータベース６から検索結果の抽出を行い（Ｓ１３０）、検索結果の表示を行う。図３２に検索結果画面の一例を示す。検索結果画面の「はい」ボタンを選択することによって、より詳細な検索結果を閲覧することが出来る。図３３、図３４、図３５に詳細な検索結果の閲覧画面の一例を示す。図３３は当該制約条件の車種仕様とグレードの部分を示した画面であり、図３４は当該制約条件の「ランプ」「ハンドル」「サドル」「ベル」の部分を示した画面である。図３５は当該制約条件の「泥除け」「荷台」「テールランプ」「スタンド」の部分を示した画面である。尚これらの画面は同一の画面で表示されることが好適であるが、複数の画面に分けて表示されても構わない。見やすさに応じて適宜変更できることが好適である。
【０１１１】
このように検索を充足可能解列挙システム１に於いて検索を行わせることによって、複雑な制約条件であっても容易且つ高速に検索結果を抽出することが可能となる。
【０１１２】
本発明に於ける各手段、データベースは、その機能が論理的に区別されているのみであって、物理上あるいは事実上は同一の領域を為していても良い。又データベースの代わりにデータファイルであっても良いことは言うまでもなく、データベースとの記載にはデータファイルをも含んでいる。
【０１１３】
尚、本発明を実施するにあたり本実施態様の機能を実現するソフトウェアのプログラムを記録した記憶媒体をシステムに供給し、そのシステムのコンピュータが記憶媒体に格納されたプログラムを読み出し実行することによって実現されることは当然である。
【０１１４】
この場合、記憶媒体から読み出されたプログラム自体が前記した実施態様の機能を実現することとなり、そのプログラムを記憶した記憶媒体は本発明を当然のことながら構成することになる。
【０１１５】
プログラムを供給する為の記憶媒体としては、例えば磁気ディスク、ハードディスク、光ディスク、光磁気ディスク、磁気テープ、不揮発性のメモリカード等を使用することができる。
【０１１６】
又、コンピュータが読み出したプログラムを実行することにより、上述した実施態様の機能が実現されるだけではなく、そのプログラムの指示に基づき、コンピュータ上で稼働しているオペレーティングシステムなどが実際の処理の一部又は全部を行い、その処理によって前記した実施態様の機能が実現される場合も含まれることは言うまでもない。
【０１１７】
更に、記憶媒体から読み出されたプログラムが、コンピュータに挿入された機能拡張ボードやコンピュータに接続された機能拡張ユニットに備わる不揮発性あるいは揮発性の記憶手段に書き込まれた後、そのプログラムの指示に基づき、機能拡張ボードあるいは機能拡張ユニットに備わる演算処理装置などが実際の処理の一部あるいは全部を行い、その処理により前記した実施態様の機能が実現される場合も含まれることは当然である。
【０１１８】
【発明の効果】
本発明によって、組合せを検索する為の条件を充足可能解の列挙問題として定式化し、条件分岐によって生成される探索ツリーを深さ優先探索し、探索の浅いレベルで探索の必要性を調査し、不要な枝を早い段階で削減することによって探索を効率化することが可能となり、又複雑な制約条件を単純な制約条件に帰着させるような分岐を行い、単純な制約条件の集合になった際に依存関係グラフによって高速に解を求める充足可能解列挙システムが可能となる。
【０１１９】
本発明者が図３７に示した環境で処理時間に関するテストを行ったところ、仕様項目数（制約式の数）が４の場合には、本発明を用いて処理を行うと処理時間が４秒であり、リレーショナルデータベースを用いて処理を行うと処理時間が６秒、仕様項目数が９の場合には、本発明を用いて処理を行うと処理時間が３秒であり、リレーショナルデータベースを用いて処理を行うと処理時間が７秒、仕様項目数が３６の場合には、本発明を用いて処理を行うと処理時間が６分５３秒、リレーショナルデータベースを用いて処理を行うと処理時間が３３分７秒、仕様項目数が５４の場合には、本発明を用いて処理を行うと処理時間が６分２１秒、リレーショナルデータベースでは処理を行えず、仕様項目数が８３の場合には、本発明を用いて処理を行うと処理時間が４２秒、リレーショナルデータベースでは処理が行えなかった。尚、仕様項目数が多い方が少ない場合より処理時間が短い場合があるが、これは制約式、制約条件等によって変化する為である。当然同じ仕様項目数では、同じ条件で本発明とリレーショナルデータベースとの比較をしている。又リレーショナルデータベースでは、４０個以上の制約式を受け付けないので、処理そのものが不可能である。
【０１２０】
以上のようなテスト結果からも明らかなように、制約条件が複雑であるほど、本発明の著しい効果が現出し、特に制約式の数が４１個以上の場合には、従来のリレーショナルデータベースでは処理が行えないのに対し、本発明では処理が行え、且つ高速である。
【図面の簡単な説明】
【図１】本発明のシステム構成の一例を示したシステム構成図である。
【図２】本発明の全体のプロセスの流れの一例を示したフローチャート図である。
【図３】本発明の充足可能解算出のプロセスの流れの一例を示したフローチャート図である。
【図４】本発明の充足可能解算出のプロセスの流れの一例を示したフローチャート図である。
【図５】本発明の充足可能解算出のプロセスの流れの一例を示したフローチャート図である。
【図６】依存関係グラフの概念図である。
【図７】図６からｘ２を除いた場合の依存関係グラフの概念図である。
【図８】図７からｘ１を除いた場合の依存関係グラフの概念図である。
【図９】処理Ｂに於ける依存関係グラフの概念図である。
【図１０】処理Ｄに於ける依存関係グラフの概念図である。
【図１１】制約条件の概念図である。
【図１２】ｘ２を固定した場合の概念図である。
【図１３】ｘ３＝１として決定した場合の制約条件の概念図である。
【図１４】ｘ０＝０∪ｘ１＝１の場合の依存関係グラフの概念図である。
【図１５】ｘ０＝１∪ｘ０＝２∪ｘ１＝０の場合の依存関係グラフの概念図である。
【図１６】第２項と第１項の依存関係グラフを重ね合わせた概念図である。
【図１７】ｘ０＝３として固定した場合の概念図である。
【図１８】第２項の解の要素の概念図である。
【図１９】ｘ２＝０として固定した場合の解の要素の概念図である。
【図２０】ｘ２＝１として固定した場合の解の要素の概念図である。
【図２１】ｘ２＝２として固定した場合の解の要素の概念図である。
【図２２】オプション仕様の概念図である。
【図２３】オプション仕様の制約条件の一例である。
【図２４】設定選択パネルの一例である。
【図２５】ランプ設定パネルの一例である。
【図２６】レンズ設定パネルの一例である。
【図２７】ランプケース設定パネルの一例である。
【図２８】ランプ留め金設定パネルの一例である。
【図２９】発電機設定パネルの一例である。
【図３０】制約条件の相互関係の一例である。
【図３１】制約条件の相互関係の概念を示した図である。
【図３２】結果表示画面の一例である。
【図３３】制約条件の車種仕様とグレードの部分を示した画面の一例である。
【図３４】制約条件の「ランプ」「ハンドル」「サドル」「ベル」の部分を示した画面の一例である。
【図３５】制約条件の「泥除け」「荷台」「テールランプ」「スタンド」の部分を示した画面の一例である。
【図３６】充足可能解算出の概略を示したフローチャート図である。
【図３７】テスト結果を示した図である。
【符号の説明】
１：充足可能解列挙システム
２：制約条件受信手段
３：連言標準形生成手段
４：充足可能解算出手段
５：出力手段
６：データベース
【図１】
2004280523.tif 000003
【図２】
2004280523.tif 000004
【図３】
2004280523.tif 000005
【図４】
2004280523.tif 000006
【図５】
2004280523.tif 000007
【図６】
2004280523.tif 000008
【図７】
2004280523.tif 000009
【図８】
2004280523.tif 000010
【図９】
2004280523.tif 000011
【図１０】
2004280523.tif 000012
【図１１】
2004280523.tif 000013
【図１２】
2004280523.tif 000014
【図１３】
2004280523.tif 000015
【図１４】
2004280523.tif 000016
【図１５】
2004280523.tif 000017
【図１６】
2004280523.tif 000018
【図１７】
2004280523.tif 000019
【図１８】
2004280523.tif 000020
【図１９】
2004280523.tif 000021
【図２０】
2004280523.tif 000022
【図２１】
2004280523.tif 000023
【図２２】
2004280523.tif 000024
【図２３】
2004280523.tif 000025
【図２４】
2004280523.tif 000026
【図２５】
2004280523.tif 000027
【図２６】
2004280523.tif 000028
【図２７】
2004280523.tif 000029
【図２８】
2004280523.tif 000030
【図２９】
2004280523.tif 000031
【図３０】
2004280523.tif 000032
【図３１】
2004280523.tif 000033
【図３２】
2004280523.tif 000034
【図３３】
2004280523.tif 000035
【図３４】
2004280523.tif 000036
【図３５】
2004280523.tif 000037
【図３６】
2004280523.tif 000038
【図３７】
2004280523.tif 000039