(57)【要約】【課題】ＱＢＦの充足可能性を判定する際に使用されるＱＢＦ技法を提供する。【解決手段】ＱＢＦは、充足可能性（ＳＡＴ）ソルバによって分析可能な構成要素部に分解される。その場合、各構成要素は、独立に、おそらくは並列に、充足可能性のために分析される。構成要素が充足不能である場合、ＱＢＦは充足不能であると判定され、分析が中止される。構成要素が充足可能である場合、充足可能な構成要素に対応する割り当てが書き留められる。構成要素が充足可能である場合、それが別の未テストの構成要素に追加されて、組合せ構成要素が提供され、組合せ構成要素の充足可能性が分析される。そのような追加および分析は、ＱＢＦが完了され、充足可能と判定されるか、または充足不能と判定されるまで繰り返される。【選択図】図２
2006202288.tif 000002
【特許請求の範囲】
【請求項１】
限量記号付きブール式（ＱＢＦ）の充足可能性を判定する方法であって、
ＱＢＦを受け取るステップと、
前記ＱＢＦを充足可能性（ＳＡＴ）ソルバによって分析可能な複数の構成要素部に分解するステップと、
前記ＳＡＴソルバによって各構成要素の充足可能性を独立に分析するステップと
を含むことを特徴とする方法。
【請求項２】
構成要素が充足不能である場合、前記ＱＢＦは充足不能であると判定し、前記分析を中止することを特徴とする請求項１に記載の方法。
【請求項３】
構成要素が充足可能である場合、前記充足可能な構成要素に対応する割り当てを記憶することを特徴とする請求項１に記載の方法。
【請求項４】
前記充足可能な構成要素を別の未テストの構成要素に追加して、組合せ構成要素を提供するステップと、
前記組合せ構成要素の充足可能性を分析するステップと
をさらに含むことを特徴とする請求項３に記載の方法。
【請求項５】
前記ＱＢＦが完了され、充足可能と判定されるか、または充足不能と判定されるまで、前記分析および追加を繰り返すステップをさらに含むことを特徴とする請求項４に記載の方法。
【請求項６】
前記ＱＢＦは全称記号または存在記号の少なくとも一方を含むことを特徴とする請求項１に記載の方法。
【請求項７】
前記ＱＢＦがその割り当ての下で真と評価されるような、すべての束縛ブール変数に対する割り当てが存在する場合、前記ＱＢＦは充足可能であることを特徴とする請求項１に記載の方法。
【請求項８】
前記各構成要素の充足可能性を独立に分析するステップは並列に実行されることを特徴とする請求項１に記載の方法。
【請求項９】
限量記号付きブール式（ＱＢＦ）を解く方法であって、
ＱＢＦを受け取るステップと、
前記ＱＢＦを１組の命題ブール式の充足可能性問題に帰着するステップと、
前記命題ブール式の充足可能性問題を解くステップと
を含むことを特徴とする方法。
【請求項１０】
前記解くステップは充足可能性（ＳＡＴ）ソルバによって実行されることを特徴とする請求項９に記載の方法。
【請求項１１】
前記解くステップは前記命題ブール式の充足可能性問題を並列に再帰的に解くステップを含むことを特徴とする請求項９に記載の方法。
【請求項１２】
前記ＱＢＦは全称記号または存在記号の少なくとも一方を含むことを特徴とする請求項９に記載の方法。
【請求項１３】
限量記号付きブール式（ＱＢＦ）を解く方法であって、
ＱＢＦを命題ブール式に抽象化するステップと、
前記ブール式を解くステップと
を含むことを特徴とする方法。
【請求項１４】
前記抽象化するステップは限量記号を含む部分式を変数で置き換えるステップを含むことを特徴とする請求項１３に記載の方法。
【請求項１５】
前記ブール式を解くステップ後に、前記抽象化部分式のために割り当てられた前記変数を再帰的に正当化するステップをさらに含むことを特徴とする請求項１４に記載の方法。
【請求項１６】
前記正当化するステップが成功した場合、前記ＱＢＦが解かれることを特徴とする請求項１５に記載の方法。
【請求項１７】
前記正当化するステップが不成功だった場合、前記命題ブール式に制約を追加することによって前記抽象化を洗練するステップと、
前記ブール式を解くことを繰り返すステップと
をさらに含むことを特徴とする請求項１５に記載の方法。
【請求項１８】
前記制約は前記正当化するステップから決定されることを特徴とする請求項１７に記載の方法。
【請求項１９】
前記解くステップは充足可能性（ＳＡＴ）ソルバによって実行されることを特徴とする請求項１３に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は一般に、計算の分野に関し、より詳細には、限量記号付きブール式の充足可能性問題（quantified Boolean formula satisfiability problem）に関する。
【背景技術】
【０００２】
命題ブール式の充足可能性（ＳＡＴ）問題は、ソフトウェアおよびハードウェア検証、ならびにコンピュータ支援設計を含む、多くのアプリケーションで使用される。多くの先進のソフトウェア解析ツールは、それらの推論エンジンでＳＡＴ解決（SAT solving）を使用する。
【０００３】
命題ブール式は、論理演算子によって結合されたブール変数から成る。演算子の例として、論理積（∧）、論理和（∨）、および論理否定（¬）が挙げられる。そのような式が与えられたとき、ＳＡＴ問題は、その式がある割り当ての下で真と評価されるような、変数への値割り当てが存在するかを問う。ＳＡＴ問題は、ＮＰ完全（NP-Complete）であることが知られている。効率的にＳＡＴ問題を解くための多くのアルゴリズムが存在する。本明細書で用いるように、命題ブール式は、単にブール式と呼ばれる。
【発明の開示】
【発明が解決しようとする課題】
【０００４】
限量記号付きブール式（ＱＢＦ）は、限量記号を含むブール式のより一般的な形式である。限量記号の例として、全称記号∀および存在記号∃が挙げられる。ＱＢＦの充足可能性問題は、ＰＳＰＡＣＥ完全（PSPACE-complete）であり、ＮＰ完全よりも計算的に難しいと考えられている。従来のＱＢＦアルゴリズムは、多くの現実世界の応用に対してうまく機能しない。より効果的なＱＢＦ技法が望まれている。
【０００５】
ＱＢＦ解決に対して広く使用されている手法の１つは、変換後にＳＡＴソルバ（SAT solver）によって解くことができる限量記号無しブール式（quantifier-free Boolean formula）にＱＢＦ式を変換することである。しかし、従来は限量記号を除去するためにこの種の変換が実行されるたび、より大きな式が生じる結果となり、それは望ましくない。
【０００６】
上記の事柄に鑑みて、かかる欠点を克服するシステムおよび方法が必要とされている。
【課題を解決するための手段】
【０００７】
以下では、本発明の様々な態様についての概要を提供する。本発明のすべての態様についての網羅的な説明を提供することも、本発明の範囲を確定することも意図されてはいない。むしろ、後続の詳細な説明および図面に対する導入として役立つよう意図されている。
【０００８】
本発明の例示的な実施形態は、ＱＢＦの充足可能性を判定する際にＱＢＦ技法を使用するシステムおよび方法に関する。反例駆動学習手順（counter-example driven learning procedure）は、抽象と洗練を結び付ける。充足可能性問題は、並列に再帰的に解かれる１組の類似した、ただしより小さく、より単純な下位問題に帰着される。
【０００９】
ＱＢＦの充足可能性を判定するためのシステムおよび方法例は、ＱＢＦを受け取ることと、次いで、各構成要素が充足可能性（ＳＡＴ）ソルバによって分析可能になるまでＱＢＦを複数の構成要素部に再帰的に分解することを含む。構成要素は、１つの命題ブール式部と、子構成要素（child component）の集合とから成る。構成要素は、その子構成要素のすべてを充足不能にする、その命題式部の充足可能な割り当てが存在する場合に限り充足可能である。その場合、各子構成要素は、独立に、おそらくは並列に、充足可能性に関して再帰的に分析される。
【００１０】
本発明の態様によれば、構成要素は、その命題式部の充足可能な割り当て候補を見つけるためにＳＡＴソルバを呼び出し、その子構成要素のすべてにその候補を提示する。ＳＡＴソルバがそのような候補を見つけることができない場合、この構成要素は、充足不能であると判定される。提示された割り当ての下ですべての子構成要素が充足不能である場合、この構成要素は、充足可能であり、その割り当て候補は、その構成要素の充足可能な割り当てとなると結論される。提示された割り当ての下で子構成要素の全部または一部が充足可能である場合、それらが充足される理由が抽出され、構成要素に加えられる。提示、分析、および学習というこのプロセスは、望ましくは、構成要素が充足可能と判定されるか、または充足不能と判定されるまで繰り返される。
【００１１】
システムおよび方法例は、ＱＢＦを１組の命題ブール式の充足可能性問題に帰着し、命題ブール式の充足可能性問題を望ましくはＳＡＴソルバを使用して解くことによって、ＱＢＦを解くことにも関する。そのような解決は、再帰的かつ並列に実行され得る。
【００１２】
本発明のさらなる特徴および利点は、添付図面を参照しながら進められる、例示的な実施形態についての以下の詳細な説明から明らかにされる。
【００１３】
好ましい実施形態についての以下の詳細な説明と同様、上記内容も、添付図面と併せて読まれることでより良く理解される。本発明を図説する目的で、図面には本発明の例示的な構成が示されているが、本発明は、開示される具体的な方法および手段に限定されるものではない。
【発明を実施するための最良の形態】
【００１４】
主題は法定の要件を満たすために特異性をもって説明される。しかし、説明自体は、本特許の範囲を限定しようとするものではない。むしろ、発明者らは、特許請求された主題が、別の既存のまたは将来の技術と併用される、本明細書で説明されたものに類似する異なるステップまたはステップの組合せを含むその他の方法によって実施され得ることも企図している。さらに、「ステップ」という用語は、利用される方法の異なる要素を暗示するために本明細書では使用され得るが、個々のステップの順序が明示的に記されない限り、また記されたときを除き、この用語は、本明細書で開示される様々なステップ間に何か特定の順序を意味するものと解釈されてはならない。
【００１５】
本明細書で用いられるように、以下のシンボルが定められている。∨は論理和、∧は論理積、¬は論理否定（否定）である。典型的な限量記号としては、∀および∃によってそれぞれ表される、全称記号および存在記号が挙げられる。
【００１６】
限量記号付きブール式（ＱＢＦ）は、限量記号を含むブール式の一般化形式である。限量記号は、全称記号または存在記号とすることができる。定義されているように、全称記号∀ｘｆ（ｘ）＝ｆ（真）∧ｆ（偽）であり、存在記号∃ｘｆ（ｘ）＝ｆ（真）∨ｆ（偽）である。限量化された変数は、束縛変数と呼ばれ、限量化されていない変数は、自由変数と呼ばれる。例えば、Ｐ（ｘ）∧∀ｙＱ（ｘ，ｙ）は、ＱＢＦである。この例では、変数ｙが束縛変数であり、ｘが自由変数である。ＱＢＦは、その割り当ての下で式が真と評価されるような、全（自由）ブール変数に対する割り当てが存在するならば充足可能である。ＱＢＦの充足可能性問題とは、ＱＢＦが充足可能かどうかを判定するものであり、充足可能なときは、少なくとも１つのそのような割り当てを与えるものである。
【００１７】
形式的に、ＱＢＦの構文は、以下のように定義される。  
ｆ：：＝ｘ｜¬ｆ｜ｆ∧ｇ｜ｆ∨ｇ｜∀ｘｆ｜∃ｘｆ
ここで、ｘはブール変数を表し、ｆおよびｇはブール式を表す。存在記号は、恒等式∃ｘｆ＝¬∀ｘ¬ｆを適用することによって除去することができるので、これ以降の説明では、ＱＢＦは存在限量を含まないと仮定する。以下で説明される技法に適切な変更を施すことで、代わりに全称記号が除去され得ることが企図されている。
【００１８】
ＱＢＦ式は、すべての可能な割り当ての下で式が真と評価される場合、恒真である。式が恒真であるかどうかを判定することが望ましい。式は、その否定が充足不能な場合に限り、恒真である。
【００１９】
従来のＳＡＴソルバは、より単純なブール式の充足可能性問題を取り扱う。本発明の態様は、ＱＢＦの充足可能性を、ＳＡＴソルバによって解くことができる１組の命題ブール式の充足可能性問題に帰着する。上で述べたように、ＱＢＦ式を限量記号が存在しないブール式に変形することが望ましい。最も一般的に用いられる技法は、∀および∃の定義を使用した展開である。しかし、限量記号を除去するために展開が実行されるたび、より大きな式が生じる結果となり、それは望ましくない。本発明の実施形態は、展開することを回避し、式が充足可能であるかどうかを効率的に判定する。
【００２０】
言い換えれば、式Ｐ（ｘ，ｙ，ｚ）が恒真（真）であることを証明するのが望ましく、その場合、この式はｘ、ｙ、ｚのすべての可能な値に対して真である。式は¬Ｐ（ｘ，ｙ，ｚ）の充足可能性問題に変換される。¬Ｐ（ｘ，ｙ，ｚ）が充足不能であるならば、Ｐ（ｘ，ｙ，ｚ）は恒真である。Ｐが限量記号を含む場合、これは複雑になる。従来技術の技法の１つは、展開を使用するものであるが、それは望ましくない。
【００２１】
図１は、本発明の態様を説明する際に有用な高水準ブロック図である。ＱＢＦは、ＱＢＦソルバ１０に提供される。ＱＢＦソルバ１０は、本明細書で説明される技法例を使用して、ＱＢＦが充足可能かどうかを判定する。ＱＢＦが充足可能なときに、１つまたは複数の充足可能な割り当てを提供することが、しばしば望ましい。
【００２２】
図２は、本発明による例示的なシステムのブロック図である。図２に示されたシステムの全部または一部は、ＱＢＦソルバ１０などのＱＢＦソルバ内に含まれ得る。ＱＢＦレシーバ２００は、ＱＢＦを受け取るように適合される。ＱＢＦアナライザ２２０は、ＱＢＦを分析し、例えば充足可能性（ＳＡＴ）ソルバ２４０による後続の分析および解決のため、ＱＢＦを適切な構成要素に分解する。ＳＡＴソルバはよく知られており、本明細書でさらに説明されるように、望ましい解に達するため、任意の適切なＳＡＴソルバが使用されてよい。その後、ＱＢＦの充足可能性または充足不能性の判定は、出力２６０を介して提供される。
【００２３】
図３は、本発明によるＱＢＦを解く例示的な方法の流れ図である。ＱＢＦは、ステップ３００で受け取られ、例えば手続きＢｕｉｌｄＣｏｍｐｏｎｅｎｔを呼び出すことによって、ステップ３１０で１組の構成要素に帰着される。その後、例えば手続きＳｏｌｖｅＣｏｍｐｏｎｅｎｔを呼び出すことによって、ステップ３２０で構成要素の充足可能性が解かれる。例示的なＢｕｉｌｄＣｏｍｐｏｎｅｎｔおよびＳｏｌｖｅＣｏｍｐｏｎｅｎｔの詳細が、本明細書で説明される。ＢｕｉｌｄＣｏｍｐｏｎｅｎｔおよびＳｏｌｖｅＣｏｍｐｏｎｅｎｔは例にすぎず、これらの手続きは、要求に応じて組み合わせられ、かつ／または構築され得ることが企図されている。
【００２４】
図４は、充足可能性が元のＱＢＦと同一である構成要素にＱＢＦ式を変換する例示的な方法の流れ図である。形式的に、構成要素は、ブール式と子構成要素の集合から成るように再帰的に定義される。ステップ４００で、ＱＢＦ式ｆが受け取られ、子構成要素の集合ｓは最初、空に設定される。
【００２５】
ステップ４１０でｆが限量記号を含まないと判断された場合、手続きはステップ４９０で結果として生じる構成要素を出力し、ステップ４９５で終了する。反対にｆが限量記号を含むと判断された場合、ステップ４２０で手続きは∀ｘｇによって表されるｆの部分式を見つける。部分式∀ｘｇは、望ましくはトップレベルであり、これは∀ｘｇが∀ｙｈの形式の別の部分式の部分式であることができないことを意味する。
【００２６】
ステップ４３０で、新しいブール変数ｕが部分式∀ｘｇのために導入され、ｆ内に出現するすべての∀ｘｇを変数ｕで置き換えることによって、新しい式ｆuが生成される。その後、手続きはｆをｆu∧（ｕ∨¬ｇ）と書き改める。ステップ４４０で、式ｕ∧¬ｇに対応する構成要素が子構成要素として再帰的に構成され、追加される。ステップ４１０から４４０は、ｆが限量記号を含まなくなるまで繰り返される。
【００２７】
図５は、本発明による構成要素の充足可能性を判定する例示的な方法の流れ図である。ブール式ｆおよび子構成要素の集合ｓからなる構成要素が、ステップ５００で受け取られる。ステップ５１０で、ブール式ｆの充足可能性が、望ましくはＳＡＴソルバによって解かれる。
【００２８】
ステップ５１０でｆが充足不能であると判断された場合、ステップ５９０で構成要素は充足不能であると結論され、手続きはステップ５９５で終了する。反対にステップ５１０でｆが充足可能であると判断された場合、ステップ５２０で充足可能な割り当てａが書き留められ、すなわち記憶され、ステップ５３０で充足可能な割り当てが子構成要素の各々に結合され、各組合せが独立に、おそらくは並列にテストされる。すべての子構成要素が充足不能であると判断された場合、元の構成要素は充足可能であると判定され、ステップ５８０で充足可能な割り当てａが戻り値として返され、手続きはステップ５８５で終了する。反対に子構成要素の全部または一部が充足可能である場合、そのような構成要素の１つ＜ｆ1，ｓ1＞と、その充足可能な割り当ての１つｂがステップ５５０で選択される。元の構成要素のブール式ｆは、ブール式ｆ1と割り当てｂとで結合されたｆによって置き換えられる。ステップ５１０から５５０は、構成要素がステップ５９０で充足不能であると判定されるか、またはステップ５８０で充足可能であると判定されるまで繰り返される。
【００２９】
図１から図５で参照されるような本発明の態様は、以下の例に関してさらに説明される。例えば、Ｈ（ｘ）：Ｐ（ｘ）∧∀ｙＱ（ｘ，ｙ）のように限量記号を含む式Ｈ（ｘ）を仮定した場合、この式の充足可能性を判定することが望ましい。式Ｈ（ｘ）が充足可能であるならば、式中の∧の被演算子（すなわち、Ｐ（ｘ）および∀ｙＱ（ｘ，ｙ））はともに充足されなければならない。
【００３０】
図３にしたがって、Ｈ（ｘ）に対応する構成要素が構成される。図４にしたがって、新しい変数ｕが∀ｙＱ（ｘ，ｙ）のために導入される。構成要素のブール式ｆは、Ｐ（ｘ）∧ｕ∧（ｕ∨¬Ｑ（ｘ，ｙ））であり、子構成要素の集合は、構成要素＜ｕ∧¬Ｑ（ｘ，ｙ），｛｝＞から成る単集合である。その後、構成された構成要素の充足可能性が、図５にしたがって判定される。ｆの充足可能性が、最初にＳＡＴソルバによって判定される。ｆが充足不能である場合、式Ｈ（ｘ）全体が充足可能ではないと判定される。
【００３１】
反対にｆが充足可能である場合、ｆの充足可能な割り当てが選択され、その子構成要素の充足可能性を判定するのに使用される。この例の場合、ｘおよびｕのための充足可能な割り当てを、それぞれａxおよびａuとする。この割り当ては、１つの子構成要素＜ｕ∧¬Ｑ（ｘ，ｙ），｛｝＞の充足可能性を判定するのに使用される。
【００３２】
＜ｕ∧¬Ｑ（ｘ，ｙ），｛｝＞の充足可能性を割り当てａxおよびａuの下で判定するため、図５で説明された手続きが再び呼び出される。しかし、この場合、この子構成要素は子構成要素を含んでいない。この子構成要素が充足不能であると判定された場合、元のＱＢＦ式は充足可能な割り当てａxによって充足可能であると判定される。
【００３３】
反対にこの子構成要素が割り当てａxおよびａuの下で充足可能である場合、充足可能な割り当てが返される。充足可能な割り当ては変数ｙ用であり、ａyによって表される。元の構成要素のブール式ｆは更新される。図５のステップ５５０の表記では、ｆ1がｕ∧¬Ｑ（ｘ，ｙ）であり、ｂがａyであるので、新しいブール式ｆは、Ｐ（ｘ）∧ｕ∧（ｕ∨¬Ｑ（ｘ，ｙ））∧¬（ｕ∧¬Ｑ（ｘ，ａy））となる。充足可能性が判定されるまで、手続きは新しいｆを用いて繰り返される。
【００３４】
このように、ＱＢＦの充足可能性問題に対する技法が提供される。ＱＢＦの充足可能性を判定するための擬似コードによるアルゴリズム設計例が以下に提供されている。技法例は、元の式の構造を利用して、ＱＢＦ問題を１組のより小さな（Ｑ）ＢＦ問題に分解し、その後、（Ｑ）ＢＦ問題は並列に解かれる。
【００３５】
ＱＢＦの構成要素構造を組み立てるための例示的な手続きは以下の通りである。ＢｕｉｌｄＣｏｍｐｏｎｅｎｔ（ｆ）は、ＱＢＦ  ｆに対応する構成要素を生成する。結果として生じる構成要素は、ブール式である第１の要素と構成要素の集合である第２の要素の１組として表される。  
ＢｕｉｌｄＣｏｍｐｏｎｅｎｔ（ｆ）｛
ｓ＝｛｝；
ｗｈｉｌｅ（ｆが限量記号を含む）｛
ｈ＝ｆのトップレベルの部分式∀ｘｇを選択する；
ｕ＝ｈの新しい変数；
ｆu＝出現するｈをすべてｕによって置き換えたｆ；
ｆ＝ｆu∧（ｕ∨¬ｇ）；
ｓ＝ｓ∪｛ＢｕｉｌｄＣｏｍｐｏｎｅｎｔ（ｕ∧¬ｇ）｝；
｝
ｒｅｔｕｒｎ  ＜ｆ，ｓ＞；
｝
【００３６】
構成要素を解くための例示的な判定手続きは以下の通りである。ＳｏｌｖｅＣｏｍｐｏｎｅｎｔ（ｃ）は、入力構成要素ｃが充足可能かどうかを判定する。ｃが充足可能であるならば、ＳｏｌｖｅＣｏｍｐｏｎｅｎｔ（ｃ）は充足可能な割り当てを生成する。以下の手続きではＳＡＴソルバＳｏ１ｖｅＳＡＴが利用可能であると仮定している。ブール式ｆが与えられたとき、ＳｏｌｖｅＳＡＴ（ｆ）は、ｆが充足不能である旨を報告するか、または式ｆの充足可能な割り当てａを返す。  
ＳｏｌｖｅＣｏｍｐｏｎｅｎｔ（ｃ）｛
ｆ＝ｃのブール式；
ｓ＝ｃの子構成要素の集合；
ｗｈｉｌｅ（ｔｒｕｅ）｛
ａ＝ＳｏｌｖｅＳＡＴ（ｆ）；
ｉｆ（ａは充足不能）｛
ｒｅｔｕｒｎ  充足不能；
｝
ｄｏｎｅ＝ｔｒｕｅ；
ｆｏｒｅａｃｈ（ｓの中のｃ１）ｄｏ｛
ａ１＝ＳｏｌｖｅＣｏｍｐｏｎｅｎｔ（ｃ１（ａ））；
ｉｆ（ａ１は充足可能）｛
ｆ１＝ｃ１のブール式；
ｆ＝ｆ∧¬ｆ１（ａ１）；
ｄｏｎｅ＝ｆａｌｓｅ；
ｇｏｔｏ  ＬＯＯＰ＿ＥＮＤ；
｝
｝
ＬＯＯＰ＿ＥＮＤ：ｉｆ（ｄｏｎｅ）｛
ｒｅｔｕｒｎ  ｆは充足可能であり、充足可能な割り当てはａ；
｝
｝
｝
【００３７】
ＱＢＦを解くための判定手続きは以下の通りである。  
ＳｏｌｖｅＱＢＦ（ｆ）｛
ｃ＝ＢｕｉｌｄＣｏｍｐｏｎｅｎｔ（ｆ）；
ｒｅｔｕｒｎ  ＳｏｌｖｅＣｏｍｐｏｎｅｎｔ（ｃ）；
｝
【００３８】
（コンピューティング環境例）
図６および以下の説明は、本発明の例示的な実施形態を実施できる適切なコンピューティング環境についての簡潔で概略的な説明を提供することを意図している。しかし、本発明に関連して、ハンドヘルド、ポータブル、およびその他のすべての種類のコンピューティング装置の使用が企図されていることを理解されたい。以下では汎用コンピュータについて説明がなされるが、これは一例にすぎない。本発明は、ネットワークサーバと相互運用性を有し、対話を行うシンクライアントでも動作可能である。したがって、本発明の例示的な実施形態は、クライアント資源が非常に僅かまたは最低限しか含まれないネットワーク化されたホストサービス環境、例えば、クライアント装置がワールドワイドウェブへのブラウザまたはインターフェースとしてのみ機能するネットワーク環境で実施することができる。
【００３９】
必ずしも必要というわけではないが、本発明は、開発者または試験者による使用のため、アプリケーションプログラミングインターフェース（ＡＰＩ）を介して実施することができ、かつ／または１つまたは複数のコンピュータ（例えば、クライアントワークステーション、サーバ、またはその他の装置）によって実行されるプログラムモジュールなどのコンピュータ実行可能命令の一般的コンテキスト内で説明されるネットワーク閲覧ソフトウェアに含めることができる。通常、プログラムモジュールは、特定のタスクを実行し、あるいは特定の抽象データ型を実装するルーチン、プログラム、オブジェクト、コンポーネント、およびデータ構造などを含む。一般に、プログラムモジュールの機能は、様々な実施形態での要求に応じて、組み合わされてもよく、分散されてもよい。さらに、本発明がその他のコンピュータシステム構成によっても実施できることは、当業者であれば理解されよう。本発明と共に使用するのに適し得るその他のよく知られたコンピューティングシステム、環境、および／または構成は、パーソナルコンピュータ（ＰＣ）、現金自動預払機、サーバコンピュータ、ハンドヘルドまたはラップトップ装置、マルチプロセッサシステム、マイクロプロセッサベースシステム、プログラム可能家電、ネットワークＰＣ、ミニコンピュータ、およびメインフレームコンピュータなどを含むが、これらに限定されるものではない。本発明の実施形態は、通信ネットワークまたはその他のデータ伝送媒体によって接続されたリモート処理装置でタスクが実行される分散コンピューティング環境で実施することもできる。分散コンピューティング環境では、プログラムモジュールは、メモリ記憶装置を含むローカルおよびリモートコンピュータ記憶媒体の両方に配置することができる。
【００４０】
したがって、図６は、本発明を実施し得る適切なコンピューティングシステム環境１００の一例を示すものであるが、上で明らかにされたように、コンピューティングシステム環境１００は、適切なコンピューティング環境の一例であるにすぎず、本発明の使用または機能の範囲に関して何らの限定も意味するものではない。例示的な動作環境１００に示された構成要素のいずれか１つまたは組合せに関して、本発明が何らかの依存または要求を有すると解釈されるべきではない。
【００４１】
図６を参照すると、本発明を実施するためのシステム例は、コンピュータ１１０の形態の汎用コンピューティング装置を含む。コンピュータ１１０のコンポーネントには、プロセッシングユニット１２０、システムメモリ１３０、およびシステムメモリを含む様々なシステムコンポーネントをプロセッシングユニット１２０に連結するシステムバス１２１が含まれ得るが、これらに限定されるものではない。システムバス１２１は、メモリバスまたはメモリコントローラ、周辺バス、および様々なバスアーキテクチャのいずれかを使用するローカルバスを含む複数のタイプのバス構造のいずれであってもよい。例えば、そのようなアーキテクチャには、業界標準アーキテクチャ（ＩＳＡ）バス、マイクロチャネルアーキテクチャ（ＭＣＡ）バス、拡張ＩＳＡ（ＥＩＳＡ）バス、ビデオ電子規格協会（ＶＥＳＡ）ローカルバス、および（メザニンバスとしても知られる）周辺コンポーネント相互接続（ＰＣＩ）バスが含まれるが、これらに限定されるものではない。
【００４２】
コンピュータ１１０は一般に、様々なコンピュータ可読媒体を含む。コンピュータ可読媒体は、コンピュータ１１０によってアクセス可能な任意の利用可能媒体とすることができ、揮発性および不揮発性媒体、着脱可能および着脱不能媒体が含まれる。例えば、コンピュータ可読媒体として、コンピュータ記憶媒体と通信媒体を挙げることができるが、これらに限定されるものではない。コンピュータ記憶媒体には、コンピュータ可読命令、データ構造、プログラムモジュール、またはその他のデータといった情報を記憶するための任意の方法または技法で実施される、揮発性および不揮発性媒体、着脱可能および着脱不能媒体が含まれる。コンピュータ記憶媒体には、ランダムアクセスメモリ（ＲＡＭ）、読み取り専用メモリ（ＲＯＭ）、電気的消去可能なプログラム可能読み取り専用メモリ（ＥＥＰＲＯＭ）、フラッシュメモリ、もしくはその他のメモリ技術、コンパクトディスク読み取り専用メモリ（ＣＤＲＯＭ）、デジタル多用途ディスク（ＤＶＤ）、もしくはその他の光ディスク記憶、磁気カセット、磁気テープ、磁気ディスク記憶、もしくはその他の磁気記憶装置、または所望の情報を記憶するのに使用でき、コンピュータ１１０によってアクセスできる、その他の任意の媒体が含まれるが、これらに限定されるものではない。
【００４３】
システムメモリ１３０は、ＲＯＭ１３１およびＲＡＭ１３２などの、揮発性および／または不揮発性メモリの形態をとるコンピュータ記憶媒体を含む。基本入出力システム（ＢＩＯＳ）１３３は、起動中などにコンピュータ１１０内の要素間の情報伝送を助ける基本ルーチンを含み、一般にＲＯＭ１３１に保存される。ＲＡＭ１３２は一般に、プロセッシングユニット１２０が直ちにアクセス可能であり、かつ／または現在それに基づいて動作している、データおよび／またはプログラムモジュールを含む。例えば、図６には、オペレーティングシステム１３４、アプリケーションプログラム１３５、その他のプログラムモジュール１３６、およびプログラムデータ１３７が示されているが、これらに限定されるものではない。ＲＡＭ１３２は、その他のデータおよび／またはプログラムモジュールを含むこともできる。
【００４４】
コンピュータ１１０はまた、その他の着脱可能／着脱不能、揮発性／不揮発性コンピュータ記憶媒体も含む。図６には、着脱不能な不揮発性の磁気媒体に対して読み書きを行うハードディスクドライブ１４１、着脱可能な不揮発性の磁気ディスク１５２に対して読み書きを行う磁気ディスクドライブ１５１、およびＣＤＲＯＭまたはその他の光媒体などの着脱可能な不揮発性の光ディスク１５６に対して読み書きを行う光ディスクドライブ１５５が、一例として示されている。動作環境例で使用可能なその他の着脱可能／着脱不能、揮発性／不揮発性コンピュータ記憶媒体には、磁気テープカセット、フラッシュメモリカード、デジタル多用途ディスク、デジタルビデオテープ、ソリッドステートＲＡＭ、およびソリッドステートＲＯＭなどが含まれるが、これらに限定されるものではない。ハードディスクドライブ１４１は一般に、インターフェース１４０などの着脱不能メモリインターフェースを介してシステムバス１２１に接続され、磁気ディスクドライブ１５１および光ディスクドライブ１５５は一般に、インターフェース１５０などの着脱可能メモリインターフェースによってシステムバス１２１に接続される。
【００４５】
上述した、図６に示すドライブおよびそれに関連するコンピュータ記憶媒体は、コンピュータ可読命令、データ構造、プログラムモジュール、およびその他のデータの記憶保持をコンピュータ１１０に提供する。図６には、例えば、オペレーティングシステム１４４、アプリケーションプログラム１４５、その他のプログラムモジュール１４６、およびプログラムデータ１４７を記憶するハードディスクドライブ１４１が示されている。これらのコンポーネントは、オペレーティングシステム１３４、アプリケーションプログラム１３５、その他のプログラムモジュール１３６、およびプログラムデータ１３７と同じでもよく、異なってもよいことに留意されたい。オペレーティングシステム１４４、アプリケーションプログラム１４５、その他のプログラムモジュール１４６、およびプログラムデータ１４７には、少なくともそれらが異なるコピーであることを示すため、図６では異なる番号が振られている。ユーザは、キーボード１６２、および一般にマウス、トラックボール、またはタッチパッドと呼ばれるポインティングデバイス１６１などの入力装置を介して、コンピュータ１１０にコマンドおよび情報を入力することができる。その他の入力装置（図示せず）として、マイクロフォン、ジョイスティック、ゲームパッド、衛星放送受信アンテナ、またはスキャナなどが挙げられる。これらおよびその他の入力装置は、システムバス１２１に連結されたユーザ入力インターフェース１６０を介して、しばしばプロセッシングユニット１２０に接続されるが、パラレルポート、ゲームポート、またはユニバーサルシリアルバス（ＵＳＢ）など、その他のインターフェースおよびバス構造によって接続することもできる。
【００４６】
モニタ１９１またはその他のタイプのディスプレイ装置も、ビデオインターフェース１９０などのインターフェースを介して、システムバス１２１に接続される。モニタ１９１に加えて、コンピュータは、出力周辺インターフェース１９５を介して接続できる、スピーカ１９７やプリンタ１９６などのその他の周辺出力装置も含むことができる。
【００４７】
コンピュータ１１０は、リモートコンピュータ１８０などの１つまたは複数のリモートコンピュータへの論理コネクションを使用して、ネットワーク環境で動作することができる。リモートコンピュータ１８０は、パーソナルコンピュータ、サーバ、ルータ、ネットワークＰＣ、ピア装置、またはその他の共通ネットワークノードとすることができ、コンピュータ１１０に関連して上述した多くの要素またはすべての要素を一般に含むが、図６には、メモリ記憶装置１８１だけが示されている。図６に示す論理コネクションは、ローカルエリアネットワーク（ＬＡＮ）１７１およびワイドエリアネットワーク（ＷＡＮ）１７３を含むが、その他のネットワークも含むことができる。そのようなネットワーク環境は、オフィス、企業規模のコンピュータネットワーク、イントラネット、およびインターネットにおいて一般的である。
【００４８】
ＬＡＮネットワーク環境で使用される場合、コンピュータ１１０は、ネットワークインターフェースまたはアダプタ１７０を介してＬＡＮ１７１に接続される。ＷＡＮネットワーク環境で使用される場合、コンピュータ１１０は一般に、インターネットなどのＷＡＮ１７３を介する通信を確立するためのモデム１７２またはその他の手段を含む。モデム１７２は、内蔵とも外付けともすることができ、ユーザ入力インターフェース１６０またはその他の適切な機構を介して、システムバス１２１に接続することができる。ネットワーク環境では、コンピュータ１１０に関して示されたプログラムモジュールまたはその部分は、リモートメモリ記憶装置に保存することができる。例えば、図６には、メモリ装置１８１に存在するリモートアプリケーションプログラム１８５が示されているが、これに限定されるものではない。図示したネットワーク接続は例示的なものであり、コンピュータ間の通信リンクを確立するその他の手段も使用できることは理解されよう。
【００４９】
コンピュータ１１０またはその他のクライアント装置がコンピュータネットワークの一部として配備され得ることは、当業者であれば理解することができよう。この点で、本発明は、任意の数のメモリまたは記憶ユニットおよび任意の数の記憶ユニットまたはボリュームにわたって存在する任意の数のアプリケーションならびにプロセスを有する任意のコンピュータシステムに関する。本発明の実施形態は、リモートまたはローカル記憶装置を有する、ネットワーク環境に配備されたサーバコンピュータおよびクライアントコンピュータを備える環境に適用することができる。本発明はまた、プログラミング言語機能、解釈および実行能力を有する、スタンドアロンコンピューティング装置にも適用することができる。
【００５０】
本明細書で説明された様々なシステム、方法、および技法は、ハードウェアもしくはソフトウェアで、または必要に応じて両方の組合せで実施することができる。したがって、本発明の方法および装置、またはその一定の態様もしくは部分は、フロッピー（登録商標）ディスケット、ＣＤ−ＲＯＭ、ハードドライブ、またはその他の任意のマシン可読記憶媒体など、有形な媒体に表現されたプログラムコード（すなわち命令）の形態をとることができ、プログラムコードがコンピュータなどのマシンによってロードされ、実行されると、そのマシンは本発明を実行するための装置になる。プログラム可能コンピュータでプログラムコードが実行される場合、コンピュータは一般に、プロセッサと、プロセッサによって可読な（揮発性および不揮発性メモリならびに／または記憶要素を含む）記憶媒体と、少なくとも１つの入力装置と、少なくとも１つの出力装置を含む。コンピュータシステムと通信するために、１つまたは複数のプログラムが好ましくは、高水準手続型またはオブジェクト指向プログラミング言語で実装される。しかし、プログラムは、必要に応じてアセンブリ言語またはマシン語で実装され得る。いずれにせよ、言語はコンパイル言語またはインタープリタ言語とすることができ、ハードウェア実装を組み合わせてもよい。
【００５１】
本発明の方法および装置はまた、電気配線もしくはケーブル、光ファイバ、またはその他の任意の伝送形態など、何らかの伝送媒体を介して送信されるプログラムコードの形態で実施されることもでき、プログラムコードが受信され、ＥＰＲＯＭ、ゲートアレイ、プログラマブル論理回路（ＰＬＤ）、クライアントコンピュータ、またはビデオレコーダなどのマシンにロードされ、マシンによって実行されると、そのマシンは本発明を実行するための装置になる。汎用プロセッサで実施される場合、プログラムコードは、プロセッサと相まって、本発明の機能を実行するように動作する独自の装置を提供する。
【００５２】
本発明が様々な図面の好ましい実施形態に関連して説明されたが、その他の類似した実施形態が使用され得ること、あるいは本発明の同じ機能を実行するために、本発明から逸脱することなく、説明された実施形態に変更および追加を施し得ることを理解されたい。したがって、本発明は、いずれか１つの実施形態に限定されるべきではなく、むしろ添付の特許請求の範囲にしたがってその幅および範囲について解釈されるべきである。
【図面の簡単な説明】
【００５３】
【図１】本発明の態様を説明する際に有用な高水準ブロック図である。
【図２】本発明による例示的なシステムのブロック図である。
【図３】本発明によるＱＢＦを解く例示的な方法の流れ図である。
【図４】ＱＢＦを複数の構成要素部に分解する例示的な方法の流れ図である。
【図５】本発明による構成要素の充足可能性を判定する例示的な方法の流れ図である。
【図６】本発明の態様を実施できるコンピューティング環境例を示すブロック図である。
【図１】
2006202288.tif 000003
【図２】
2006202288.tif 000004
【図３】
2006202288.tif 000005
【図４】
2006202288.tif 000006
【図５】
2006202288.tif 000007
【図６】
2006202288.tif 000008