【手続補正書】
【提出日】平成27年12月8日(2015.12.8)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】全文
【補正方法】変更
【補正の内容】
【特許請求の範囲】
【請求項１】
複雑な完全論理式、ＷＦＦ、を単純化するコンピュータ実行方法であって、
式プロセッサ（１８）内で入力ＷＦＦ（１００）を受け取るステップであって、前記入力ＷＦＦ（１００）は、
i）真の原子、
ii）偽の原子、
iii）ブール述語、および／または
iv）等価述語
のうちの１つ以上、および
i）否定演算子、
ii）連言演算子、および／または
iii）選言演算子
のうちの０個以上により成っている、ステップと、
次のこと：
式コンバータ（２０）を用いて、前記入力ＷＦＦ（１００）を初期ビット配列（２００）に変換すること；
ビット配列シンプリファイヤ（２２）を用いて、前記初期ビット配列（２００）の冗長な次元をセマンティックス的に除去することによって、前記初期ビット配列（２００）を単純化されたビット配列（２１２）に単純化すること；および
ビット配列コンバータ（２４）を用いて、前記単純化されたビット配列（２１２）を連言標準形（１４２）または選言標準形（１４０）の戻りＷＦＦ（１３８）に変換することを実行するステップと、
前記式プロセッサ（１８）を用いて、前記戻りＷＦＦ（１３８）を返すステップと、を含み、
前記方法は、トレード研究において、データ依存制約ネットワークの一部である入力変数のユーザ指定の集合から出力変数のユーザ指定の集合の値を計算するための条件計算プランにおいて実行される、方法。
【請求項２】
前記入力ＷＦＦ（１００）を前記初期ビット配列（２００）に変換する前記ステップは、
前記入力ＷＦＦ（１００）内の述語（１１４）を判定すること、
前記述語（１１４）の各１つに関連する領域要素（１２０）を判定すること、
前記述語（１１４）および前記領域要素（１２０）に対応する前記初期ビット配列（２００）のビット配列次元（２１８）を判定すること、および
前記ビット配列次元（２１８）ならびにそれに関連する前記述語（１１４）および前記領域要素（１２０）を有する前記初期ビット配列（２００）を返すために前記入力ＷＦＦ（１００）を処理することを含み、
前記入力ＷＦＦ（１００）は、好ましくは、真の原子ＷＦＦ（１４８）および偽の原子ＷＦＦ（１５０）のうちの１つであり、
前記初期ビット配列（２００）を返すために前記入力ＷＦＦ（１００）を処理する前記ステップは、好ましくは、
前記真の原子ＷＦＦ（１４８）または偽の原子ＷＦＦ（１５０）に対して、世界の真の配列（２１４）または世界の偽の配列（２１６）をそれぞれ返す、請求項１に記載の方法。
【請求項３】
前記入力ＷＦＦ（１００）は、ブール述語（１２４）または等価述語（１２６）を含む原子ＷＦＦ（１０６）であり、
前記初期ビット配列（２００）を返すために前記入力ＷＦＦ（１００）を処理する前記ステップは、
前記原子ＷＦＦがブール述語（１２４）である場合に、前記ブール述語（１２４）を等価述語（１２６）に変換すること、
前記等価述語（１２６）について、前記ビット配列次元（２１８）ならびにそれに関連する前記述語（１１４）および前記領域要素（１２０）を判定すること、
配列キャッシュ（３０）から、前記等価述語（１２６）に関連する前記ビット配列次元（２１８）、前記述語（１１４）、および前記領域要素（１２０）を有する初期ビット配列（２００）を取り出すこと、および
前記配列キャッシュ（３０）からの前記初期ビット配列（２００）の取出がない場合に前記初期ビット配列（２００）を構成することを含む、請求項２に記載の方法。
【請求項４】
前記入力ＷＦＦ（１００）は、複合ＷＦＦ（１３６）であり、
前記初期ビット配列（２００）を生成するために前記入力ＷＦＦ（１００）を処理する前記ステップは、
原子ＷＦＦ（１０６）に出会うまで、前記複合ＷＦＦ（１３６）を再帰的に処理すること、
再帰的に処理された前記原子ＷＦＦ（１４８、１５０）の各１つについて初期ビット配列（２００）を返すこと、および
否定演算子（１３０）、連言演算子（１３２）、および選言演算子（１３４）のうちの少なくとも１つに基づいて前記初期ビット配列（２００）を組み合わせることを含む、請求項３に記載の方法。
【請求項５】
前記ビット配列次元（２１８）は、ビット要素を有する部分配列（２２０）を含み、
前記初期ビット配列（２００）を縮小させる前記ステップは、
前記ビット配列次元（２１８）の各１つについて前記部分配列（２２０）の前記ビット要素（２２２）を比較すること、
等しいビット要素（２２２）を有する部分配列（２２０）を有する各ビット配列次元（２１８）を前記初期ビット配列（２００）から除去すること、
前記初期ビット配列（２００）から除去されないビット配列次元（２１８）を含む保存された次元インデックス（２８）を生成すること、および
単純化されたビット配列（２１２）および前記保存された次元インデックス（２８）を返すことを含む、請求項１に記載の方法。
【請求項６】
前記単純化されたビット配列（２１２）は、ビット要素からなり、
前記単純化されたビット配列（２１２）を前記戻りＷＦＦ（１３８）に変換する前記ステップは、
前記単純化されたビット配列（２１２）内の前記ビット要素（２２２）の総量を判定すること、
１の値を有する前記単純化されたビット配列（２１２）内の前記ビット要素（２２２）の量を判定すること、
前記ビット要素（２２２）の前記総量の半分未満が１の値を有する場合に、前記単純化されたビット配列（２１２）を前記選言標準形（１４０）の前記ＷＦＦに変換すること、および
前記ビット要素（２２２）の前記総量の少なくとも半分が１の値を有する場合に、前記単純化されたビット配列（２１２）を前記連言標準形（１４２）の前記戻りＷＦＦ（１３８）に変換することを含む、請求項１ないし５のいずれか一項に記載の方法。
【請求項７】
前記式プロセッサ（１８）内で前記入力ＷＦＦ（１００）を受け取る前に、古典的プロセッサ（１４）内で、１つまたは複数の古典的アルゴリズムを使用して前記入力ＷＦＦ（１００）を処理することによって所定のタイムアウト期間内に結果のＷＦＦ（１０４）を処理するステップと、
前記結果のＷＦＦ（１０４）またはそれがないことを前記式プロセッサ（１８）に通信するステップと、
前記結果のＷＦＦ（１０４）がない場合に前記式プロセッサ（１８）内で前記入力ＷＦＦ（１００）を受け取るステップと、をさらに含む、請求項１ないし６のいずれか一項に記載の方法。
【請求項８】
設計制約式計算をサポートするプロセッサベースのシステムであって、
入力完全論理式（ＷＦＦ）を初期ビット配列（２００）に変換するように構成された式コンバータ（２０）と、
前記初期ビット配列（２００）の冗長な次元をセマンティックス的に除去することによって、前記初期ビット配列（２００）を単純化されたビット配列（２１２）に単純化するように構成されたビット配列シンプリファイヤ（２２）と、
前記単純化されたビット配列（２１２）を連言標準形（１４２）または選言標準形（１４０）の戻りＷＦＦ（１３８）に変換するように構成されたビット配列コンバータ（２４）と、を含み、
前記入力ＷＦＦ（１００）は、
i）真の原子、
ii）偽の原子、
iii）ブール述語、および／または
iv）等価述語
のうちの１つ以上、および
i）否定演算子、
ii）連言演算子、および／または
iii）選言演算子
のうちの０個以上により成っており、
前記プロセッサベースのシステムは、トレード研究において、データ依存制約ネットワークの一部である入力変数のユーザ指定の集合から出力変数のユーザ指定の集合の値を計算するための条件計算プランの入力ＷＦＦを単純化するように構成されている、システム。
【請求項９】
前記式コンバータ（２０）は、前記入力ＷＦＦ（１００）内の前記述語（１１４）を判定し、前記述語（１１４）の各１つに関連する領域要素（１２０）を判定し、前記述語（１１４）および前記領域要素（１２０）に対応する前記初期ビット配列（２００）のビット配列次元（２１８）を判定するように構成され、
前記入力ＷＦＦ（１００）は、好ましくは、真の原子ＷＦＦ（１４８）および偽の原子ＷＦＦ（１５０）のうちの１つであり、
前記式コンバータ（２０）は、好ましくは、前記真の原子ＷＦＦ（１４８）または前記偽の原子ＷＦＦ（１５０）を、０次元で世界の真の配列（２１４）および世界の偽の配列（２１６）のそれぞれの１つを含む初期ビット配列（２００）に変換するように構成される、請求項８に記載のシステム。
【請求項１０】
１つまたは複数の初期ビット配列（２００）を含む配列キャッシュ（３０）と、
ブール述語（１２４）または等価述語（１２６）を含む前記入力ＷＦＦ（１００）と、
前記ブール述語（１２４）を等価述語（１２６）に変換し、ビット配列次元（２１８）ならびに前記等価述語（１２６）に関連する前記述語（１１４）および前記領域要素（１２０）を判定し、前記配列キャッシュ（３０）から、前記等価述語（１２６）を表す初期ビット配列（２００）を取り出すように構成された前記式コンバータ（２０）と、をさらに含み、任意に、
前記配列キャッシュ（３０）内に前記初期ビット配列（２００）がない場合に前記初期ビット配列（２００）を構成するように構成されたビット配列コンストラクタ（２６）と、をさらに含む、請求項８または９に記載のシステム。
【請求項１１】
前記入力ＷＦＦは、少なくとも１つの演算子に関連する２つ以上の原子ＷＦＦを含む複合ＷＦＦであり、
前記式コンバータは、前記原子ＷＦＦのうちの各１つに対して初期ビット配列を返すように構成され、否定演算子、連言演算子、および選言演算子のうちの少なくとも１つに基づいて前記初期ビット配列を組み合わせるように構成される、請求項１０に記載のシステム。
【請求項１２】
前記初期ビット配列（２００）は、前記述語（１１４）に関連する複数のビット配列次元（２１８）を有し、
前記ビット配列シンプリファイヤ（２２）は、前記ビット配列次元（２１８）のうちの少なくとも１つを除去することによって前記初期ビット配列（２００）を縮小させるように構成され、
前記ビット配列次元は、ビット要素を有する部分配列（２２０）を含み、
前記ビット配列シンプリファイヤ（２２）は、前記ビット配列次元（２１８）の各１つについて前記部分配列（２２０）の前記ビット要素（２２２）を比較し、等しいビット要素（２２２）を有する部分配列を有する各ビット配列次元を前記初期ビット配列（２００）から除去するように構成される、請求項８ないし１１のいずれか一項に記載のシステム。
【請求項１３】
ビット配列コンバータ（２４）であって、
前記単純化されたビット配列内のビット要素（２２２）の総量に対する１の値を有する前記単純化されたビット配列（２１２）内の前記ビット要素（２２２）の量を判定し、
前記ビット要素（２２２）の前記総量の半分未満が１の値を有する場合に、前記単純化されたビット配列（２１２）を前記選言標準形（１４０）の前記ＷＦＦに変換し、
前記ビット要素（２２２）の前記総量の少なくとも半分が１の値を有する場合に、前記単純化されたビット配列（２１２）を前記連言標準形（１４２）の前記戻りＷＦＦ（１３８）に変換するように構成された、ビット配列コンバータ（２４）をさらに含む、請求項８ないし１２のいずれか一項に記載のシステム。
【請求項１４】
前記入力ＷＦＦ（１００）を受け取るように構成され、１つ以上の古典的アルゴリズムを用いて所定のタイムアウト期間内に結果のＷＦＦ（１０４）を判定するように構成された古典的プロセッサ（１４）をさらに含み、
前記古典的プロセッサ（１４）は、前記結果のＷＦＦおよびその欠如を式プロセッサ（１８）に伝えるように構成され、
前記式プロセッサ（１８）は、前記古典的プロセッサから結果のＷＦＦ（１０４）を受け取らなかったときに、前記入力ＷＦＦ（１００）を受け取るように構成されている、請求項８ないし１３に記載のシステム。