ＣＮＦ関係データ構造、及びＣＮＦ関係データ構成プログラム、及びＣＮＦＳＡＴ計算プログラム
【課題】ＳＡＴ（充足可能性問題）及びＣＮＦＳＡＴの構造を計算複雑性に関連する形で整理・抽出したデータ構造は存在しなかった。また上記データ構造をＣＮＦＳＡＴから構成する計算手法が存在しなかった。また、上記データ構造を用いてＣＮＦＳＡＴを計算する手法も存在しなかった。
【解決手段】ＣＮＦＳＡＴの節同士の相関・直交関係に従って節を分類・整理することにより計算複雑性を明らかにする。また、コンピュータにこの相関・直交関係の計算を効率的に行わせる機能を実現させるためのプログラムを用意することで、コンピュータにＣＮＦの計算複雑性の明確化やＣＮＦＳＡＴの計算を効率良く行わせることができるようになった。
【解決手段】ＣＮＦＳＡＴの節同士の相関・直交関係に従って節を分類・整理することにより計算複雑性を明らかにする。また、コンピュータにこの相関・直交関係の計算を効率的に行わせる機能を実現させるためのプログラムを用意することで、コンピュータにＣＮＦの計算複雑性の明確化やＣＮＦＳＡＴの計算を効率良く行わせることができるようになった。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ＣＮＦの節同士の関係を表すデータ構造、及びコンピュータにてＣＮＦの節同士の関係を表すデータを構成するプログラム、及びＣＮＦＳＡＴを計算するプログラムに関する
【背景技術】
【０００２】
従来、コンピュータでは様々な問題が扱われており、また論理式や充足可能性問題、恒真式問題など論理に関する問題も様々なものが扱われている。
【０００３】
例えばＳＡＴ（充足可能性問題）は、ＮＰ完全問題に属し、その応用範囲も広い。特にＣＮＦ（乗法標準形）で構成されたＳＡＴであるＣＮＦＳＡＴは、ＳＡＴから多項式時間で変換可能（例えば非特許文献１参照）でありながら変換後の取り扱いが容易となるため、様々な問題で活用されている。例えば構造物などにおいて各種の拘束条件を満たす解が存在するかどうかを判定する問題や、あるいは各種パズルなどの作成や計算など様々な場面で活用されている。
【０００４】
ＣＮＦＳＡＴは本質的にコンピュータで計算するのが困難な問題であり、判定するのに実質不可能な指数規模の時間が必要になることがある。ＣＮＦＳＡＴの計算複雑性はＣＮＦの構造の複雑さにより決まる。よってＣＮＦＳＡＴをＣＮＦの構造の観点から整理することは、ＣＮＦＳＡＴを効率的に計算するために重要となる。また、ＣＮＦＳＡＴの節同士の関係はＣＮＦＳＡＴの構造を明らかにするにあたり重要となる。
【０００５】
しかし、今まではＣＮＦＳＡＴの構造を、ＣＮＦの節の関係で表現するデータ構造は存在しなかった。
【０００６】
また、複数の論理式から新たな論理式を構成する導出という演繹方法が存在する。導出とは２つの節から制約条件を変えずに追加可能な１つの節を導き出す操作である。片方の節にＡ∨Ｐという命題があり、もう片方に¬Ａ∨Ｑという命題がある時、両方の命題が同時に成立するときはＰ∨Ｑという命題も存在することを導き出す操作である。導出を用いることによって、ＣＮＦに含まれる命題を導き出して充足可否を求めることも可能である。また、この導出やその他の論理式を削除する手法をまとめたＤＬＰＰというアルゴリズムも存在する。
【０００７】
しかし、導出やＤＰＬＬアルゴリズムはある２つの命題の肯定と否定を組合せて別の命題を顕在化する操作であり、ＣＮＦのような様々なリテラルの肯定・否定が入れ混じる論理式で導出を行うのは計算の効率が悪かった。
【０００８】
また、ＣＮＦをＤＮＦ（加法標準形）にすることができれば、ＤＮＦから容易に充足可否を判定することができるが、ＣＮＦからＤＮＦへの変換は多くの計算量が必要であり、単にＤＮＦに変換して充足可否を求めるのは計算の効率が悪かった。
【先行技術文献】
【非特許文献】
【０００９】
【非特許文献１】「オートマトン 言語理論 計算論 ２」Ｊ．ホップクロフト，Ｊ．ウルマン，Ｒ．モトワニ サイエンス社 ２００８年 Ｐ１４７−１５５
【発明の概要】
【発明が解決しようとする課題】
【００１０】
本発明の解決しようとする課題は、ＣＮＦＳＡＴの計算複雑性をＣＮＦの節同士の関係から整理・抽出したデータ構造を提供する点にある。またそのデータ構造を効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。また、そのデータ構造を用いてＣＮＦＳＡＴを効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。
【課題を解決するための手段】
【００１１】
本発明で使用する用語を説明する。本発明では肯定リテラルを肯定変数、否定リテラルを否定変数、リテラルを肯否変数、リテラルを意識しない（肯否を無視する）場合は単に変数と呼ぶ。ＣＮＦを式と呼ぶ。ＣＮＦＳＡＴの対象となる式を対象式と呼ぶ。対象式の節の部分集合からなる式を部分式と呼ぶ。対象式や部分式を単に式と呼ぶことがある。節の集合と式を等価に扱うことがある。変数を含まない節を空節と呼ぶ。空節は恒偽に対応する。節を含まない式を空式と呼ぶ。空式は恒真に対応する。式や節に含まれる変数の集合を基礎と呼ぶ。基礎では変数の肯否を区別しない。空節の基礎は空集合となり、空式の基礎は任意の変数となる。基礎に含まれる変数の個数を次数と呼ぶ。
【００１２】
２つの節について、片方の節にある変数の肯定変数が、もう片方に同じ変数の否定変数が含まれる場合、その２つの節同士の関係を、その変数についての節の直交関係と呼ぶ。例えば（Ｘ∨Ｙ）は、（Ａ∨¬Ｘ）などのように¬Ｘを含む節とＸについて直交関係になり、（Ｂ∨¬Ｙ）や（Ｘ∨¬Ｙ）などのように¬Ｙを含む節とＹについて直交関係になり、（¬Ｘ∨¬Ｙ）などのように¬Ｘと¬Ｙを含む節とＸとＹについて直交関係になる。直交関係にならない節同士の関係を相関関係と呼ぶ。また、ある節Ａと式Ｂにおいて、節Ａが式Ｂの任意の節と相関関係にある時、節Ａと式Ｂの関係も相関関係と呼ぶ。同様に、ある式Ｃと式Ｄにおいて、式Ｃの任意の節が式Ｄの任意の節と相関関係にある時、式Ｃと式Ｄの関係も相関関係と呼ぶ。また、全ての節の関係が相関関係となる式を相関式と呼ぶ。空節は任意の節と相関関係に、空式は任意の節と直交関係にあるものとする。
【００１３】
なお本発明では、式や節、変数、集合、元などの計算対象を表すデータは従来のコンピュータで用いられるデータとする。バイナリ列や配列、テーブル、レコード、構造体などのデータや、変数の区切りを空白とし節の区切りを改行としたテキストデータを用いる場合もある。また変数番号の偶数奇数で変数の肯定否定を定める場合や計算対象の省略形を表すデータ構造などの場合もある。あるいは集合を表すデータで式や節を表すことがある。また計算対象を表すデータ構造が他に存在し、そのデータへの参照によって計算対象を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。このように計算対象のデータ構造は様々だが、計算対象を特定し他と区別できるデータであれば良く、これらに限定されない。
【００１４】
また、順序をグラフやリンクや配列で表す場合、この順序を表すグラフやリンクや配列は従来のコンピュータで用いられるデータであるとする。このデータには有向非循環グラフが使用されることがある。グラフやリンクや配列を表すデータは様々なものが存在するが、計算対象の順序が判れば良く、特定のものに限定されない。
【００１５】
また、本発明で用いる構成要素は、メモリ等の記憶手段やコンピュータ読取可能な記録媒体に記録・記憶され、コンピュータのデータとして活用される。なお、表記の簡単化のため、メモリ等の記憶手段に記録されたデータを、式や節、変数、集合、元、順序、グラフ、参照、などのようにそのまま表記することがある。
【００１６】
なお本発明では、論理式と等価なＤＮＦを計算する機能を実現するためのプログラムは、従来のコンピュータで用いられるプログラムを使用するものとする。
【００１７】
課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序を出力して機能の実行を終了する出力機能。
【００１８】
また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
順序付けられた式の集合のデータを受け取り、飽和順序として記録する入力機能。
影響順序に基礎が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行後に、影響順序を出力して機能の実行を終了する出力機能。
【００１９】
また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
順序付けられた基礎の集合のデータを受け取り、影響順序として記録する入力機能。
評価順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行後に、評価順序を出力して機能の実行を終了する出力機能。
【００２０】
また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないようにし、影響順序に基礎が含まれないようにし、評価順序に節が含まれないようにし、割当候補を恒真にする初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行中または実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行中または実行後に、評価順序の小さい式から順に、その式を評価式として割当候補計算機能を実行することを、評価順序の式全てについて行う割当候補構成機能。
他の機能から呼び出されると、評価式と割当候補の論理積と等価なＤＮＦを計算して割当候補に記録する割当候補計算機能。
割当候補構成機能の終了後に、割当候補、または飽和順序と割当候補、または飽和順序と影響順序と割当候補、または飽和順序と影響順序と評価順序と割当候補を出力して機能の実行を終了する出力機能。
【００２１】
また課題を解決するため、本発明では、対象式の全ての節が含まれる相関式の集合が記録されたコンピュータ読取可能な記録媒体とした。
【００２２】
また、上記の相関式が順序付けられており、かつ相関式に属する節は、節の属する相関式よりも大きい相関式全てと相関関係にならないものとする場合がある。
【００２３】
また課題を解決するため、本発明では、対象式に含まれる変数を元とする基礎について、次の構成（Ａ）かつ（Ｂ）となる基礎の順序が記録されたコンピュータ読取可能な記録媒体とした。
（Ａ）それぞれの基礎が互いに包含する・されるの関係にある。
（Ｂ）ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する。
【００２４】
また課題を解決するため、本発明では、対象式に含まれる節を、その節と相関関係にならない相関式の個数の多い順に並べた順序が記録されたコンピュータ読取可能な記録媒体とした。
【発明の効果】
【００２５】
本発明により、対象式の節を相関関係によって分類することができるようになった。この分類を活用することで、どの節がどの節と相関関係にあるのか、及び相関関係にならない相関式はどれなのかということを把握することができるようになった。相関関係はＣＮＦＳＡＴの計算複雑性の指標となり、この結果として対象式のＣＮＦＳＡＴの計算複雑性を把握することができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。
【００２６】
また本発明により、対象式の変数を、相関式の多い順に順序付けることができるようになった。相関式の数は直交関係の規模であり、計算複雑性の指針となる。また、相関式の多い変数は、ＣＮＦＳＡＴの構造が複雑な部分でもあるため、この結果としてＣＮＦＳＡＴを計算するときに重要となる変数を順番に並べることができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。
【００２７】
また本発明により、対象式の節を、直交関係となる相関式の多い順に順序付けることができるようになった。直交・相関関係はＣＮＦＳＡＴの計算複雑性の指標となる。また、直交関係となる相関式の多い節は、ＣＮＦＳＡＴの構造が複雑な部分でもあるため、ＣＮＦＳＡＴを計算するときに重要となる節を順番に並べることができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。
【００２８】
また本発明により、対象式の節の直交・相関関係を用いてＣＮＦＳＡＴを計算することができるようになった。節の直交・相関関係はＣＮＦＳＡＴの構造の大きな部分を占めるため、その構造の詰まった節から順番にＣＮＦＳＡＴを計算することにより、効率良く判定を行うことができる。
【００２９】
つまり、本発明のプログラム及びコンピュータ読取可能な記録媒体により、ＣＮＦＳＡＴの計算複雑性をＣＮＦの節の相関・直交関係から整理・抽出したデータ構造を記録することができるようになった。またそのような相関・直交関係を表すデータ構造を効率良く計算する機能をコンピュータで実現することが可能となった。またそのような相関・直交関係を表すデータ構造を使用してＣＮＦが真となる真理値割当を効率良く計算する機能をコンピュータで実現することが可能となった。
【図面の簡単な説明】
【００３０】
【図１】図１は本実施形態によるプログラムのブロック図である。
【発明を実施するための形態】
【００３１】
以下に本発明の実施形態の一つについて説明する。図１は本実施形態によるプログラムのブロック図である。本実施形態では、コンピュータで判定機能１００を実現させるためのプログラムとした。判定機能１００は下記機能から構成されている。
入力として受け取ったＣＮＦを目標式１８０に記録する入力機能１１０。
飽和順序１８１に式が含まれないようにし、影響順序１８２に基礎が含まれないようにし、評価順序１８３に節が含まれないようにし、割当候補１８４を恒真にする初期化機能１２０。
入力機能１１０と初期化機能１２０の実行後に、飽和順序追加機能１３１を繰り返し実行し、目標式１８０全ての節を飽和順序１８１の式に記録した後に終了する飽和順序構成機能１３０。
他の機能から呼び出されると、目標式１８０の節のうち飽和順序１８１の式に記録されていない節のいずれか１つからなる新たな飽和式１３３を記録し、飽和式構成機能１３２を実行し、飽和式１３３を飽和順序１８１に既に記録されている式よりも小さい式として飽和順序１８１に記録する飽和順序追加機能１３１。
他の機能から呼び出されると、飽和式１３３と相関関係にあると同時に飽和順序１８１の式や飽和式１３３に記録されていない目標式１８０のいずれかの節を１つ飽和式１３３に記録することを繰り返し実行し、飽和式１３３に記録できる節が無くなった時に終了する飽和式構成機能１３２。
飽和順序構成機能１３０の実行後に、飽和順序１８１の小さい式から順に、その式を対象式として影響順序追加機能１４１を繰り返し実行することを、飽和順序１８１の式全てについて行う影響順序構成機能１４０。
他の機能から呼び出されると、もしも影響順序１８２の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序１８２に記録する影響順序追加機能１４１。
影響順序構成機能１４０の実行中または実行後に、影響順序１８２の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能１５１を繰り返し実行することを、影響順序１８２の基礎全てについて行う評価順序構成機能１５０。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序１８３の式に記録されていない目標式１８０の節からなる式を、評価順序１８３に記録されている節よりも大きい節として評価順序１８３に記録する評価順序追加機能１５１。
評価順序構成機能１５０の実行中または実行後に、評価順序１８３の小さい式から順に、その式を評価式として割当候補計算機能１６１を実行することを、評価順序１８３の式全てについて行う割当候補構成機能１６０。
他の機能から呼び出されると、評価式と割当候補１８４の論理積と等価なＤＮＦを計算して割当候補１８４に記録する割当候補計算機能１６１。
割当候補構成機能１６０の終了後に、飽和順序１８１、影響順序１８２、評価順序１８３、割当候補１８４を出力して機能の実行を終了する出力機能１７０。
【００３２】
入力機能１１０の受け取るＣＮＦのデータは、従来コンピュータでＣＮＦとして使用されるデータ構造とする。なお、空式は節を含まないＣＮＦのデータで表す。また空節は変数を含まない節からなるＣＮＦのデータで表す。
【００３３】
飽和順序追加機能１３１や飽和式構成機能１３２で節を選択するときは、ランダムに節を選択するものとする。なお、この選択がランダムではなく、入力のＣＮＦの順序やＣＮＦの節に含まれる変数の辞書順など、従来からコンピュータで使用されている順序付けにおいて小さい／大きい順で選択する場合がある。また、この他に従来のコンピュータで用いられる選択方法を用いて節を選択する場合がある。
【００３４】
割当候補計算機能１６１により論理式と等価なＤＮＦを計算する機能は、従来のコンピュータでＤＮＦを計算する時に使用されている機能とする。
【００３５】
目標式１８０のデータ構造は、従来コンピュータでＣＮＦとして使用されるデータ構造とする。
なお、目標式１８０の節は順序付けられて記録されていることがある。例えば変数を索引とする辞書順に並べられていることがある。
また目標式１８０には、ＣＮＦの他に、計算を容易にするためのデータが記録されることがある。例えば肯否変数についての検索や、それぞれの機能によって処理されたかどうかを判定するためのフラグなどである。
また目標式１８０には、ＣＮＦについての複数のデータが記録されることがある。例えば飽和順序追加機能１３１や飽和式構成機能１３２用として、あるいは評価順序追加機能１５１用として別のデータを用意することがある。飽和順序追加機能１３１や飽和式構成機能１３２は、節を処理するごとにこのデータから節を削除し、飽和順序１８１に記録されていない目標式１８０の節を構成する代用とする。また評価順序追加機能１５１も同様に、節を処理するごとにこのデータから節を削除し、評価順序１８３に記録されていない目標式１８０の節を構成する代用とする。
【００３６】
飽和順序１８１のデータ構造は、節を表す肯否変数のレコードについて、そのレコードを集めた式となるレコードを、順序の大きい式から順番に並べた配列となる。飽和順序追加機能１３１が相関関係となる節を全て取り込むため、飽和順序１８１の全ての節は、その節の含まれる式よりも大きい式とは相関関係にならない。
【００３７】
影響順序１８２のデータ構造は、基礎を表す変数のレコードを、順序の小さい基礎から順番に並べた配列となる。影響順序追加機能１４１は、最大基礎にそれまでの影響順序１８２に記録された基礎の変数を全て含むようにするため、影響順序１８２に記録された基礎は互いに包含する・されるの関係となる。また、影響順序１８２は、より大きい式の方が含まれる変数の多くなる傾向のある飽和順序１８１から構成される。よって、影響順序１８２に記録された基礎は、ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する傾向となる。
【００３８】
なお影響順序１８２に記録されるデータは、それぞれの基礎の差分となる変数の集合にすることがある。この結果、影響順序１８２のデータの重複部分を省略することが出来、データを圧縮することができる。
【００３９】
評価順序１８３のデータ構造は、節を表す肯否変数のレコードについて、そのレコードを集めた式となるレコードを、順序の小さい式から順番に並べた配列となる。評価順序１８３は、評価順序追加機能１５１によって、影響順序１８２の基礎の順序に従って順序付けられる。影響順序１８２ではより小さいの基礎の方が相関式の個数が多くなるため、評価順序１８３も相関関係にならない相関式の個数の多い節から、相関関係にならない相関式の個数の同じ節が一つの式としてまとめられるようにして順番に並べられる。
【００４０】
割当候補１８４のデータ構造はＤＮＦのレコードとなる。ＤＮＦのレコードは、従来コンピュータでＤＮＦとして使用されるデータ構造とする。なお、ＤＮＦとＣＮＦは双対の関係となるため、ＣＮＦのレコードをＤＮＦのレコードの代用とすることがある。恒真は何も式を含まないＤＮＦのデータで表す。
【産業上の利用可能性】
【００４１】
本発明のプログラム及びコンピュータ読取可能な記録媒体により、ＣＮＦＳＡＴの計算複雑性をＣＮＦの節の相関・直交関係から整理・抽出したデータ構造を記録することができるようになった。その結果、ＣＮＦＳＡＴの構造を分析したデータを記録することができ、そのデータを保存したり通信したりすることができるようになった。またそのような相関・直交関係を表すデータ構造を効率良く計算する機能をコンピュータで実現することが可能となり、またそのデータ構造を用いてＣＮＦが真となる真理値割当やＣＮＦＳＡＴを効率良く計算する機能をコンピュータで実現することが可能となった。
【符号の説明】
【００４２】
１００ 判定機能
１１０ 入力機能
１２０ 初期化機能
１３０ 飽和順序構成機能
１３１ 飽和順序追加機能
１３２ 飽和式構成機能
１３３ 飽和式
１４０ 影響順序構成機能
１４１ 影響順序追加機能
１５０ 評価順序構成機能
１５１ 評価順序追加機能
１６０ 割当候補構成機能
１６１ 割当候補計算機能
１７０ 出力機能
１８０ 目標式
１８１ 飽和順序
１８２ 影響順序
１８３ 評価順序
１８４ 割当候補
【技術分野】
【０００１】
本発明は、ＣＮＦの節同士の関係を表すデータ構造、及びコンピュータにてＣＮＦの節同士の関係を表すデータを構成するプログラム、及びＣＮＦＳＡＴを計算するプログラムに関する
【背景技術】
【０００２】
従来、コンピュータでは様々な問題が扱われており、また論理式や充足可能性問題、恒真式問題など論理に関する問題も様々なものが扱われている。
【０００３】
例えばＳＡＴ（充足可能性問題）は、ＮＰ完全問題に属し、その応用範囲も広い。特にＣＮＦ（乗法標準形）で構成されたＳＡＴであるＣＮＦＳＡＴは、ＳＡＴから多項式時間で変換可能（例えば非特許文献１参照）でありながら変換後の取り扱いが容易となるため、様々な問題で活用されている。例えば構造物などにおいて各種の拘束条件を満たす解が存在するかどうかを判定する問題や、あるいは各種パズルなどの作成や計算など様々な場面で活用されている。
【０００４】
ＣＮＦＳＡＴは本質的にコンピュータで計算するのが困難な問題であり、判定するのに実質不可能な指数規模の時間が必要になることがある。ＣＮＦＳＡＴの計算複雑性はＣＮＦの構造の複雑さにより決まる。よってＣＮＦＳＡＴをＣＮＦの構造の観点から整理することは、ＣＮＦＳＡＴを効率的に計算するために重要となる。また、ＣＮＦＳＡＴの節同士の関係はＣＮＦＳＡＴの構造を明らかにするにあたり重要となる。
【０００５】
しかし、今まではＣＮＦＳＡＴの構造を、ＣＮＦの節の関係で表現するデータ構造は存在しなかった。
【０００６】
また、複数の論理式から新たな論理式を構成する導出という演繹方法が存在する。導出とは２つの節から制約条件を変えずに追加可能な１つの節を導き出す操作である。片方の節にＡ∨Ｐという命題があり、もう片方に¬Ａ∨Ｑという命題がある時、両方の命題が同時に成立するときはＰ∨Ｑという命題も存在することを導き出す操作である。導出を用いることによって、ＣＮＦに含まれる命題を導き出して充足可否を求めることも可能である。また、この導出やその他の論理式を削除する手法をまとめたＤＬＰＰというアルゴリズムも存在する。
【０００７】
しかし、導出やＤＰＬＬアルゴリズムはある２つの命題の肯定と否定を組合せて別の命題を顕在化する操作であり、ＣＮＦのような様々なリテラルの肯定・否定が入れ混じる論理式で導出を行うのは計算の効率が悪かった。
【０００８】
また、ＣＮＦをＤＮＦ（加法標準形）にすることができれば、ＤＮＦから容易に充足可否を判定することができるが、ＣＮＦからＤＮＦへの変換は多くの計算量が必要であり、単にＤＮＦに変換して充足可否を求めるのは計算の効率が悪かった。
【先行技術文献】
【非特許文献】
【０００９】
【非特許文献１】「オートマトン 言語理論 計算論 ２」Ｊ．ホップクロフト，Ｊ．ウルマン，Ｒ．モトワニ サイエンス社 ２００８年 Ｐ１４７−１５５
【発明の概要】
【発明が解決しようとする課題】
【００１０】
本発明の解決しようとする課題は、ＣＮＦＳＡＴの計算複雑性をＣＮＦの節同士の関係から整理・抽出したデータ構造を提供する点にある。またそのデータ構造を効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。また、そのデータ構造を用いてＣＮＦＳＡＴを効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。
【課題を解決するための手段】
【００１１】
本発明で使用する用語を説明する。本発明では肯定リテラルを肯定変数、否定リテラルを否定変数、リテラルを肯否変数、リテラルを意識しない（肯否を無視する）場合は単に変数と呼ぶ。ＣＮＦを式と呼ぶ。ＣＮＦＳＡＴの対象となる式を対象式と呼ぶ。対象式の節の部分集合からなる式を部分式と呼ぶ。対象式や部分式を単に式と呼ぶことがある。節の集合と式を等価に扱うことがある。変数を含まない節を空節と呼ぶ。空節は恒偽に対応する。節を含まない式を空式と呼ぶ。空式は恒真に対応する。式や節に含まれる変数の集合を基礎と呼ぶ。基礎では変数の肯否を区別しない。空節の基礎は空集合となり、空式の基礎は任意の変数となる。基礎に含まれる変数の個数を次数と呼ぶ。
【００１２】
２つの節について、片方の節にある変数の肯定変数が、もう片方に同じ変数の否定変数が含まれる場合、その２つの節同士の関係を、その変数についての節の直交関係と呼ぶ。例えば（Ｘ∨Ｙ）は、（Ａ∨¬Ｘ）などのように¬Ｘを含む節とＸについて直交関係になり、（Ｂ∨¬Ｙ）や（Ｘ∨¬Ｙ）などのように¬Ｙを含む節とＹについて直交関係になり、（¬Ｘ∨¬Ｙ）などのように¬Ｘと¬Ｙを含む節とＸとＹについて直交関係になる。直交関係にならない節同士の関係を相関関係と呼ぶ。また、ある節Ａと式Ｂにおいて、節Ａが式Ｂの任意の節と相関関係にある時、節Ａと式Ｂの関係も相関関係と呼ぶ。同様に、ある式Ｃと式Ｄにおいて、式Ｃの任意の節が式Ｄの任意の節と相関関係にある時、式Ｃと式Ｄの関係も相関関係と呼ぶ。また、全ての節の関係が相関関係となる式を相関式と呼ぶ。空節は任意の節と相関関係に、空式は任意の節と直交関係にあるものとする。
【００１３】
なお本発明では、式や節、変数、集合、元などの計算対象を表すデータは従来のコンピュータで用いられるデータとする。バイナリ列や配列、テーブル、レコード、構造体などのデータや、変数の区切りを空白とし節の区切りを改行としたテキストデータを用いる場合もある。また変数番号の偶数奇数で変数の肯定否定を定める場合や計算対象の省略形を表すデータ構造などの場合もある。あるいは集合を表すデータで式や節を表すことがある。また計算対象を表すデータ構造が他に存在し、そのデータへの参照によって計算対象を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。このように計算対象のデータ構造は様々だが、計算対象を特定し他と区別できるデータであれば良く、これらに限定されない。
【００１４】
また、順序をグラフやリンクや配列で表す場合、この順序を表すグラフやリンクや配列は従来のコンピュータで用いられるデータであるとする。このデータには有向非循環グラフが使用されることがある。グラフやリンクや配列を表すデータは様々なものが存在するが、計算対象の順序が判れば良く、特定のものに限定されない。
【００１５】
また、本発明で用いる構成要素は、メモリ等の記憶手段やコンピュータ読取可能な記録媒体に記録・記憶され、コンピュータのデータとして活用される。なお、表記の簡単化のため、メモリ等の記憶手段に記録されたデータを、式や節、変数、集合、元、順序、グラフ、参照、などのようにそのまま表記することがある。
【００１６】
なお本発明では、論理式と等価なＤＮＦを計算する機能を実現するためのプログラムは、従来のコンピュータで用いられるプログラムを使用するものとする。
【００１７】
課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序を出力して機能の実行を終了する出力機能。
【００１８】
また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
順序付けられた式の集合のデータを受け取り、飽和順序として記録する入力機能。
影響順序に基礎が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行後に、影響順序を出力して機能の実行を終了する出力機能。
【００１９】
また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
順序付けられた基礎の集合のデータを受け取り、影響順序として記録する入力機能。
評価順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行後に、評価順序を出力して機能の実行を終了する出力機能。
【００２０】
また課題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないようにし、影響順序に基礎が含まれないようにし、評価順序に節が含まれないようにし、割当候補を恒真にする初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行中または実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行中または実行後に、評価順序の小さい式から順に、その式を評価式として割当候補計算機能を実行することを、評価順序の式全てについて行う割当候補構成機能。
他の機能から呼び出されると、評価式と割当候補の論理積と等価なＤＮＦを計算して割当候補に記録する割当候補計算機能。
割当候補構成機能の終了後に、割当候補、または飽和順序と割当候補、または飽和順序と影響順序と割当候補、または飽和順序と影響順序と評価順序と割当候補を出力して機能の実行を終了する出力機能。
【００２１】
また課題を解決するため、本発明では、対象式の全ての節が含まれる相関式の集合が記録されたコンピュータ読取可能な記録媒体とした。
【００２２】
また、上記の相関式が順序付けられており、かつ相関式に属する節は、節の属する相関式よりも大きい相関式全てと相関関係にならないものとする場合がある。
【００２３】
また課題を解決するため、本発明では、対象式に含まれる変数を元とする基礎について、次の構成（Ａ）かつ（Ｂ）となる基礎の順序が記録されたコンピュータ読取可能な記録媒体とした。
（Ａ）それぞれの基礎が互いに包含する・されるの関係にある。
（Ｂ）ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する。
【００２４】
また課題を解決するため、本発明では、対象式に含まれる節を、その節と相関関係にならない相関式の個数の多い順に並べた順序が記録されたコンピュータ読取可能な記録媒体とした。
【発明の効果】
【００２５】
本発明により、対象式の節を相関関係によって分類することができるようになった。この分類を活用することで、どの節がどの節と相関関係にあるのか、及び相関関係にならない相関式はどれなのかということを把握することができるようになった。相関関係はＣＮＦＳＡＴの計算複雑性の指標となり、この結果として対象式のＣＮＦＳＡＴの計算複雑性を把握することができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。
【００２６】
また本発明により、対象式の変数を、相関式の多い順に順序付けることができるようになった。相関式の数は直交関係の規模であり、計算複雑性の指針となる。また、相関式の多い変数は、ＣＮＦＳＡＴの構造が複雑な部分でもあるため、この結果としてＣＮＦＳＡＴを計算するときに重要となる変数を順番に並べることができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。
【００２７】
また本発明により、対象式の節を、直交関係となる相関式の多い順に順序付けることができるようになった。直交・相関関係はＣＮＦＳＡＴの計算複雑性の指標となる。また、直交関係となる相関式の多い節は、ＣＮＦＳＡＴの構造が複雑な部分でもあるため、ＣＮＦＳＡＴを計算するときに重要となる節を順番に並べることができる。また、このような関係が記録されたコンピュータ読取可能な記録媒体を提供できるようになった。
【００２８】
また本発明により、対象式の節の直交・相関関係を用いてＣＮＦＳＡＴを計算することができるようになった。節の直交・相関関係はＣＮＦＳＡＴの構造の大きな部分を占めるため、その構造の詰まった節から順番にＣＮＦＳＡＴを計算することにより、効率良く判定を行うことができる。
【００２９】
つまり、本発明のプログラム及びコンピュータ読取可能な記録媒体により、ＣＮＦＳＡＴの計算複雑性をＣＮＦの節の相関・直交関係から整理・抽出したデータ構造を記録することができるようになった。またそのような相関・直交関係を表すデータ構造を効率良く計算する機能をコンピュータで実現することが可能となった。またそのような相関・直交関係を表すデータ構造を使用してＣＮＦが真となる真理値割当を効率良く計算する機能をコンピュータで実現することが可能となった。
【図面の簡単な説明】
【００３０】
【図１】図１は本実施形態によるプログラムのブロック図である。
【発明を実施するための形態】
【００３１】
以下に本発明の実施形態の一つについて説明する。図１は本実施形態によるプログラムのブロック図である。本実施形態では、コンピュータで判定機能１００を実現させるためのプログラムとした。判定機能１００は下記機能から構成されている。
入力として受け取ったＣＮＦを目標式１８０に記録する入力機能１１０。
飽和順序１８１に式が含まれないようにし、影響順序１８２に基礎が含まれないようにし、評価順序１８３に節が含まれないようにし、割当候補１８４を恒真にする初期化機能１２０。
入力機能１１０と初期化機能１２０の実行後に、飽和順序追加機能１３１を繰り返し実行し、目標式１８０全ての節を飽和順序１８１の式に記録した後に終了する飽和順序構成機能１３０。
他の機能から呼び出されると、目標式１８０の節のうち飽和順序１８１の式に記録されていない節のいずれか１つからなる新たな飽和式１３３を記録し、飽和式構成機能１３２を実行し、飽和式１３３を飽和順序１８１に既に記録されている式よりも小さい式として飽和順序１８１に記録する飽和順序追加機能１３１。
他の機能から呼び出されると、飽和式１３３と相関関係にあると同時に飽和順序１８１の式や飽和式１３３に記録されていない目標式１８０のいずれかの節を１つ飽和式１３３に記録することを繰り返し実行し、飽和式１３３に記録できる節が無くなった時に終了する飽和式構成機能１３２。
飽和順序構成機能１３０の実行後に、飽和順序１８１の小さい式から順に、その式を対象式として影響順序追加機能１４１を繰り返し実行することを、飽和順序１８１の式全てについて行う影響順序構成機能１４０。
他の機能から呼び出されると、もしも影響順序１８２の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序１８２に記録する影響順序追加機能１４１。
影響順序構成機能１４０の実行中または実行後に、影響順序１８２の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能１５１を繰り返し実行することを、影響順序１８２の基礎全てについて行う評価順序構成機能１５０。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序１８３の式に記録されていない目標式１８０の節からなる式を、評価順序１８３に記録されている節よりも大きい節として評価順序１８３に記録する評価順序追加機能１５１。
評価順序構成機能１５０の実行中または実行後に、評価順序１８３の小さい式から順に、その式を評価式として割当候補計算機能１６１を実行することを、評価順序１８３の式全てについて行う割当候補構成機能１６０。
他の機能から呼び出されると、評価式と割当候補１８４の論理積と等価なＤＮＦを計算して割当候補１８４に記録する割当候補計算機能１６１。
割当候補構成機能１６０の終了後に、飽和順序１８１、影響順序１８２、評価順序１８３、割当候補１８４を出力して機能の実行を終了する出力機能１７０。
【００３２】
入力機能１１０の受け取るＣＮＦのデータは、従来コンピュータでＣＮＦとして使用されるデータ構造とする。なお、空式は節を含まないＣＮＦのデータで表す。また空節は変数を含まない節からなるＣＮＦのデータで表す。
【００３３】
飽和順序追加機能１３１や飽和式構成機能１３２で節を選択するときは、ランダムに節を選択するものとする。なお、この選択がランダムではなく、入力のＣＮＦの順序やＣＮＦの節に含まれる変数の辞書順など、従来からコンピュータで使用されている順序付けにおいて小さい／大きい順で選択する場合がある。また、この他に従来のコンピュータで用いられる選択方法を用いて節を選択する場合がある。
【００３４】
割当候補計算機能１６１により論理式と等価なＤＮＦを計算する機能は、従来のコンピュータでＤＮＦを計算する時に使用されている機能とする。
【００３５】
目標式１８０のデータ構造は、従来コンピュータでＣＮＦとして使用されるデータ構造とする。
なお、目標式１８０の節は順序付けられて記録されていることがある。例えば変数を索引とする辞書順に並べられていることがある。
また目標式１８０には、ＣＮＦの他に、計算を容易にするためのデータが記録されることがある。例えば肯否変数についての検索や、それぞれの機能によって処理されたかどうかを判定するためのフラグなどである。
また目標式１８０には、ＣＮＦについての複数のデータが記録されることがある。例えば飽和順序追加機能１３１や飽和式構成機能１３２用として、あるいは評価順序追加機能１５１用として別のデータを用意することがある。飽和順序追加機能１３１や飽和式構成機能１３２は、節を処理するごとにこのデータから節を削除し、飽和順序１８１に記録されていない目標式１８０の節を構成する代用とする。また評価順序追加機能１５１も同様に、節を処理するごとにこのデータから節を削除し、評価順序１８３に記録されていない目標式１８０の節を構成する代用とする。
【００３６】
飽和順序１８１のデータ構造は、節を表す肯否変数のレコードについて、そのレコードを集めた式となるレコードを、順序の大きい式から順番に並べた配列となる。飽和順序追加機能１３１が相関関係となる節を全て取り込むため、飽和順序１８１の全ての節は、その節の含まれる式よりも大きい式とは相関関係にならない。
【００３７】
影響順序１８２のデータ構造は、基礎を表す変数のレコードを、順序の小さい基礎から順番に並べた配列となる。影響順序追加機能１４１は、最大基礎にそれまでの影響順序１８２に記録された基礎の変数を全て含むようにするため、影響順序１８２に記録された基礎は互いに包含する・されるの関係となる。また、影響順序１８２は、より大きい式の方が含まれる変数の多くなる傾向のある飽和順序１８１から構成される。よって、影響順序１８２に記録された基礎は、ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する傾向となる。
【００３８】
なお影響順序１８２に記録されるデータは、それぞれの基礎の差分となる変数の集合にすることがある。この結果、影響順序１８２のデータの重複部分を省略することが出来、データを圧縮することができる。
【００３９】
評価順序１８３のデータ構造は、節を表す肯否変数のレコードについて、そのレコードを集めた式となるレコードを、順序の小さい式から順番に並べた配列となる。評価順序１８３は、評価順序追加機能１５１によって、影響順序１８２の基礎の順序に従って順序付けられる。影響順序１８２ではより小さいの基礎の方が相関式の個数が多くなるため、評価順序１８３も相関関係にならない相関式の個数の多い節から、相関関係にならない相関式の個数の同じ節が一つの式としてまとめられるようにして順番に並べられる。
【００４０】
割当候補１８４のデータ構造はＤＮＦのレコードとなる。ＤＮＦのレコードは、従来コンピュータでＤＮＦとして使用されるデータ構造とする。なお、ＤＮＦとＣＮＦは双対の関係となるため、ＣＮＦのレコードをＤＮＦのレコードの代用とすることがある。恒真は何も式を含まないＤＮＦのデータで表す。
【産業上の利用可能性】
【００４１】
本発明のプログラム及びコンピュータ読取可能な記録媒体により、ＣＮＦＳＡＴの計算複雑性をＣＮＦの節の相関・直交関係から整理・抽出したデータ構造を記録することができるようになった。その結果、ＣＮＦＳＡＴの構造を分析したデータを記録することができ、そのデータを保存したり通信したりすることができるようになった。またそのような相関・直交関係を表すデータ構造を効率良く計算する機能をコンピュータで実現することが可能となり、またそのデータ構造を用いてＣＮＦが真となる真理値割当やＣＮＦＳＡＴを効率良く計算する機能をコンピュータで実現することが可能となった。
【符号の説明】
【００４２】
１００ 判定機能
１１０ 入力機能
１２０ 初期化機能
１３０ 飽和順序構成機能
１３１ 飽和順序追加機能
１３２ 飽和式構成機能
１３３ 飽和式
１４０ 影響順序構成機能
１４１ 影響順序追加機能
１５０ 評価順序構成機能
１５１ 評価順序追加機能
１６０ 割当候補構成機能
１６１ 割当候補計算機能
１７０ 出力機能
１８０ 目標式
１８１ 飽和順序
１８２ 影響順序
１８３ 評価順序
１８４ 割当候補
【特許請求の範囲】
【請求項１】
コンピュータに下記機能を実現させるためのプログラム。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序を出力して機能の実行を終了する出力機能。
【請求項２】
コンピュータに下記機能を実現させるためのプログラム。
順序付けられた式の集合のデータを受け取り、飽和順序として記録する入力機能。
影響順序に基礎が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行後に、影響順序を出力して機能の実行を終了する出力機能。
【請求項３】
コンピュータに下記機能を実現させるためのプログラム。
順序付けられた基礎の集合のデータを受け取り、影響順序として記録する入力機能。
評価順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行後に、評価順序を出力して機能の実行を終了する出力機能。
【請求項４】
コンピュータに下記機能を実現させるためのプログラム。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないようにし、影響順序に基礎が含まれないようにし、評価順序に節が含まれないようにし、割当候補を恒真にする初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行中または実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行中または実行後に、評価順序の小さい式から順に、その式を評価式として割当候補計算機能を実行することを、評価順序の式全てについて行う割当候補構成機能。
他の機能から呼び出されると、評価式と割当候補の論理積と等価なＤＮＦを計算して割当候補に記録する割当候補計算機能。
割当候補構成機能の終了後に、割当候補、または飽和順序と割当候補、または飽和順序と影響順序と割当候補、または飽和順序と影響順序と評価順序と割当候補を出力して機能の実行を終了する出力機能。
【請求項５】
対象式の全ての節が含まれる相関式の集合が記録されたコンピュータ読取可能な記録媒体。
【請求項６】
請求項５において、相関式が順序付けられており、かつ相関式の節は、その相関式よりも大きい相関式全てと相関関係にならない相関式の集合が記録されたコンピュータ読取可能な記録媒体。
【請求項７】
対象式に含まれる変数を元とする基礎について、次の構成（Ａ）かつ（Ｂ）となる基礎の順序が記録されたコンピュータ読取可能な記録媒体。
（Ａ）それぞれの基礎が互いに包含する・されるの関係にある。
（Ｂ）ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する。
【請求項８】
対象式に含まれる節を、その節と相関関係にならない相関式の個数の多い順に並べた順序が記録されたコンピュータ読取可能な記録媒体。
【請求項１】
コンピュータに下記機能を実現させるためのプログラム。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序を出力して機能の実行を終了する出力機能。
【請求項２】
コンピュータに下記機能を実現させるためのプログラム。
順序付けられた式の集合のデータを受け取り、飽和順序として記録する入力機能。
影響順序に基礎が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行後に、影響順序を出力して機能の実行を終了する出力機能。
【請求項３】
コンピュータに下記機能を実現させるためのプログラム。
順序付けられた基礎の集合のデータを受け取り、影響順序として記録する入力機能。
評価順序に式が含まれないよう初期化する初期化機能。
入力機能と初期化機能の実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行後に、評価順序を出力して機能の実行を終了する出力機能。
【請求項４】
コンピュータに下記機能を実現させるためのプログラム。
式のデータを受け取り、目標式として記録する入力機能。
飽和順序に式が含まれないようにし、影響順序に基礎が含まれないようにし、評価順序に節が含まれないようにし、割当候補を恒真にする初期化機能。
入力機能と初期化機能の実行後に、飽和順序追加機能を繰り返し実行し、目標式全ての節を飽和順序の式に記録した後に終了する飽和順序構成機能。
他の機能から呼び出されると、目標式の節のうち飽和順序の式に記録されていない節のいずれか１つからなる新たな飽和式を記録し、飽和式構成機能を実行し、飽和式を飽和順序に既に記録されている式よりも小さい式として飽和順序に記録する飽和順序追加機能。
他の機能から呼び出されると、飽和式と相関関係にあると同時に飽和式や飽和順序の式に記録されていない目標式のいずれかの節を１つ飽和式に記録することを繰り返し実行し、飽和式に記録できる節が無くなった時に終了する飽和式構成機能。
飽和順序構成機能の実行後に、飽和順序の小さい式から順に、その式を対象式として影響順序追加機能を繰り返し実行することを、飽和順序の式全てについて行う影響順序構成機能。
他の機能から呼び出されると、もしも影響順序の最も大きな基礎（最大基礎と呼ぶ）に含まれない変数が対象式に含まれる場合は、対象式の基礎に最大基礎を加えた基礎を最大基礎よりも大きい基礎として影響順序に記録する影響順序追加機能。
影響順序構成機能の実行中または実行後に、影響順序の小さい基礎から順に、その基礎を対象基礎として評価順序追加機能を繰り返し実行することを、影響順序の基礎全てについて行う評価順序構成機能。
他の機能から呼び出されると、対象基礎のみで構成されると同時に評価順序の式に記録されていない目標式の節からなる式を、評価順序に記録されている式よりも大きい式として評価順序に記録する評価順序追加機能。
評価順序構成機能の実行中または実行後に、評価順序の小さい式から順に、その式を評価式として割当候補計算機能を実行することを、評価順序の式全てについて行う割当候補構成機能。
他の機能から呼び出されると、評価式と割当候補の論理積と等価なＤＮＦを計算して割当候補に記録する割当候補計算機能。
割当候補構成機能の終了後に、割当候補、または飽和順序と割当候補、または飽和順序と影響順序と割当候補、または飽和順序と影響順序と評価順序と割当候補を出力して機能の実行を終了する出力機能。
【請求項５】
対象式の全ての節が含まれる相関式の集合が記録されたコンピュータ読取可能な記録媒体。
【請求項６】
請求項５において、相関式が順序付けられており、かつ相関式の節は、その相関式よりも大きい相関式全てと相関関係にならない相関式の集合が記録されたコンピュータ読取可能な記録媒体。
【請求項７】
対象式に含まれる変数を元とする基礎について、次の構成（Ａ）かつ（Ｂ）となる基礎の順序が記録されたコンピュータ読取可能な記録媒体。
（Ａ）それぞれの基礎が互いに包含する・されるの関係にある。
（Ｂ）ある基礎を基準基礎とし、基準基礎とその基準基礎に含まれる基礎との差集合を差分基礎すると、基準基礎に含まれる変数が増加するに従い、差分基礎を含む節による相関式の個数が減少する。
【請求項８】
対象式に含まれる節を、その節と相関関係にならない相関式の個数の多い順に並べた順序が記録されたコンピュータ読取可能な記録媒体。
【図１】
【公開番号】特開２０１３−５４６１０（Ｐ２０１３−５４６１０Ａ）
【公開日】平成２５年３月２１日（２０１３．３．２１）
【国際特許分類】
【出願番号】特願２０１１−１９３４１３（Ｐ２０１１−１９３４１３）
【出願日】平成２３年９月５日（２０１１．９．５）
【出願人】（５９８１０８０７６）
【Ｆターム（参考）】
【公開日】平成２５年３月２１日（２０１３．３．２１）
【国際特許分類】
【出願日】平成２３年９月５日（２０１１．９．５）
【出願人】（５９８１０８０７６）
【Ｆターム（参考）】
[ Back to top ]