コンピュータに下記機能を実現させるためのプログラム。式のデータを受け取り、目標式として記録する入力機能。飽和順序に式が含まれないよう初期化する初期化機能。入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか1つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を1つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。飽和順序構成機能の実行後に、飽和順序を出力して機能の実行を終了する出力機能。コンピュータに下記機能を実現させるためのプログラム。順序付けられた式の集合のデータを受け取り、飽和順序として記録する入力機能。影響順序に基礎が含まれないよう初期化する初期化機能。入力機能と初期化機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。他の機能から呼び出されると、もしも影響順序の最も大きな基礎最大基礎と呼ぶに含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。影響順序構成機能の実行後に、影響順序を出力して機能の実行を終了する出力機能。コンピュータに下記機能を実現させるためのプログラム。順序付けられた基礎の集合のデータを受け取り、影響順序として記録する入力機能。評価順序に式が含まれないよう初期化する初期化機能。入力機能と初期化機能の実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。評価順序構成機能の実行後に、評価順序を出力して機能の実行を終了する出力機能。コンピュータに下記機能を実現させるためのプログラム。式のデータを受け取り、目標式として記録する入力機能。飽和順序に式が含まれないようにし、影響順序に基礎が含まれないようにし、評価順序に節が含まれないようにし、割当候補を恒真にする初期化機能。入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか1つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を1つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。飽和順序構成機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。他の機能から呼び出されると、もしも影響順序の最も大きな基礎最大基礎と呼ぶに含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。影響順序構成機能の実行中または実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。評価順序構成機能の実行中または実行後に、評価順序の小さい式から順に、その式を評価式として割当候補計算機能を実行することを、評価順序の式全てについて行う割当候補構成機能。他の機能から呼び出されると、評価式と割当候補の論理積と等価なDNFを計算して割当候補に記録する割当候補計算機能。割当候補構成機能の終了後に、割当候補、または飽和順序と割当候補、または飽和順序と影響順序と割当候補、または飽和順序と影響順序と評価順序と割当候補を出力して機能の実行を終了する出力機能。対象式の全ての節が含まれる相関式の集合が記録されたコンピュータ読取可能な記録媒体。請求項5において、相関式が順序付けられており、かつ相関式の節は、その相関式よりも大きい相関式全てと相関関係にならない相関式の集合が記録されたコンピュータ読取可能な記録媒体。対象式に含まれる変数を元とする基礎について、次の構成AかつBとなる基礎の順序が記録されたコンピュータ読取可能な記録媒体。Aそれぞれの基礎が互いに包含するされるの関係にある。Bある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する。対象式に含まれる節を、その節と相関関係にならない相関式の個数の多い順に並べた順序が記録されたコンピュータ読取可能な記録媒体。本発明の解決しようとする課題は、CNFSATの計算複雑性をCNFの節同士の関係から整理抽出したデータ構造を提供する点にある。またそのデータ構造を効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。また、そのデータ構造を用いてCNFSATを効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。本発明で使用する用語を説明する。本発明では肯定リテラルを肯定変数、否定リテラルを否定変数、リテラルを肯否変数、リテラルを意識しない肯否を無視する場合は単に変数と呼ぶ。CNFを式と呼ぶ。CNFSATの対象となる式を対象式と呼ぶ。対象式の節の部分集合からなる式を部分式と呼ぶ。対象式や部分式を単に式と呼ぶことがある。節の集合と式を等価に扱うことがある。変数を含まない節を空節と呼ぶ。空節は恒偽に対応する。節を含まない式を空式と呼ぶ。空式は恒真に対応する。式や節に含まれる変数の集合を基礎と呼ぶ。基礎では変数の肯否を区別しない。空節の基礎は空集合となり、空式の基礎は任意の変数となる。基礎に含まれる変数の個数を次数と呼ぶ。2つの節について、片方の節にある変数の肯定変数が、もう片方に同じ変数の否定変数が含まれる場合、その2つの節同士の関係を、その変数についての節の直交関係と呼ぶ。例えばX∨Yは、A∨¬Xなどのように¬Xを含む節とXについて直交関係になり、B∨¬YやX∨¬Yなどのように¬Yを含む節とYについて直交関係になり、¬X∨¬Yなどのように¬Xと¬Yを含む節とXとYについて直交関係になる。直交関係にならない節同士の関係を相関関係と呼ぶ。また、ある節Aと式Bにおいて、節Aが式Bの任意の節と相関関係にある時、節Aと式Bの関係も相関関係と呼ぶ。同様に、ある式Cと式Dにおいて、式Cの任意の節が式Dの任意の節と相関関係にある時、式Cと式Dの関係も相関関係と呼ぶ。また、全ての節の関係が相関関係となる式を相関式と呼ぶ。空節は任意の節と相関関係に、空式は任意の節と直交関係にあるものとする。なお本発明では、式や節、変数、集合、元などの計算対象を表すデータは従来のコンピュータで用いられるデータとする。バイナリ列や配列、テーブル、レコード、構造体などのデータや、変数の区切りを空白とし節の区切りを改行としたテキストデータを用いる場合もある。また変数番号の偶数奇数で変数の肯定否定を定める場合や計算対象の省略形を表すデータ構造などの場合もある。あるいは集合を表すデータで式や節を表すことがある。また計算対象を表すデータ構造が他に存在し、そのデータへの参照によって計算対象を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。このように計算対象のデータ構造は様々だが、計算対象を特定し他と区別できるデータであれば良く、これらに限定されない。また、順序をグラフやリンクや配列で表す場合、この順序を表すグラフやリンクや配列は従来のコンピュータで用いられるデータであるとする。このデータには有向非循環グラフが使用されることがある。グラフやリンクや配列を表すデータは様々なものが存在するが、計算対象の順序が判れば良く、特定のものに限定されない。また、本発明で用いる構成要素は、メモリ等の記憶手段やコンピュータ読取可能な記録媒体に記録記憶され、コンピュータのデータとして活用される。なお、表記の簡単化のため、メモリ等の記憶手段に記録されたデータを、式や節、変数、集合、元、順序、グラフ、参照、などのようにそのまま表記することがある。なお本発明では、論理式と等価なDNFを計算する機能を実現するためのプログラムは、従来のコンピュータで用いられるプログラムを使用するものとする。課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。式のデータを受け取り、目標式として記録する入力機能。飽和順序に式が含まれないよう初期化する初期化機能。入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか1つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を1つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。飽和順序構成機能の実行後に、飽和順序を出力して機能の実行を終了する出力機能。また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。順序付けられた式の集合のデータを受け取り、飽和順序として記録する入力機能。影響順序に基礎が含まれないよう初期化する初期化機能。入力機能と初期化機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。他の機能から呼び出されると、もしも影響順序の最も大きな基礎最大基礎と呼ぶに含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。影響順序構成機能の実行後に、影響順序を出力して機能の実行を終了する出力機能。また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。順序付けられた基礎の集合のデータを受け取り、影響順序として記録する入力機能。評価順序に式が含まれないよう初期化する初期化機能。入力機能と初期化機能の実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。評価順序構成機能の実行後に、評価順序を出力して機能の実行を終了する出力機能。また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。式のデータを受け取り、目標式として記録する入力機能。飽和順序に式が含まれないようにし、影響順序に基礎が含まれないようにし、評価順序に節が含まれないようにし、割当候補を恒真にする初期化機能。入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか1つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を1つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。飽和順序構成機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。他の機能から呼び出されると、もしも影響順序の最も大きな基礎最大基礎と呼ぶに含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。影響順序構成機能の実行中または実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。評価順序構成機能の実行中または実行後に、評価順序の小さい式から順に、その式を評価式として割当候補計算機能を実行することを、評価順序の式全てについて行う割当候補構成機能。他の機能から呼び出されると、評価式と割当候補の論理積と等価なDNFを計算して割当候補に記録する割当候補計算機能。割当候補構成機能の終了後に、割当候補、または飽和順序と割当候補、または飽和順序と影響順序と割当候補、または飽和順序と影響順序と評価順序と割当候補を出力して機能の実行を終了する出力機能。また課題を解決するため、本発明では、対象式の全ての節が含まれる相関式の集合が記録されたコンピュータ読取可能な記録媒体とした。また、上記の相関式が順序付けられており、かつ相関式に属する節は、節の属する相関式よりも大きい相関式全てと相関関係にならないものとする場合がある。また課題を解決するため、本発明では、対象式に含まれる変数を元とする基礎について、次の構成AかつBとなる基礎の順序が記録されたコンピュータ読取可能な記録媒体とした。Aそれぞれの基礎が互いに包含するされるの関係にある。Bある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する。また課題を解決するため、本発明では、対象式に含まれる節を、その節と相関関係にならない相関式の個数の多い順に並べた順序が記録されたコンピュータ読取可能な記録媒体とした。本発明により、対象式の節を相関関係によって分類することができるようになった。この分類を活用することで、どの節がどの節と相関関係にあるのか、及び相関関係にならない相関式はどれなのかということを把握することができるようになった。相関関係はCNFSATの計算複雑性の指標となり、この結果として対象式のCNFSATの計算複雑性を把握することができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。また本発明により、対象式の変数を、相関式の多い順に順序付けることができるようになった。相関式の数は直交関係の規模であり、計算複雑性の指針となる。また、相関式の多い変数は、CNFSATの構造が複雑な部分でもあるため、この結果としてCNFSATを計算するときに重要となる変数を順番に並べることができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。また本発明により、対象式の節を、直交関係となる相関式の多い順に順序付けることができるようになった。直交相関関係はCNFSATの計算複雑性の指標となる。また、直交関係となる相関式の多い節は、CNFSATの構造が複雑な部分でもあるため、CNFSATを計算するときに重要となる節を順番に並べることができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。また本発明により、対象式の節の直交相関関係を用いてCNFSATを計算することができるようになった。節の直交相関関係はCNFSATの構造の大きな部分を占めるため、その構造の詰まった節から順番にCNFSATを計算することにより、効率良く判定を行うことができる。つまり、本発明のプログラム及びコンピュータ読取可能な記録媒体により、CNFSATの計算複雑性をCNFの節の相関直交関係から整理抽出したデータ構造を記録することができるようになった。またそのような相関直交関係を表すデータ構造を効率良く計算する機能をコンピュータで実現することが可能となった。またそのような相関直交関係を表すデータ構造を使用してCNFが真となる真理値割当を効率良く計算する機能をコンピュータで実現することが可能となった。以下に本発明の実施形態の一つについて説明する。図1は本実施形態によるプログラムのブロック図である。本実施形態では、コンピュータで判定機能100を実現させるためのプログラムとした。判定機能100は下記機能から構成されている。入力として受け取ったCNFを目標式180に記録する入力機能110。飽和順序181に式が含まれないようにし、影響順序182に基礎が含まれないようにし、評価順序183に節が含まれないようにし、割当候補184を恒真にする初期化機能120。入力機能110と初期化機能120の実行後に、飽和順序追加機能131を繰り返し実行し、目標式180全ての節を飽和順序181の式に記録した後に終了する飽和順序構成機能130。他の機能から呼び出されると、目標式180の節のうち飽和順序181の式に記録されていない節のいずれか1つからなる新たな飽和式133を記録し、飽和式構成機能132を実行し、飽和式133を飽和順序181に既に記録されている式よりも小さい式として飽和順序181に記録する飽和順序追加機能131。他の機能から呼び出されると、飽和式133と相関関係にあると同時に飽和順序181の式や飽和式133に記録されていない目標式180のいずれかの節を1つ飽和式133に記録することを繰り返し実行し、飽和式133に記録できる節が無くなった時に終了する飽和式構成機能132。飽和順序構成機能130の実行後に、飽和順序181の小さい式から順に、その式を対象式として影響順序追加機能141を繰り返し実行することを、飽和順序181の式全てについて行う影響順序構成機能140。他の機能から呼び出されると、もしも影響順序182の最も大きな基礎最大基礎と呼ぶに含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序182に記録する影響順序追加機能141。影響順序構成機能140の実行中または実行後に、影響順序182の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能151を繰り返し実行することを、影響順序182の基礎全てについて行う評価順序構成機能150。他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序183の式に記録されていない目標式180の節からなる式を、評価順序183に記録されている節よりも大きい節として評価順序183に記録する評価順序追加機能151。評価順序構成機能150の実行中または実行後に、評価順序183の小さい式から順に、その式を評価式として割当候補計算機能161を実行することを、評価順序183の式全てについて行う割当候補構成機能160。他の機能から呼び出されると、評価式と割当候補184の論理積と等価なDNFを計算して割当候補184に記録する割当候補計算機能161。割当候補構成機能160の終了後に、飽和順序181、影響順序182、評価順序183、割当候補184を出力して機能の実行を終了する出力機能170。入力機能110の受け取るCNFのデータは、従来コンピュータでCNFとして使用されるデータ構造とする。なお、空式は節を含まないCNFのデータで表す。また空節は変数を含まない節からなるCNFのデータで表す。飽和順序追加機能131や飽和式構成機能132で節を選択するときは、ランダムに節を選択するものとする。なお、この選択がランダムではなく、入力のCNFの順序やCNFの節に含まれる変数の辞書順など、従来からコンピュータで使用されている順序付けにおいて小さい/大きい順で選択する場合がある。また、この他に従来のコンピュータで用いられる選択方法を用いて節を選択する場合がある。割当候補計算機能161により論理式と等価なDNFを計算する機能は、従来のコンピュータでDNFを計算する時に使用されている機能とする。目標式180のデータ構造は、従来コンピュータでCNFとして使用されるデータ構造とする。なお、目標式180の節は順序付けられて記録されていることがある。例えば変数を索引とする辞書順に並べられていることがある。また目標式180には、CNFの他に、計算を容易にするためのデータが記録されることがある。例えば肯否変数についての検索や、それぞれの機能によって処理されたかどうかを判定するためのフラグなどである。また目標式180には、CNFについての複数のデータが記録されることがある。例えば飽和順序追加機能131や飽和式構成機能132用として、あるいは評価順序追加機能151用として別のデータを用意することがある。飽和順序追加機能131や飽和式構成機能132は、節を処理するごとにこのデータから節を削除し、飽和順序181に記録されていない目標式180の節を構成する代用とする。また評価順序追加機能151も同様に、節を処理するごとにこのデータから節を削除し、評価順序183に記録されていない目標式180の節を構成する代用とする。飽和順序181のデータ構造は、節を表す肯否変数のレコードについて、そのレコードを集めた式となるレコードを、順序の大きい式から順番に並べた配列となる。飽和順序追加機能131が相関関係となる節を全て取り込むため、飽和順序181の全ての節は、その節の含まれる式よりも大きい式とは相関関係にならない。影響順序182のデータ構造は、基礎を表す変数のレコードを、順序の小さい基礎から順番に並べた配列となる。影響順序追加機能141は、最大基礎にそれまでの影響順序182に記録された基礎の変数を全て含むようにするため、影響順序182に記録された基礎は互いに包含するされるの関係となる。また、影響順序182は、より大きい式の方が含まれる変数の多くなる傾向のある飽和順序181から構成される。よって、影響順序182に記録された基礎は、ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する傾向となる。なお影響順序182に記録されるデータは、それぞれの基礎の差分となる変数の集合にすることがある。この結果、影響順序182のデータの重複部分を省略することが出来、データを圧縮することができる。評価順序183のデータ構造は、節を表す肯否変数のレコードについて、そのレコードを集めた式となるレコードを、順序の小さい式から順番に並べた配列となる。評価順序183は、評価順序追加機能151によって、影響順序182の基礎の順序に従って順序付けられる。影響順序182ではより小さいの基礎の方が相関式の個数が多くなるため、評価順序183も相関関係にならない相関式の個数の多い節から、相関関係にならない相関式の個数の同じ節が一つの式としてまとめられるようにして順番に並べられる。割当候補184のデータ構造はDNFのレコードとなる。DNFのレコードは、従来コンピュータでDNFとして使用されるデータ構造とする。なお、DNFとCNFは双対の関係となるため、CNFのレコードをDNFのレコードの代用とすることがある。恒真は何も式を含まないDNFのデータで表す。