"コンピュータを、入力としてCNFを受け取り、出力として下記の集合の集合を出力するプログラム。CNFの項を第一成分とし、空集合を第二成分として持つ順序対。順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、それぞれの2つの項の組について、片方の項を第一成分として持ち、もう片方の項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び対象の項の差分部の肯否を入れ替えた項ただしお互い相補部共通部の肯否が一致するものは含まない全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。コンピュータを、入力としてCNFを受け取り、出力として下記の集合の集合を出力するプログラム。CNFの項を第一成分とし、空集合を第二成分として持つ順序対。順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、共通項を第一成分として持ち、共通部を持つ項のいずれか一つの項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び相補項の肯否を入れ替えた項ただし対象の項の相補部と肯否が一致するものは含まない全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。請求項1、2において、CNFの項を第一成分とし空集合を第二成分として持つ順序対を計算する代わりに、CNFの項をそのまま順序対の代用として使用して計算を行うプログラム。請求項1、2、3において、空集合を第一成分とし、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対を計算するプログラム。請求項1、2、3、4において、集合の集合を出力する代わりに、下記の項を持つHornCNFを出力するプログラム。順序対に含まれる項に代えてHornCNFの変数とする。順序対に代えて、順序対の第一成分をHornCNFの変数の肯定リテラルとし、順序対の第二成分の要素をHornCNFの変数の否定リテラルとして持つHornCNFの項とする。請求項1、2、3、4において、集合の集合を出力する代わりに、下記の有向グラフを出力するプログラム。順序対の要素を構成するのに代えて、有向グラフの頂点を構成する。順序対を構成するのに代えて、第二成分の集合に含まれる項に対応する頂点から第一成分の項に対応する頂点への有向辺を構成する。請求項1、2、3、4において、集合の集合を出力する代わりに、下記の値を出力するプログラム。順序対の数。順序対に含まれる要素の合計。浸出項の変数の最大値。浸出項の数。空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。前述をランダムに選択した標本から算出した値。コンピュータを、入力としてCNFを受け取り、出力として下記の値を出力するプログラム。CNFの項のうち、相補部を持つ項同士の組合せの数。請求項1、2、3、4、5、6において、データを出力する代わりに、CNFSATの計算結果を出力するプログラム。上記の通り、SATの構造を活用して効率的に問題を判定する汎用性の高いSAT解法が存在しなかった。論理式の充足可能性を効率的に求めることのできるHornCNFの形式に変換するプログラムが存在しなかった。SATの難易度を効率的に評価するプログラムが存在しなかった。上記問題を解決するため、本発明では、コンピュータを、入力としてCNFを受け取り、出力として下記の集合の集合を出力するプログラムとした。CNFの項を第一成分とし、空集合を第二成分として持つ順序対。順序対の第一成分として出現する項それぞれの、その項のお互いに共通の変数が存在しかつ共通の変数の肯否が全て一致する本特許ではこの部分を共通部と呼ぶ。また共通部にあるリテラルからなる項を共通項と呼ぶ項同士について、それぞれの2つの項の組について、片方の項を第一成分として持ち、もう片方の項及びその項の共通部に含まれない部分本特許では差分部と呼ぶ。また差分部にあるリテラルからなる項を差分項と呼ぶの肯否を入れ替えた項の集合を第二成分として持つ順序対。順序対の第一成分として出現する項それぞれの、その項のお互いに共通の変数が存在するがその共通の変数のいずれかの肯否が異なる本特許ではこの部分を相補部と呼ぶ。また相補部にあるリテラルからなる項を相補項と呼ぶ項同士について、対象の項の相補部に入らない部分を全て合わせた項本特許ではこの全ての差分部を集めた部分を浸出部と呼ぶ。また浸出部にあるリテラルからなる項を浸出項と呼ぶを第一成分として持ち、対象の項及び対象の項の差分部の肯否を入れ替えた項ただしお互い共通部の肯否が一致するものは含まないの集合を第二成分として持つ順序対。空集合を第一成分として持ち、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対。上記問題を解決するため、本発明では、コンピュータを、入力としてCNFを受け取り、出力として下記の集合の集合を出力するプログラムとした。CNFの項を第一成分とし、空集合を第二成分として持つ順序対。順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、共通項を第一成分として持ち、共通部を持つ項のいずれか一つの項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び相補項の肯否を入れ替えた項ただし対象の項の相補部と肯否が一致するものは含まない全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。空集合を第一成分として持ち、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対。また上記プログラムにおいて、CNFの項を第一成分とし空集合を第二成分として持つ順序対は入力のCNFから容易に構成可能なため、入力をそのまま使用する場合や、出力に含まない場合がある。また上記プログラムにおいて、空集合を第一成分として持ち要素として現れた項それぞれについてその項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対は他の順序対から容易に構成可能なため、計算を行わずに出力に含めない場合がある。また上記プログラムにおいて、共通部や相補部に対応する順序対において、共通項や相補項に対応する項を持つ場合と持たない場合が混在する場合がある。なお集合や順序対の構成は通常プログラムで行われる方法を用いる。項そのものを配列やテーブルなどのレコードで構築する場合もあり、項のデータを別に用意してそのデータへの参照を配列やテーブルなどのレコードで構築する場合もあるが、これらに限らない。また上記プログラムにおいて、集合の集合を出力する代わりに、下記の項を持つHornCNFを出力するプログラムとすることがある。順序対に含まれる項に代えてHornCNFの変数とする。順序対に代えて、順序対の第一成分をHornCNFの変数の肯定リテラルとし、順序対の第二成分の要素をHornCNFの変数の否定リテラルとして持つHornCNFの項とする。この場合、第一成分が空集合の順序対には目的項が対応し、第二成分が空集合の順序対には事実項が対応する。第一成分も第二成分も空集合にならない順序対は規則項に対応する。このような順序対を構成することで、CNFの持つ構造を扱いやすい形に再構成するため、CNFSATを計算やその難易度の評価を簡単にすることができる。なお、HornCNFは、変数が順序対の項に、項が順序対に対応するため、下記でも暗黙的にその対応関係を用いる場合がある。また上記プログラムにおいて、後の計算の容易化のため、同じ変数から構成される項を要素として持つ順序対の集合を用意する場合がある。同様に、同じリテラルから構成される順序対の集合を用意する場合がある。このようにすることで、同じ変数からなる項や同じリテラルからなる項がどの順序対に存在するかを見つけやすくし、計算を容易化する。また上記プログラムにおいて、集合の集合を出力する代わりに、下記の有向グラフを出力する場合がある。順序対の要素を構成するのに代えて、有向グラフの頂点を構成する。順序対の第一成分と第二成分を構成するのに代えて、第二成分の集合に含まれる項に対応する頂点から第一成分の項に対応する頂点への有向辺を構成する。この場合、空集合も頂点として存在する。なお、有向グラフは、頂点が順序対の項に、辺が順序対に対応するため、下記でも暗黙的にその対応関係を用いる場合がある。このグラフは充足性について半順序を持つため、空集合に繋がる有向辺の起点となる頂点目的項に対応するを考えた時に、その頂点を終点とする経路事実項と、それによって確定される規則項に対応するが全て空集合起点となる場合は充足不可となるため、比較的容易に充足可否を判定することができる。また上記プログラムにおいて、集合の集合を出力する代わりに、下記の値を出力する場合がある。順序対の数。順序対に含まれる要素の合計。浸出項の変数の最大値。浸出項の数。空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。前述をランダムに選択した標本から算出した値。また上記問題を解決するため、コンピュータを、CNFの項のうち、相補部を持つ項同士の組合せの数を出力するとした。この結果、CNFSATを実際に計算せずに難易度を評価することができる。また上記プログラムにおいて、データを出力する代わりに、CNFSATを計算してその充足可否や充足条件の計算結果をデータとして出力することもある。また、上記プログラムにおいて、論理式を受け取った時はCNFまたは3CNFに変換することとしたプログラムとすることもある。本発明により、CNFの持つ構造を活用して、コンピュータで取り扱いやすいデータ形式、特にHornCNFや半順序を持つ有向グラフの形に変形することが可能となった。またその結果を用いて効率的にSATをコンピュータで処理することが可能となった。さらに、SATの難易度を効率的に評価することが可能となった。以下に本発明の実施形態の一つについて、図面に基づき説明する。図1は本発明のプログラムの構成図である。本プログラムは以下の構成となる。論理式を受け取りCNFに変換する入力部111。入力部111から受け取ったCNFを元に、各項の関係を表すデータに変換する変換部112。変換したデータを出力する出力部113。また、変換部が作成したデータを元に充足可否を判定するSAT判定部121、及びSAT判定部121の結果を出力する判定結果出力部122が存在することもある。また、変換部が作成したデータを元にSATの難易度を評価するSAT評価部131、及びSAT評価部131の結果を出力する評価結果出力部132が存在することもある。入力部111の詳細を説明する。入力部111はメモリ、ストレージ、IO、他のプログラムなど、通常のコンピュータで使用される入出力部からの入力を受け取る。受け取った入力が論理式の条件を満たしている場合は入力をCNFに変換して変換部112に出力する。プログラムによっては正規化を一段進めて3CNFに変換する場合もある。論理式からCNFや3CNFへの変換は通常用いられる方法を用いる例えば非特許文献3参照。また、変換部112に出力する際に、CNFや3CNFを作成するときに付加した変数を識別可能なように渡すことがある。例えば変数にCNFに変換するときに付加した変数、あるいは3CNFに変換するときに付加した変数であることがわかるように、変数に識別子を付けたり、変数の一覧を別途データとして渡したりすることがある。CNFを作成するときに付加する変数は肯定リテラルと否定リテラルの数が同数になり、また3CNFを作成する時に付加する変数は肯定リテラルと否定リテラルがそれぞれ一つの項にしか出てこない。よって、このような特徴を、充足可能性を判定するときに活用することで判定を効率化することができる。入力は論理式及び論理式の変数の満たす条件で構成される。論理式や論理式を表すバイナリ列など、通常用いられる論理式の省略形を表現したデータを受け取ることも可能とするが、この内容に制限されない。また、入力が論理式の条件を満たしていない場合は入力を拒否する。拒否の方法は通常のプログラムで計算失敗として行われている動作を用いる。例えば判定結果出力部122がある場合は充足不可として判定結果出力部122に出力する場合や、単に入力を無視する場合などである。また通常のプログラムで行われている動作特殊な値の出力、例外の発行なども行うことがあるが、この内容に制限されない。変換部112の詳細を説明する。変換部112は、入力部111からの出力としてCNFを受け取ると、CNFの項を共通の変数を持つ集合に分類する。そして共通の変数を持つ集合のうち、同じ肯否を持つ組合せと異なる肯否を持つ組合せを作成し、それぞれについて順序対を作成する。ここで、順序対を作成する代わりに有向グラフを作成する場合がある。有向グラフは順序対の作成と同様の手順にて作成することができる。順序対あるいは有向グラフの作成は、下記の手順にて行う。まずはCNFから、CNFの項を第一成分とし、空集合を第二成分として持つ順序対を作成する。この項はHornCNFの事実項に対応する項でもあり、空集合を条件として持つ無条件に真となる必要のある条件を意味する。ただし、この事実項に対応する順序対はCNFの各項から容易に作成することができるため、CNFの各項を順序対の第一成分に読み替えて使用する場合もある。また、出力にこの順序対を含まずCNFを含む場合、あるいはまったく含まない場合がある。次に、これまでに作成した順序対の第一成分に含まれる項入力のCNFの項も含むについて、お互いに共通の変数を含む組合せを計算し、その組合せに関係する順序対を計算する。この順序対はHornCNFの規則項に相当する。まだ計算を行っていない組合せがある場合、共通の変数の全ての肯否が同じ場合と、共通の変数のいずれかの肯否が異なる場合の、全ての組合せについて順序対の計算を行う。まず、共通の変数の全ての肯否が同じ場合の詳細を述べる。この場合、共通項は必ず真偽が同じになるため、ある項で共通部が真となる場合は別の項でも真となり、ある項で共通部が偽となる場合は別の項でも偽となる。この条件をHornCNFの規則項を意識して順序対で構成すると次のようになる。共通部を持つ項同士のうちある項を第一成分とし、別の項の差分部の肯否全ての場合を集めた集合を第二成分とする。例えば、順序対の第一成分にX0V¬X2VX4とX0V¬X2VX6があった場合、ある項をX0V¬X2VX4、別の項をX0V¬X2VX6とすると、この時の順序対はX0V¬X2VX4,X0V¬X2VX6,X0V¬X2V¬X6となる。当然、ある項をX0V¬X2VX6、別の項をX0V¬X2VX4とした場合も考慮する必要があり、この時の順序対はX0V¬X2VX6,X0V¬X2VX4,X0V¬X2V¬X4となる。次に、共通の変数のいずれかの肯否が異なる場合の詳細を述べる。この場合、相補項が同時に真となることは無いため、対象の項が全て真になる場合は浸出部のいずれかが真となる。この条件をHornCNFの規則項を意識して順序対で構成すると次のようになる。浸出項を第一成分とし、対象の項及び対象の項の差分部の肯否を入れ替えた項ただしお互い共通部の肯否が一致するものは含まないの集合を第二成分とする。この順序対の計算は、お互いに相補部を持つ項の組合せ全ての場合について行う必要がある。例えば、順序対の第一成分にX0V¬X2VX4とX0VX2VX6があった場合、この順序対の一つの例はX4VX6,X0V¬X2VX4,¬X0VX2VX4,¬X0V¬X2VX6,X0VX2VX6となる。当然、上記順序対の¬X0VX2VX4及び¬X0V¬X2VX6は恣意的に選択した項であり、この項である必要はない。例えばX4VX6,X0V¬X2VX4,¬X0VX2VX6,¬X0V¬X2VX4,X0VX2VX6X4VX6,X0V¬X2VX4,¬X0VX2VX6,¬X0V¬X2VX6,X0VX2VX6などとすることもできる。また、3つ以上の項の関係も2つの項の関係と同様に計算する必要がある。例えば、X0V¬X2VX4X0VX2VX6¬X0VX2V¬X8の場合、この順序対の一つの例はX4VX6V¬X8,X0V¬X2VX4,X0VX2VX6,¬X0VX2VX8,¬X0V¬X2VX8となる。当然、この場合でも2つの項の関係をそれぞれ別に計算する必要がある。また、上記において効率化のために共通項相補項を用意してその順序対とすることもできる。例えば上記の共通部についてはX0V¬X2,X0V¬X2VX6,X0V¬X2V¬X6X0V¬X2,X0V¬X2VX4,X0V¬X2V¬X4とすることができ、上記の相補部についてはX4VX6,X0V¬X2VX4,X0VX2VX6,¬X0VX2,¬X0V¬X23つの項の場合はX4VX6V¬X8,X0V¬X2VX4,X0VX2VX6,¬X0VX2VX8,¬X0V¬X2Vとすることができる。全ての第一成分の項の組合せについて順序対の計算を行った後に、次の手順で順序対を計算する。この順序対はHornCNFの目的項に相当するこれまでに作成した順序対に含まれる項全てについて、その項に含まれるリテラルの肯否全ての組合せの項全てを集めた集合を第二成分とし、空集合を第一成分とする順序対とする。例えば、¬X0V¬X2Vという項が含まれる場合、この順序対はφ,X0VX2V,¬X0VX2V,X0V¬X2V,¬X0V¬X2Vとなる。ただし、この目的項に相当する順序対は規則項から容易に作成することができるため、計算しない場合がある。また、出力としてこの順序対を含まない場合がある。前述の事実項に対応する順序対も含まない場合は、規則項に対応する順序対しか出力しないことになる。なお、順序対は、順序対を構成する項をそれぞれの変数に、第一成分の項をその対応する変数の肯定リテラルとし、第二成分の集合に含まれる項をそれぞれ対応する変数の否定リテラルとする項に変換することで、容易にHornCNFの項に変換することができる。よって、変換部112は順序対を出力する代わりにHornCNFを計算して出力することがある。なお、順序対の計算と同様の手順にて有向グラフを作成することができるため、変換部112は順序対を計算する代わりに有向グラフを計算して出力することがある。また、変換部112は後の計算が容易になるよう、順序対あるいは有向グラフに付加的な情報を追加することがある。例えば、同じ変数で構成される項の関係は重要となるため、その項を含む順序対あるいは頂点の集合を別途出力することがある。同様に、同じリテラルで構成される項の関係は重要となるため、その項を含む順序対の集合を別途出力することがあるこれは有向グラフの頂点と一致する。変換部112は、このようにして構成したデータを出力部113、SAT判定部121、SAT評価部131に出力する。出力部113の詳細を説明する。出力部113は、変換部112からの入力を変換したデータを受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、データ作成の途中で生成したデータなどを含むことがある。他のプログラムはこのデータを活用してSAT計算やデータ解析などの処理を行う。また、出力部113の出力したデータには、SATの潜在的な構造が顕在化された形で表現されているため、このデータを用いることでSATの構造の解析が容易となっている。そのため、SATの難易度の評価を、実際に計算を始める前に見積もることができる。SAT判定部121の詳細を説明する。SAT判定部121は、変換部112からデータを受け取ると、データを活用してHornCNFに読み替えて充足可能性を判定する。変換部112のデータは、それぞれの部分を読み替えることでHornCNFとして捉えることができる。また、変換部112から有向グラフを受け取った場合は、空集合に繋がる有向辺の起点となる頂点目的項に対応するを考えた時に、その頂点を終点とする経路事実項と、それによって確定される規則項に対応するが全て空集合起点となる場合は充足不可となるため、このことを確認することで充足可否を判定することもできる。なお、ここで作成した順序対HornCNF、有向グラフは、順序対の第一成分の増殖性からもわかるように、CNFの構造によっては最悪指数規模の規模となり、その規模を小さいものに変換することが本質的にできない。そのため、計算によってはある程度の計算難易度の見積りを行い、必要に応じて計算を打ち切る、あるいはデータ処理の優先順位を付けることが重要となる。例えば、後述のSAT評価部131によるSAT難易度によって、本特許による順序対の構築を行わず、乱択アルゴリズムによる解法に切り替えるなどである。SAT判定部121は、判定結果を判定結果出力部122に出力する。判定結果出力部122の詳細を説明する。判定結果出力部122は、SAT判定部121から判定結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部111や変換部112、SAT判定部121から計算過程結果のデータを受け取ることがある。SAT評価部131の詳細を説明する。SAT評価部131は、変換部112からデータを受け取ると、データの構造から充足可能性の判定難易度を評価する。評価を行った後、その結果を評価結果出力部132に出力する。前述の通り、CNFをHornCNFに変換する時のHornCNFの規模は浸出項の構造によって大きく変化する。そこで、SAT評価部131は変換部112から受け取ったデータの浸出項の構造を分析し、CNFの難易度を評価する。この難易度の評価にはいくつか方法がある。具体的には次の通りである。項の数を難易度とする。順序対の数を難易度とする。浸出項の数を難易度とする。浸出項を第一成分とする順序対の数を難易度とする。浸出項の第一成分とする順序対の数を難易度とする。などである。あるいは浸出項の変数の数の最大値を難易度とする、などのこともある。あるいは空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。などのこともある。またはこれらの評価を重み付きで組合せることで全体の評価を行うこともある。また、前述の評価を行う際に、全ての場合について計算を行うのではなく、ランダムに選択した標本から計算することもある。この場合、乱択アルゴリズムなどを活用することがある。評価結果出力部132の詳細を説明する。評価結果出力部132は、SAT評価部131から評価結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部111や変換部112、SAT評価部131から計算過程結果のデータを受け取ることがある。以下に本発明の別の実施形態について、図面に基づき説明する。図2は本発明のプログラムの構成図である。本プログラムは以下の構成となる。論理式を受け取りCNFに変換する入力部211。入力部211から受け取ったCNFを元に、CNFSATの難易度を計算する評価部212。評価した結果を出力する出力部213。入力部211は、入力部111と同様の機能となる。入力を受け取り、評価部212にCNFを出力する。出力部213は、出力部111と同様の機能となる。評価部212からデータを受け取り、出力を行う。評価部212の詳細を説明する。評価部212はCNFを受け取ると、CNFに含まれる項全てについて、それぞれ相補部を含む項同士の組合せの数を求める。その組合せの数を出力部213に送る。このような構成とすることで、簡易的にCNFSATの難易度を評価することができる。前述の例よりも難易度判定の精度が落ちるが、前述の例よりもはるかに短い時間で難易度の判定を行うことができる。"