"対象CNFと、対象CNFの調和CNFが記録されたコンピュータ読み取り可能な記録媒体。請求項1において、調和CNFが調和変数組をキーとする索引あるいは冪索引のレコードとして記録された、コンピュータ読み取り可能な記録媒体。請求項1~2いずれかの項において、同じ相関CNFを構成する全ての調和CNFを参照するデータが記録された、コンピュータ読み取り可能な記録媒体。請求項1~3いずれかの項において、対象CNFから導出した浸出CNFの一部または全てが記録された、コンピュータ読み取り可能な記録媒体。請求項4項において、浸出CNFの一部または全てが対応する調和CNFに記録され、浸出CNFを含む調和CNFの組合せから導出した浸出CNFも浸出CNFに含めて記録された、コンピュータ読み取り可能な記録媒体。請求項4~5いずれかの項において、対象CNFと浸出CNFの節のうち簡約可能な節が削除されて記録された、コンピュータ読み取り可能な記録媒体。請求項4~6いずれかの項において、浸出CNFに空節が含まれる場合、対象CNFが充足不可であるということを表すデータが記録された、コンピュータ読み取り可能な記録媒体。コンピュータに下記機能を実現させるためのプログラム。CNFのデータを受け取り、未分類CNFに追加して記録する入力機能。未分類CNFから節を選択して対象節として抽出して未分類CNFから削除して記録し、調和変数組をキーとし調和CNFをレコードとして記録された調和CNF冪索引を用いて対象節から調和CNFを調和CNF冪索引にレコードが存在しない場合は追加しながら冪検索して抽出し、抽出した調和CNF全てに対象節を追加して記録する分類機能。未分類CNFの全ての節が分類機能により分類された後に、記録されている調和CNF冪索引を出力して機能の実行を終了する出力機能。コンピュータに下記機能を実現させるためのプログラム。CNFのデータを受け取り、未分類CNFに追加して記録する入力機能。未分類CNFから節を選択し対象節として抽出し未分類CNFから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。調和変数組をキーとし調和CNFをレコードとして記録された調和CNF冪索引を用いて、対象節から調和CNFをレコードが存在しない場合は追加しながら冪検索し、もしも冪検索した調和CNFの中に極小調和CNFが存在しない場合、冪検索した調和CNFを全て抽出し、抽出した調和CNFのうち節が存在しない調和CNFに対して下記の作成機能を適用し、抽出した調和CNFに対して下記の追加機能を適用し、対象節を極小調和CNFとする調和CNFに対して下記の削除機能を適用する検索機能。それぞれの調和CNFに対応する相関CNF同じ相関CNFからなる調和CNFの集合に、その調和CNFを追加して記録する作成機能。それぞれの調和CNFに対して対象節を追加して記録し、同じ対象節を持つ調和CNFの集合を所属CNFとして記録する追加機能。対象節を極小調和CNFとする調和CNFが極小調和CNFでない場合は、その調和CNFに含まれる節のうち対象節を除いた節を削除CNFとして抽出し、削除CNFのそれぞれの節について、その節の所属CNFに含まれる全ての調和CNFからその節を削除して記録する削除機能。未分類CNFの全ての節が分類機能により分類された後に、記録されている調和CNF冪索引を出力して機能の実行を終了する出力機能。コンピュータに下記機能を実現させるためのプログラム。CNFのデータを受け取り、未分類CNFに追加して記録する入力機能。未分類CNFから節を選択し対象節として抽出し未分類CNFから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。調和変数組をキーとし調和CNFをレコードとして記録された調和CNF冪索引を用いて、対象節から調和CNFをレコードが存在しない場合は追加しながら冪検索し、もしも冪検索した調和CNFの中に極小調和CNFが存在しない場合、冪検索した調和CNFを全て抽出し、抽出した調和CNFのうち節が存在しない調和CNFに対して下記の作成機能を適用し、抽出した調和CNFに対して下記の追加機能を適用し、対象節を極小調和CNFとする調和CNFに対して下記の削除機能を適用する検索機能。それぞれの調和CNFに対応する相関CNF同じ相関CNFからなる調和CNFの集合に、その調和CNFを追加して記録する作成機能。それぞれの調和CNFに対して対象節を追加して記録し、同じ対象節を持つ調和CNFの集合を所属CNFとして記録する追加機能。対象節を極小調和CNFとする調和CNFが極小調和CNFでない場合は、その調和CNFに含まれる節のうち対象節を除いた節を削除CNFとして抽出し、削除CNFのそれぞれの節について、その節の所属CNFに含まれる全ての調和CNFからその節を削除して記録する削除機能。調和CNF冪索引から、導出済CNFでない節を含む調和CNFを選択して導出CNFとして抽出し、導出CNFと同じ相関CNFに属する調和CNFを錯綜CNFとして抽出し、導出CNFの導出済CNFでない節全てを未導出CNFとして抽出して導出CNFから削除して記録し、全ての錯綜CNFの導出済CNFと未導出CNFを組み合わせてできる全ての完備相関CNFから浸出CNFを構成し、浸出CNFを未分類CNFに追加して記録し、未導出CNFを導出CNFの導出済CNFに追加して記録し、浸出CNFに空節が含まれるかどうかを出力する導出機能。もし導出機能が充足不可であることを記録した場合は充足不可であることを出力して機能の実行を終了し、あるいは未分類CNFの全ての節が分類機能により分類されて全ての調和CNFの全ての節が導出済CNFとして記録された場合は、充足可能であることを出力して機能の実行を終了する出力機能。請求項10において、下記の機能が追加されたプログラム。追加機能にて、調和CNFに対象節を追加する際に、その調和CNFを未導出調和CNF集合に追加する。導出機能にて、未導出CNFを含む調和CNFを選択する際に、未導出調和CNF集合から調和CNFを選択して導出CNFとして抽出して未導出調和CNF集合から削除して記録する。請求項10~11いずれかの項において、出力機能が充足可能であることを出力する際に、調和CNF冪索引のレコードから不備相関CNFを構成し、その不備相関CNFに含まれない極小調和CNFを全て偽とする真理値割当を集めて出力する機能が追加されたプログラム。請求項10~12いずれかの項において、出力機能が出力する際に、記録されている調和CNF冪索引も出力する機能が追加されたプログラム。本発明の解決しようとする課題は、CNFSATの計算複雑性をCNFの構造から整理抽出したデータ構造を提供する点にある。また上記データ構造をCNFSATから効率良く構成する機能をコンピュータで実現させるためのプログラムを提供する点にある。また、上記データ構造を用いてCNFSATを効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。まず、本発明で使用する用語を説明する。本発明では肯定リテラルを肯定変数、否定リテラルを否定変数、リテラルを肯否変数、リテラルを意識しない肯否を無視する場合は単に変数と呼ぶ。また、単数または複数の変数の組合せを変数組、変数組に含まれる変数の部分集合となる変数組を部分変数組と呼ぶ。また、あるCNFの節の部分集合からなるCNFを部分CNFと呼ぶ。また、CNFのある節と他の節の両方に含まれる変数の一部または全てを集めた変数組を相関変数組と呼ぶ。ある変数の組合せを含む節が複数存在しない場合でも、その変数の組合せを相関変数組と呼ぶことがある。また、相関変数組の部分変数組を部分相関変数組と呼ぶ。なお、簡単のため、相関変数組と部分相関変数組を合わせて単に相関変数組と呼ぶことがある。同じ相関変数組の節を全て集めたCNFを相関CNFと呼ぶ。なお、相関CNFには対になる相関変数組が存在する。また肯定変数否定変数肯否変数についても、それぞれの変数組や相関変数組を、肯定変数組否定変数組肯否変数組、肯定相関変数組否定相関変数組肯否相関変数組と呼ぶ。また、節に含まれる変数から相関変数組に含まれる変数を除いた変数組を分離変数組と呼ぶ。分離変数組についても同様に、それぞれの肯定変数否定変数肯否変数を肯定分離変数組否定分離変数組肯否分離変数組と呼ぶ。また、ある節の相関変数組の部分を相関部、分離変数組の部分を分離部と呼ぶ。また、同じ相関変数組を含む節同士の関係を相関関係と呼ぶ。また相関関係のうち、肯否相関変数組の一致する関係を調和関係と呼び、肯否相関変数組の異なる関係を錯綜関係と呼ぶ。同様に相関~~と呼ぶものについて、肯否相関変数組の一致するものを調和~~、異なるものを錯綜~~と呼ぶ。また、相関CNFのうち、お互いに調和関係にある節で構成されるCNFを調和CNFと呼ぶ。また、ある調和CNFと錯綜関係にある単数あるいは複数の調和CNFで構成されるCNFを調和CNFの錯綜CNFと呼ぶ。また、ある節について、その節を含む調和CNFを所属CNFと呼ぶ。また、調和CNFと対になる肯否相関変数組を、特に調和変数組と呼ぶ。なお、調和CNFのうち、その調和CNFの調和変数組のみで構成されている節のみからなる調和CNFを極小調和CNFと呼ぶ。極小調和CNFは、そのCNFに調和CNFの条件を満たすどのような節を追加したとしても、簡約律によりただ一つの節になる調和CNFである。例えば{X,¬Y,¬Z}が調和変数組となる極小調和CNFはX∨¬Y∨¬Zとなる。{X,¬Y,¬Z}を調和変数組とする調和CNFはX∨¬Y∨¬Z∨......のように{X,¬Y,¬Z}を含む任意の節で構成することができる。しかし極小調和CNFはX∨¬Y∨¬Zを含むため、調和CNFの節を全てこの節に簡約することができる。なお、コンピュータでの取り扱いを容易にするため、極小調和CNFに調和CNFの節を追加した簡約化前のCNFは極小調和CNFとは呼ばないこととする簡約化により極小調和CNFに変形することはできる。ある相関CNFを考える。その相関CNFの相関変数組の取り得る肯否相関変数組それぞれについて調和CNFが存在するとする。この時、それぞれの調和CNFから1つずつ節を取り出して構成したCNFを相関CNFの完備相関CNFと呼ぶ。つまり、完備相関CNFはその相関関係について互いに錯綜関係となる節のみを集めた、全ての錯綜関係が存在するCNFである。また完備相関CNFの各節から、その相関変数組の分離肯否変数を集めた節を浸出節と呼ぶ。完備相関CNFは、どの真理値割当でもいずれかの節の相関部が必ず偽となる。よって、完備相関CNFを含むCNFにおいて浸出部が充足不可の場合は、CNF全体も充足不可となる。つまり、完備相関CNFには浸出節で表される潜在的な制約が存在し、浸出節を導くことにより顕在化することができる。本発明では完備相関CNF~浸出節を導く操作を相関導出、あるいは単に導出と呼ぶ。相関導出は導出の拡張であり、相関変数組が変数1つの場合は導出と同じ操作となる。完備相関CNFから任意の節を取り除いたCNFを不備相関CNFと呼ぶ。不備相関CNFからは完備相関CNFを構成することができない。また完備相関CNFに、相関変数組が同じだが完備相関CNFに含まれない節を追加したCNFを過剰相関CNFと呼ぶ。過剰相関CNFからは複数の完備相関CNFを構成することができる。それぞれの調和CNFからいずれか1つの節を選択して組合せたCNFは完備相関CNFとなる。なお、ある相関CNFで複数種類の完備相関CNFが構成可能な場合、それぞれの完備相関CNFからそれぞれ異なる浸出節を導出することができる。つまり、過剰相関CNFには複数の完備相関CNFが畳み込まれていると言う事ができる。ここで、ある相関CNFの取り得る全ての完備相関CNFの浸出節を合わせたCNFを相関CNFの浸出CNFと呼ぶ。なお簡単のため、単独の浸出節も浸出CNFと呼ぶ。複数の相関CNFについての浸出CNFを組み合わせたCNFもまた浸出CNFと呼ぶことがある。ここで具体例として3CNFを考える。肯否変数をA、B、C、Dとした時に、次の3CNFの相関CNF{X}を考える。A∨B∨X∧C∨D∨¬Xこの3CNFは相関変数組{X}の完備相関CNFとなり、浸出節A∨B∨C∨Dを導出することができる。次に、上記の3CNFに節を追加した下記の相関CNF{X}を考える。A∨B∨X∧A∨C∨X∧C∨D∨¬X∧B∨D∨¬Xこの相関CNF{X}は、同じ調和CNFから1つずつ選択した組合せそれぞれの完備相関CNFを考えることができる。つまり下記の4通りとなる。A∨B∨X∧C∨D∨¬X、A∨B∨X∧B∨D∨¬X、A∨C∨X∧C∨D∨¬X、A∨C∨X∧B∨D∨¬Xまた、上記の完備相関CNFそれぞれについて浸出節が存在するため、この相関CNF{X}の浸出CNFは次のようになる。A∨B∨C∨D∧A∨B∨D∧A∨C∨D∧A∨C∨B∨Dこの関係は相関変数組の変数が2つの3CNFの場合も同様となる。例えば、肯否変数をA、B、C、Dとした時に、下記の相関CNF{X,Y}を考える。A∨X∨Y∧B∨¬X∨Y∧C∨X∨¬Y∧D∨¬X∨¬Yこの3CNFは相関変数組{X,Y}の完備相関CNFとなり、浸出節A∨B∨C∨Dを導出することができる。同じ肯否相関変数組が存在する場合も同様となる。Eを肯否変数とする次の相関CNF{X,Y}を考える。Aを含む節とEを含む節が同じ調和CNFとなる。A∨X∨Y∧B∨¬X∨Y∧C∨X∨¬Y∧D∨¬X∨¬Y∧E∨X∨Yこの相関CNF{X,Y}でも、同じ調和CNFから1つずつ節を選択した組合せそれぞれの完備相関CNFを考えることができる。つまり下記の2通りとなる。A∨X∨Y∧B∨¬X∨Y∧C∨X∨¬Y∧D∨¬X∨¬Y、E∨X∨Y∧B∨¬X∨Y∧C∨X∨¬Y∧D∨¬X∨¬Yそして、上記の完備相関CNFそれぞれについて浸出節が存在するため、相関CNF{X,Y}の浸出CNFは次のようになる。A∨B∨C∨D∧E∨B∨C∨Dまた、上記の場合、相関変数組{X,Y}だけではなく、その部分集合の相関変数組{X}{Y}も同様に相関CNFを考えることができる。相関CNF{X}{Y}の浸出CNFの組み合わせでも上記結果を導くことが可能だが、単に相関CNF{X,Y}の浸出CNFの構成を優先する場合は、相関導出の方が効率良く計算できる。この延長線として、節の変数全てが相関変数組となる相関CNFを考えることもできる。ただし、この場合は分離部が存在しないため、空節を導出することに注意する必要がある。例えば、下記の3CNFの相関CNF{X,Y,Z}を考える。X∨Y∨Z∧¬X∨Y∨Z∧X∨¬Y∨Z∧X∨Y∨¬Z∧X∨¬Y∨¬Z∧¬X∨Y∨¬Z∧¬X∨¬Y∨Z∧¬X∨¬Y∨¬Zこの相関CNF{X,Y,Z}には、全ての肯否相関変数組に対応する節が存在し、完備相関CNFとなる。しかし分離部が存在しないため浸出節は空節となる。つまり、このCNFは真になることができず充足不可となる。なお、上記の関係は3CNFに限定されず、CNF一般について成り立つ。また、既に全ての浸出CNFを導出しているCNFを導出済CNFと呼ぶ。これは相関CNFの部分CNFも同様とする。つまり、ある相関CNFの部分CNFのうち、その部分CNFの範囲では全ての浸出CNFを導出している部分CNFも相関CNFの導出済CNFと呼ぶ。なお、相関CNFの導出済CNF以外の部分CNFを未導出CNFと呼ぶことがある。導出済CNFと未導出CNFの節を組み合せることにより、新たに浸出CNFを導出できる場合がある。なお本発明では、CNFや節、変数を表すデータは従来のコンピュータで用いられるデータとする。バイナリ列や配列、テーブル、レコード、構造体などのデータとする場合や、変数の区切りを空白とし節の区切りを改行としたテキストデータとする場合もある。また変数番号の偶数奇数で変数の肯定否定を定める場合もある。あるいはCNFや節、変数の省略形を表すデータ構造などの場合もある。またCNFや節、変数を表すデータ構造が他に存在し、そのデータへの参照によってCNFや節、変数を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。また、節を表すデータとして、その節に含まれる肯否変数への参照などのデータを集めたデータを用いる場合もある。同様に、CNFを表すデータとして、CNFを構成する節への参照などのデータを集めたデータを用いる場合もある。また、CNFを表すデータに、そのCNFの特徴を表すデータを含める場合がある。例えば相関CNFが、その相関CNFに対応する相関変数組を含む場合がある。また相関CNFが、その相関CNFに含まれる調和CNFのデータを含む場合がある。調和CNFが、その調和CNFの錯綜CNFとなる調和CNFへの参照を含む場合がある。あるいは調和CNFが、その調和CNFを含む相関CNFへの参照を含む場合がある。また、節が所属する相関CNFや調和CNFへの参照を含む場合がある。また、CNFを表すデータに、そのCNFのある性質を持つCNFが区別されて記録されている場合がある。例えば調和CNFのうち、その相関CNFにおける導出済CNFと未導出CNFがそれぞれわかるように記録されていることがある。また後述のように調和CNFに分類される前の節と分類された後の節を、それぞれわかるように別々に記録することがある。このようにCNFや節、変数のデータ構造は様々なものがあるが、CNFや節、変数を特定し他と区別できるデータであれば良く、これらに限定されない。また変数組を表すデータは従来のコンピュータで変数の組合せを表すのに用いられるものとする。バイナリ列や配列、テーブル、レコード、構造体などのデータとする場合や、変数の区切りを空白としたテキストデータとする場合もある。また変数組を表すデータが他に存在し、そのデータへの参照によって変数組を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。また前述のCNFや節、変数との組合せで用いるデータとする場合もある。例えばCNFや節、変数を表すデータへの参照などである。参照はポインタやアドレスの場合もある。またCNFが配列やレコードの時は、その配列やレコードの要素を特定する添字やタグの場合もある。このように変数組を表す様々なデータ構造があるが、変数の組合せを表すデータ構造であれば良く、上記の例に限定されない。また、データの集合を表すデータも同様に、従来のコンピュータで複数のデータを表す方法として用いられるデータとする。配列やリスト、リンクリスト、循環リスト、テーブル、レコード、構造体、テキストデータなどがあるが、複数のデータをまとめて表すデータ集合を表すデータであれば良く、これらに限定されない。なお、本発明において索引のデータを使用する場合があるが、その索引のデータは従来のコンピュータでキーからレコードを検索する時に使用する索引のデータとする。例えばB木B木、B木や2分探索木、ハッシュ索引、トライ木、パトリシア木などである。このように索引のデータ構造は様々なものがあるが、キーとなるデータからレコードとなるデータを検索することのできる索引のデータとなっていれば良く、これらに限定されない。また、同様に本発明において、あるキーとなるデータから、そのキーの全ての部分集合をキーとするレコードを全て検索する時に使用する索引を用意する場合がある。この索引を特に冪索引と呼ぶ。また、冪索引から対応するレコード全てを検索することを冪検索と呼ぶ。例えば、相関肯否変数組をキーとする冪索引があるとする。この冪索引で{X,Y,Z}という相関肯否変数組をキーとして冪検索した場合、その結果は{X,Y,Z}の部分相関肯否変数組をキーとする検索結果、すなわち{X,Y,Z}{Y,Z}{X,Z}{X,Y}{X}{Y}{Z}をキーとする検索結果のレコード全ての集合となるなお、{}をキーとする検索結果を含む場合もある。この冪索引のデータを構成する方法はいくつか存在する。例えば、{X,Y,Z}に対応するレコードに{X,Y,Z}の部分集合のレコード全てを含むようにする場合である。なおこの場合、レコードの重複を避けるため、対応するレコードは全て参照としてデータそのものとは別に保存する場合がある。また、レコードを階層的に持つことで効率化することがある。例えば、あるキーのレコードは、そのキーの部分集合をキーとするレコードを参照として持つ場合である。また、冪索引として通常の索引と同様のデータ構造を使用し、冪検索する時の検索方法を工夫することで対応する場合がある。例えば、データ構造として検索木を使用する場合、キーの部分集合を列挙しながら検索を行うことで冪検索を実現する場合がある。たとえはキーの部分集合を、その有無がグレイコードの順番になるように並べた順番で検索する場合や、キーを辞書順に並べた順番で検索するなどの検索方法である。こうすることで、同じ検索経路となるキーを集中して検索することができる。その結果、冪索引の冪検索で、検索木の同じ経路を辿ることなく効率的に対象を網羅することができる。このように冪索引の冪検索を実現するデータ構造機能は様々なものが存在するが、あるキーからそのキーの部分集合をキーとする全てのレコードの集合を検索できれば良く、これらに限定されない。また、集合から要素を選択する機能を使用することがあるが、コンピュータに選択する機能を実現させるためのプログラムは従来のプログラムで用いられるものとする。例えば要素を辞書順に並べた順番に選択する、要素の大きさの大きい順、または要素の大きさの小さい順に選択する、先に追加された要素から選択する、後に追加された要素から選択する、集合からランダムに選択する、などである。なお、CNFからある節を選択する、節からある変数を選択する、冪索引の全てのレコードから1つのレコードを選択する、なども同様とする。また、本発明で用いるそれぞれの構成要素は、メモリ等の記憶手段やコンピュータ読み取り可能な記録媒体に記録記憶され、コンピュータのデータとして活用される。なお、表記の簡単化のため、メモリ等の記憶手段に記録されたデータを、CNFや節、変数、変数組、索引、冪索引、集合、要素、あるいはそれらへの参照、などのように、そのまま表記することがある。これより本発明の説明を行う。上記問題を解決するため、本発明では、対象となるCNFと、その対象となるCNFの調和CNFが記録されたコンピュータ読み取り可能な記録媒体とした。なお、本発明では、この対象となるCNFを対象CNFと呼ぶ。対象CNFは任意のCNFであり、全てのCNFが対象CNFになることができる。つまり、上記は対象CNFの構造を調和関係で整理したデータとなる。CNFの節はお互いに調和関係にある節同士の関係で全体の構造を構成する。そのため、CNFの調和関係を整理することで、その構造の複雑性を明らかにすることができる。なお、上記の調和CNFは、対象CNFの節への参照の集合となることがある。調和CNFに含まれる節は対象CNFに含まれるため、調和CNFの節を参照で表すことで節を繰り返し記録する必要が無くなり、記憶領域を節約することができる。また上記の調和CNFが、その調和CNFの調和変数組のデータを含んで記録されている場合がある。こうすることで、その調和CNFの調和変数組が何かを容易に判定することができる。また上記の調和CNFと調和変数組が、調和変数組をキーとして調和CNFをレコードとする索引、あるいは冪索引として記録されている場合がある。こうすることで、ある調和変数組に対応する調和CNFを容易に検索できるようになる。また上記において、同じ相関CNFを構成する全ての調和CNFを参照するデータが記録されている場合がある。例えば、同じ相関CNFとなる調和CNF同士が循環リストによって環状に参照しており、その参照を辿ることで、同じ相関CNFの他の調和CNFすなわち錯綜CNF全てを参照することができるようになっていることがある。あるいは、相関CNFとなるデータが存在し、その相関CNFと調和CNFの相互参照が含まれる場合がある。こうすることで、相関CNFから浸出CNFを構成するときに完備相関CNFを構成するのを効率的に行えるようになる。また上記のコンピュータ読み取り可能な記録媒体に記録されたデータが、上記の相関CNFの一部または全ての浸出CNFを含んで記録されている場合がある。浸出CNFは相関CNFの潜在的な制約であり、対象CNFに導出した浸出CNFを追加したとしてもその充足可否は変わらない。よって潜在的な制約を浸出CNFとして顕在化することで、対象CNFの充足可否を変えずに、その対象CNFの計算複雑性を明らかにすることができる。なお、浸出CNFは対象CNFと同様のデータとして記録されている。また上記のコンピュータ読み取り可能な記録媒体に記録されたデータにおいて、上記の浸出CNFの一部あるいは全ての節が対応する調和CNFに記録されている場合がある。なお、浸出CNFを含む調和CNFを組合せた相関CNFから新たに異なる浸出CNFが導出できる場合は、その新たに導出した浸出CNFも元の浸出CNFに含めて記録されている。こうすることで浸出CNFによる潜在的な制約をさらに顕在化することができ、対象CNFの構造をさらに詳細に明確化することができる。なお上記の調和CNFにて、調和CNFに含まれるCNFのうち、いずれかの節が他の節を簡約律により簡約可能な場合、そのCNFでは複数の節がその簡約した節に置き換わって記録されている場合がある。このようにすることで調和CNFの構成をCNFの充足可否を変えずに簡素化することができる。また、調和CNFと調和CNFに含まれる節がお互いに参照可能となっていることがある。例えば調和CNFが対象CNFの節との双方向参照の集合となっており、対象CNFの節から全ての調和CNFを参照することができるようになっていることがある。このようにすることで、ある簡約可能な節が複数の調和CNFに含まれる場合でも効率的に簡約することができる。また、上記の浸出CNFに空節が含まれる場合は、対象CNFが充足不可だということを表すデータが上記のコンピュータ読み取り可能な記録媒体に含まれて記録されている場合がある。こうすることで、全ての浸出CNFの節を確認することなく、対象CNFが充足不可であることを判定することができる。また上記問題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。CNFのデータを受け取り、未分類CNFに追加して記録する入力機能。未分類CNFから節を選択して対象節として抽出して未分類CNFから削除して記録し、調和変数組をキーとし調和CNFをレコードとして記録された調和CNF冪索引を用いて対象節から調和CNFを調和CNF冪索引にレコードが存在しない場合は追加しながら冪検索して抽出し、抽出した調和CNF全てに対象節を追加して記録する分類機能。未分類CNFの全ての節が分類機能により分類された後に、記録されている調和CNF冪索引を出力して機能の実行を終了する出力機能。プログラムをこのような構成とすることで、コンピュータにCNFSATの計算複雑性を表す調和CNFを構成させることができるようになる。また上記問題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。CNFのデータを受け取り、未分類CNFに追加して記録する入力機能。未分類CNFから節を選択し対象節として抽出し未分類CNFから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。調和変数組をキーとし調和CNFをレコードとして記録された調和CNF冪索引を用いて、対象節から調和CNFをレコードが存在しない場合は追加しながら冪検索し、もしも冪検索した調和CNFの中に極小調和CNFが存在しない場合、冪検索した調和CNFを全て抽出し、抽出した調和CNFのうち節が存在しない調和CNFに対して下記の作成機能を適用し、抽出した調和CNFに対して下記の追加機能を適用し、対象節を極小調和CNFとする調和CNFに対して下記の削除機能を適用する検索機能。それぞれの調和CNFに対応する相関CNF同じ相関CNFからなる調和CNFの集合に、その調和CNFを追加して記録する作成機能。それぞれの調和CNFに対して対象節を追加して記録し、同じ対象節を持つ調和CNFの集合を所属CNFとして記録する追加機能。対象節を極小調和CNFとする調和CNFが極小調和CNFでない場合は、その調和CNFに含まれる節のうち対象節を除いた節を削除CNFとして抽出し、削除CNFのそれぞれの節について、その節の所属CNFに含まれる全ての調和CNFからその節を削除して記録する削除機能。未分類CNFの全ての節が分類機能により分類された後に、記録されている調和CNF冪索引を出力して機能の実行を終了する出力機能。プログラムをこのような構成とすることで、コンピュータに浸出CNFを構成する時に必要となる調和CNFを構成させることができるようになる。さらに、調和CNFを構成している時に、並行して簡約律による簡約化を行うため、より効率良く実行することができる。また同じ相関CNFとなる調和CNF同士の集合を構成することにより、浸出CNFを構成するのが容易となる。なお、作成機能により作成される相関CNFは、前述の様々な集合とすることができるが、特に索引と循環リストが重要となる。索引は、同じ相関CNF毎に作成した、相関変数組をキーとして調和CNFの集合をレコードとするものである。循環リストは、同じ相関CNFとなる調和CNF同士を循環リストで接続したものである。索引の場合、調和CNFに参照などを追加することなく、調和CNFの集合を調和CNF自体から切り離して用意することができる。そのため、調和CNFへの影響を最小限に抑えながらデータ構造を実現することができる。循環リストの場合、調和CNFに循環リストのデータ構造を用意する必要があるが、同じ調和CNFを検索するための索引を調和CNF冪索引と共用することができ例えば肯定相関変数のみの調和CNFを相関CNFの代表とすることにより、共用を実現できる、データの大きさを効率化することができる。また追加機能により記録される所属CNFの集合も、前述の様々な集合とすることができる。特に索引と双方向参照が重要となる。索引は、同じ節毎に作成した、調和変数組をキーとして調和CNFの集合をレコードとするものである。双方向参照は、対象節と所属CNFの参照をそれぞれの節CNFに記録したものである。索引の場合、対象節に参照などを追加することなく、調和CNFの集合を対象節から切り離して用意することができる。そのため、対象節への影響を最小限に抑えながらデータ構造を実現することができる。双方向参照の場合、その整合性の維持をどのように行うかを考える必要がある。例えば、同じ対象節は唯一のデータとなるように記録し、調和CNFはそのデータへの参照として記録するなどを行い、双方向参照の整合性を保ち易くする工夫が必要となる。また上記問題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。CNFのデータを受け取り、未分類CNFに追加して記録する入力機能。未分類CNFから節を選択し対象節として抽出し未分類CNFから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。調和変数組をキーとし調和CNFをレコードとして記録された調和CNF冪索引を用いて、対象節から調和CNFをレコードが存在しない場合は追加しながら冪検索し、もしも冪検索した調和CNFの中に極小調和CNFが存在しない場合、冪検索した調和CNFを全て抽出し、抽出した調和CNFのうち節が存在しない調和CNFに対して下記の作成機能を適用し、抽出した調和CNFに対して下記の追加機能を適用し、対象節を極小調和CNFとする調和CNFに対して下記の削除機能を適用する検索機能。それぞれの調和CNFに対応する相関CNF同じ相関CNFからなる調和CNFの集合に、その調和CNFを追加して記録する作成機能。それぞれの調和CNFに対して対象節を追加して記録し、同じ対象節を持つ調和CNFの集合を所属CNFとして記録する追加機能。対象節を極小調和CNFとする調和CNFが極小調和CNFでない場合は、その調和CNFに含まれる節のうち対象節を除いた節を削除CNFとして抽出し、削除CNFのそれぞれの節について、その節の所属CNFに含まれる全ての調和CNFからその節を削除して記録する削除機能。調和CNF冪索引から、導出済CNFでない節を含む調和CNFを選択して導出CNFとして抽出し、導出CNFと同じ相関CNFに属する調和CNFを錯綜CNFとして抽出し、導出CNFの導出済CNFでない節全てを未導出CNFとして抽出して導出CNFから削除して記録し、全ての錯綜CNFの導出済CNFと未導出CNFを組み合わせてできる全ての完備相関CNFから浸出CNFを構成し、浸出CNFを未分類CNFに追加して記録し、未導出CNFを導出CNFの導出済CNFに追加して記録し、浸出CNFに空節が含まれるかどうかを出力する導出機能。もし導出機能が空節を含むと出力した場合は充足不可であることを出力して機能の実行を終了し、あるいは未分類CNFの全ての節が分類機能により分類されて全ての調和CNFの全ての節が導出済CNFとして記録された場合は、充足可能であることを出力して機能の実行を終了する出力機能。プログラムをこのような構成とすることで、CNFの潜在的な制約を顕在化し、CNFの充足可否を判定することができる。プログラムをこのような構成とすることで、コンピュータにCNFの潜在的な制約を顕在化させて、CNFの充足可否を判定させることができるようになる。なお、導出機能による浸出CNFの構成を効率化するために、導出済CNFでない節を含む調和CNFを識別可能なようにすることがある。具体的には下記の通り機能を追加する。なお、ここの未導出調和CNF集合とは、導出済CNFでない節を含む調和CNFを集めた集合である。追加機能にて、調和CNFに対象節を追加する際に、その調和CNFを未導出調和CNF集合として記録する機能を追加する。導出機能にて、未導出CNFを含む調和CNFを選択する際に、未導出調和CNF集合から選択して導出CNFとして抽出して未導出調和CNF集合から削除して記録する機能を追加する。このようにすることで、導出機能が全て導出済CNFとなっている調和CNFを選択することが無くなり、効率化することができる。なお、本プログラムによる機能は容易に並列化することができる。まず分類機能と導出機能はお互いに影響を与えないで機能させることが可能である。未分類CNFと未導出CNFがそれぞれの機能のインターフェイスとなる。しかし、分類機能は未分類CNFから節を削除して未導出CNFに節を追加するのみ、導出機能は未導出CNFから節を削除して未分類CNFに節を追加するのみの動作となる。この節の動きは一方向であるため、CNFへの節の追加削除の機能自体の整合性が保たれていれば、データの整合性は保たれる。よって未分類CNFや未導出CNFの整合性を保つことにより、分類機能と導出機能はそれぞれ独立して動作させることができる。同様に、分類機能自身も複数並列して実行することが可能である。分類機能は必要な節を未分類CNFから抽出すると、すぐに未分類CNFから削除して記録することとなっている。そのため、その抽出~削除の間だけ排他処理を行えば、他の分類機能が未分類CNFを参照しても整合性は保たれる。同様に、導出機能自身も複数並列して実行することが可能である。導出機能は相関CNFの全ての錯綜CNFの導出済CNFと導出CNFの未導出CNFから完備相関CNFを構成し、浸出CNFを構成する。そのため、導出中の相関CNFについて導出の間だけ排他処理を行えば、他の導出機能が導出を行っていない相関CNFを参照しても整合性は保たれる。また、上記の出力機能において、充足可能であることを出力する際に、調和CNF冪索引のレコードから不備相関CNFを構成し、その不備相関CNFに含まれない極小調和CNFを偽とする真理値割当を集めて出力する場合がある。不備相関CNFに含まれない極小調和CNFを偽とする真理値割当は、つまりは対象CNFを真とする真理値割当の一部であり、その真理値割当を集めることにより、対象CNF全体を真にする真理値割当を求めることができる。本発明により、CNFSATの潜在的な制約を顕在化することが可能となり、CNFSATの計算複雑性に関連するCNFの構造を整理抽出したデータ構造を実現できた。またそのようなデータを構成する機能をコンピュータで実現することが可能となった。また、そのようなデータ構造を活用してCNFSATを計算する機能をコンピュータで実現することが可能となった。以下に本発明の実施形態の一つについて説明する。図1は本例によるデータ構成図である。本例ではA∨X∧C∨¬Xの実施形態を挙げるが、他のCNFについても同様のデータ構成となる。本データ構造には、対象となるCNFのデータとなる対象CNFが記録されている。本例では対象CNF101が記録されており、対象CNF101にはその節となる、A∨Xに対応する節111、C∨¬Xに対応する節112が記録されている。また、対象CNFの調和関係を表す調和CNFも記録されている。本例では、調和変数組が{X}となる調和CNF121、{¬X}となる調和CNF122、{A,X}となる調和CNF123、{C,¬X}となる調和CNF124、{C}となる調和CNF125、{A}となる調和CNF126によって表される。対象CNFの節に含まれる調和変数組は以上となる。他の調和変数組による調和CNFも考えることができるが、対象CNFの構造を表すのには重要でないため、本例では省略する。調和CNFはそれぞれ同じようなデータ構造をしているが、図にはそのうち調和CNF121を代表して詳細を記載する。調和CNF121、及び調和CNF121と調和変数組の一致する節111には、お互いへの双方向参照が記録されている。そのため、調和CNF121から節111を参照することも可能であり、逆に節111から調和CNF121を参照することも可能である。同様に、調和CNF122と節112、調和CNF123と節111、調和CNF124と節112、調和CNF125と節112、調和CNF126と節111には、それぞれへの双方向参照が記録されている。また、相関変数組の一致する調和CNF121と調和CNF122には、同じ相関CNFとなる調和CNFへの循環リストが記録されている。この循環リストを辿ることにより、ある調和CNFの錯綜CNFを抽出することが可能である。また、調和CNF123のように他の調和CNFが存在しない場合は、循環リストの取り扱いを容易にするために、自分自身への参照が記録されている。また、本データ構造には調和CNFの中に導出済CNFが記録されているとする。例えば調和CNF121の中には導出済CNF131が記録されている。同様に、調和CNF122の中には導出済CNF132が、調和CNF123の中には導出済CNF133が、調和CNF124の中には導出済CNF134が、調和CNF125の中には導出済CNF135が、調和CNF126の中には導出済CNF136が記録されている。なお、未導出CNFの節は導出済CNFに含まれない調和CNFの節となる。また、本データ構造では調和CNF冪索引141が記録されており、調和CNF冪索引141により、調和変数組から調和CNFを冪検索できるようになっている。本例の調和CNF冪索引141は、調和変数組をキーとして調和CNFをレコードとする二分木となっている。また、本データ構造には、浸出CNF171が記録されている。もしも調和CNF121と調和CNF122から導出を行った場合、その浸出節A∨Cは浸出CNF171に記録される。この浸出CNF171に記録されるデータは、対象CNF101と同様に節のデータが記録され、調和CNFなどから参照される。また、本データ構造には、まだ調和CNFに分類していない節を集めた未分類CNF151が記録されている。もしも調和CNF121と調和CNF122から導出を行った場合、その浸出節A∨Cは浸出CNF171に記録されたあと、その参照が未分類CNFに記録される。なお、未分類CNFをさらに対象CNFとして扱い、浸出節を調和CNFに分類することもある。また、本データ構造には未導出調和CNF集合161も記録されている。本例では調和CNF121の節111が未導出CNFとなっており、他の調和CNFの節は全て導出済CNFに記録されている。そのため、未導出調和CNF集合161には調和CNF121が記録されている。以下に本発明の実施形態の一つについて説明する。本例は前述のデータ構造を使用して対象CNFの構造を顕在化するプログラムである。図2は本例のフローチャートである。フローチャートでは、機能の分岐条件や機能を切り分けて記載している。具体的には分岐203~処理204は分類機能、分岐205~分岐210は導出機能、処理211、212は出力機能となる。本例では、まず開始201より処理を開始すると、入力機能となる処理202により入力として受け取ったCNFのデータを未分類CNFに追加して記録する。次に、分岐203で未分類CNFに節が存在するかの判定を行う。節が存在する場合は分類機能となる処理204を適用し、さもなければ分岐205に移行する。処理204は、未分類CNFの節の調和CNFへの分類を行う。処理204の詳細なフローチャートを図3に示す。まず始めに処理302により未分類CNFから対象節を選択する。選択する方法は前述の通常のプログラムで使用される方法とするが、本例では未分類CNFに最後に追加された節を選択するとする。次に検索機能となる処理303により、調和CNF冪索引から、対象節の調和変数組及び調和部分変数組に対応する調和CNFを冪検索する。検索した調和CNFに極小調和CNFが存在する場合、対象節は簡約律により簡約化できるため、これ以上の処理は行わず分岐304で終了309に分岐する。極小調和CNFが存在しない場合は、分岐304で分類処理に分岐する。まず処理305で冪検索した調和CNFを全て抽出し、作成機能となる処理306により、もしも相関CNFに含まれない調和CNFが存在する場合は相関CNFへの追加を行う。処理306は、調和CNFに節が存在するかどうかで相関CNFへの追加を行うかどうかの判定を行う。一度処理された調和CNFには必ず節が存在するため、節の含まれない調和CNFは初めて現れた調和CNFと考えることができる。そこで、処理306では節の含まれない調和CNFを抽出し、その調和CNFに対応する相関変数組を構成し、相関変数組に対応する相関CNFを検索する。なお、処理306は簡単化のため、相関変数組を全て肯定変数からなる調和変数組で代用し、また相関CNFも全て肯定変数からなる調和CNFで代用する。つまり全て肯定変数からなる調和CNFは、たとえCNFに節が含まれないとしても相関CNFの代用として相関CNFに含まれることになる。そのため、全て肯定変数からなる調和CNFは特別扱いする必要があり、もしも対象節が全て肯定変数で構成される場合は処理306による処理を行わない。次に追加機能となる処理307により、調和CNFに対象節を追加する。この際に、もしも調和CNFの未導出CNFに節が含まれない場合は、その調和CNFを未導出調和CNF集合に追加する。次に削除機能となる処理308により、対象節により簡約化される節の削除を行う。まず対象節を極小調和CNFとする調和CNFを抽出する。この調和CNFに含まれる節は全て対象節によって簡約化される節となる。なお、この調和CNFには処理307によって追加された対象節も存在するため、まずはこの調和CNFから対象節を除いた節を削除CNFとして抽出する。そして、削除CNFのそれぞれの節から、その節の属する調和CNFを抽出し、その節を削除する。節にはその節の所属する調和CNFへの参照が双方向参照として含まれるため、その参照を辿ることにより節を削除する必要のある調和CNFを抽出することができる。この削除を全ての調和CNFについて行った後に、その節自体の削除を行う。この削除を、削除CNFに含まれる節全てについて行う。この結果、簡約化される節は全て削除され、対象節が調和CNFに残ることになる。処理308を実行した後は終了309に移行し、処理204を終了する。処理204は、終了後に再び分岐203に移行する。分岐203で未分類CNFに節が存在しない場合は、導出機能に移行する。導出機能は、まず分岐205で導出済CNFでない節のある調和CNFが存在するかどうかを判定する。存在する場合はその節を導出CNFとして抽出して処理206に移行し、存在しない場合は出力機能となる処理212に移行する。処理206では、まず導出CNFと同じ相関CNFに属する調和CNFを錯綜CNFとして抽出する。同じ相関CNFに属する調和CNFは、循環リストによりお互いに参照可能なため、この循環リストを辿ることで全ての錯綜CNFを抽出する。次に分岐207にて、錯綜CNFが浸出CNFを導出する条件を満たすかどうかを判定する。条件を満たす場合は処理209に移行し、満たさない場合は処理208に移行する。判定する条件の1つは、錯綜CNFの導出済CNFに節を含まないCNFが存在しないかである。錯綜CNFの導出済CNFに節が存在しない場合は浸出CNFの導出を行うことができない。よって、錯綜CNFに節を含まないCNFが存在する場合は浸出CNFが存在しないということで処理208に移行する。判定する条件の1つは、錯綜CNFの数が相関変数組の変数の数を指数とする2の冪乗となるかである。相関CNFが完備相関CNFを構成するためには、その調和CNFの種類の数が最大数存在しなくてはならない。種類の数の最大数は変数の数をNとすると2^Nただし^は冪乗を表すとなるため、錯綜CNFは2^N-1になる必要がある。もしも錯綜CNFの数が2^N-1未満の場合は、相関CNFは不備相関CNFとなるため、浸出CNFを導出できない。よって、錯綜CNFが2^N-1未満の場合は処理208に移行する。処理208では導出CNFの全ての節を導出済CNFに変更して記録し、分岐203に移行する。次に、処理209に移行する。処理209では、まず導出CNFから導出済CNFでない節全てを未導出CNFとして抽出し、導出CNFから削除して記録する。そして、未導出CNFと錯綜CNFの導出済CNFそれぞれから1つの節を取り出す組合せ全てについて完備相関CNFを構成して浸出節を構成し、この浸出節を全ての組合せについて構成することで複数の浸出節を構成し、構成した浸出節を浸出CNFに追加して記録し、その参照を未分類CNFに追加して記録する。そして分岐210に移行する。また、もしも浸出CNFに空節が含まれる場合は、対象CNFは充足不可となることが確定する。そのため分岐210で浸出CNFに空節が含まれるかどうかの判定を行い、もしも含まれる場合は出力機能となる処理211に移行する。もしも空節が含まれない場合は、分岐203に移行して未分類CNFの処理を継続する。処理211は結果の出力となる。まず計算結果として調和CNF冪索引を出力し、かつ対象CNFが充足不可なことを出力する。そして終了213に移行する。処理212は結果の出力となる。まず計算結果として調和CNF冪索引を出力し、かつ対象CNFが充足可能なことを出力する。さらに調和CNF冪索引のレコードから不備相関CNFを構成し、その不備相関CNFに含まれない極小調和CNFを全て偽とする真理値割当を集めて出力する。そして終了213に移行する。このように本例のプログラムを構成することで、対象CNFの複雑性を表す相関CNFと、対象CNFの充足可否を計算する機能をコンピュータに実現させることができるようになる。以下に本発明の実施形態の一つについて説明する。本例は前述のプログラムにおいて、導出機能を未導出CNF単位ではなく相関CNF単位で行うものである。具体的には上記プログラムにおいて導出機能となる処理209が下記の処理409となったプログラムである。処理409は、処理209と異なり、相関CNFから全ての未導出の浸出CNFを構成する。つまり、処理409は処理209を一度適用すると、導出CNFの循環リストを辿り、錯綜CNFを導出CNFとして導出を繰り返す。これを全ての相関CNFについて繰り返す。このように、相関CNFについて一括して導出を行うことで、導出CNFの選択などのオーバーヘッドを抑えることができる。"