論理式変換プログラム、ＳＡＴ解法プログラム、及びＳＡＴ難易度評価プログラム
【課題】充足可能性問題は、その対象となる式の構造により難易度が変わるが、ＳＡＴの式を正規化して効率的に構造を抽出する汎用性の高いＳＡＴ解法が存在しなかった。また、ＣＮＦをＨｏｒｎＣＮＦに効率的に変換するプログラムが存在しなかった。
【解決手段】ＣＮＦをその構造に従って解析する。ＣＮＦの共通の変数を持つ項同士の関係を正規化し、順序対やＨｏｒｎＣＮＦ、有向グラフに変換することとした。また、その順序対やＨｏｒｎＣＮＦ、有向グラフに変換したＣＮＦを使用することで効率的にＳＡＴを解くこととした。また、ＣＮＦの計算困難性の重要な点である相補部を持つ項同士の関係からＣＮＦＳＡＴの計算困難性を見積もることとした。
【解決手段】ＣＮＦをその構造に従って解析する。ＣＮＦの共通の変数を持つ項同士の関係を正規化し、順序対やＨｏｒｎＣＮＦ、有向グラフに変換することとした。また、その順序対やＨｏｒｎＣＮＦ、有向グラフに変換したＣＮＦを使用することで効率的にＳＡＴを解くこととした。また、ＣＮＦの計算困難性の重要な点である相補部を持つ項同士の関係からＣＮＦＳＡＴの計算困難性を見積もることとした。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータにて論理式を変換するプログラム、及び充足可能性問題を扱うプログラム、及び充足可能性問題の難易度を評価するプログラムに関する
【背景技術】
【０００２】
従来、コンピュータでは様々な問題が扱われており、また論理式や充足可能性問題、恒真式問題など論理に関する問題も様々なものが扱われている。
【０００３】
特にＳＡＴ（充足可能性問題）は、ＮＰ完全問題として非決定性チューリングマシンと等価であることが判明しており、またその応用範囲も広い。そのため、コンピュータで自動的に解決する様々なＳＡＴ解法（ＳＡＴソルバ）が研究・実用化されている。
【０００４】
ＳＡＴは条件により様々な種類が存在する。特にＣＮＦ（乗法標準形）で構成されたＣＮＦＳＡＴと、３ＣＮＦ（項のリテラルが３つまでに限定されたＣＮＦ）で構成された３ＳＡＴが重要である。ＳＡＴはＣＮＦＳＡＴや３ＳＡＴに変換可能であり（例えば非特許文献３参照）、また変換後のＣＮＦや３ＣＮＦは取り扱いが容易なため、ＳＡＴ解法でも始めにＳＡＴをＣＮＦＳＡＴや３ＳＡＴに変換する手法が用いられている。
【０００５】
また、特別なＣＮＦの一つとしてＨｏｒｎＣＮＦと２ＣＮＦがある。ＨｏｒｎＣＮＦは各項に０または１の肯定リテラルが存在するＣＮＦである。本出願では１つの肯定リテラルのみからなる項を事実項、肯定リテラルが１つのみで残りが否定リテラルとなる項を規則項、否定リテラルのみからなる項を目的項と呼ぶこととする。また、２ＣＮＦは項の変数が２つまでに限定されたＣＮＦである。本出願ではＨｏｒｎＣＮＦと同様に規則項、目的項を定める。また、ＨｏｒｎＣＮＦには存在しない肯定リテラルを２つ含む項を関連項と呼ぶこととする。なお、式に含まれる全ての変数の肯否を入れ替えることによってＨｏｒｎＣＮＦにすることのできる論理式も存在する。本質的にはＨｏｒｎＣＮＦと同じとなるため、以降ではそのような論理式もＨｏｒｎＣＮＦとして扱う。
【０００６】
ＨｏｒｎＣＮＦや２ＣＮＦはコンピュータで効率的に充足可能性の判定を行うことが可能（例えばＤＰＬＬアルゴリズム）だが、ＣＮＦからＨｏｒｎＣＮＦや２ＣＮＦに効率的に変換する方法は存在しない。
【０００７】
またＳＡＴは本質的にコンピュータで計算するのが困難な問題であり、判定するのに問題の規模の指数倍の時間が必要になることがある。また、確率的な乱択アルゴリズムで充足可能なことを求める確率的ＳＡＴ解法もあるが、このようなＳＡＴ解法でも充足不可を判定するのは困難である。そのため、全ての可能性を判定し充足不可を明確化する完全ＳＡＴ解法の効率化が重要となる（例えば特許文献１参照）。またＳＡＴは問題毎に難易度が大幅に異なるため、難易度を評価することも重要となる。
【０００８】
しかし、従来の完全ＳＡＴ解法や確率的ＳＡＴ解法は、充足可能である条件から式を簡約するＤＰＬＬアルゴリズム（例えば非特許文献１参照）や、可能性のある真理値割当を実際に式に適用する手法などが主であり、問題の構造を活用して効率化する手法は少なかった。また、式の構造そのものに着目してＳＡＴ解法を効率化する手法はあったが（例えば非特許文献２参照）、特定の条件を満たす必要のあるものがほとんどであり応用範囲が狭かった。また、充足解の計算時間を調整することで、充足解を計算する時の負担を軽減する技術（例えば特許文献２参照）があるが、実際に計算を行う必要があるため、必ずしも効率化になるとは限らなかった。そして、ＳＡＴの難易度を効率的に評価する方法も無かったため、計算時間などを効率的に評価する方法も存在しなかった。
【０００９】
なお、ＳＡＴを効率良く扱うために、ＳＡＴで与えられた式をＳＡＴ解法のために効率の良い形に変更することも重要となるが、そのようなプログラムにおいて、論理式をＨｏｒｎＣＮＦに効率良く変換するプログラムは存在しなかった。
【先行技術文献】
【特許文献】
【００１０】
【特許文献１】特開２００４−３５５０３８
【特許文献２】特開２００５−２９３５７５
【００１１】
【非特許文献１】″Ａ Ｃｏｍｐｕｔｉｎｇ Ｐｒｏｃｅｄｕｒｅ ｆｏｒ Ｑｕａｎｔｉｆｉｃａｔｉｏｎ Ｔｈｅｏｒｙ″Ｍａｒｔｉｎ Ｄａｖｉｓ、Ｈｉｌａｒｙ Ｐｕｔｎａｍ Ｊｏｕｒｎａｌ ｏｆ ｔｈｅ ＡＣＭ ７ １９６０年 Ｐ２０１−２１５
【非特許文献２】「基本対称関数に基づく節をもつＣＮＦ論理式の充足可能性判定」馬野洋平，酒井正彦，西田直樹，坂部俊樹，草刈圭一朗 電子情報通信学会論文誌 Ｊ９３−Ｄ ２０１０年 Ｐ１−９
【非特許文献３】「オートマトン 言語理論 計算論 ＩＩ」Ｊ．ホップクロフト，Ｊ．ウルマン，Ｒ．モトワニ サイエンス社 ２００８年 Ｐ１４７−１５５
【発明の概要】
【発明が解決しようとする課題】
【００１２】
上記の通り、ＳＡＴの構造を活用して効率的に問題を判定する汎用性の高いＳＡＴ解法が存在しなかった。論理式の充足可能性を効率的に求めることのできるＨｏｒｎＣＮＦの形式に変換するプログラムが存在しなかった。ＳＡＴの難易度を効率的に評価するプログラムが存在しなかった。
【課題を解決するための手段】
【００１３】
上記問題を解決するため、本発明では、コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラムとした。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項それぞれの、その項のお互いに共通の変数が存在しかつ共通の変数の肯否が全て一致する（本特許ではこの部分を共通部と呼ぶ。また共通部にあるリテラルからなる項を共通項と呼ぶ）項同士について、それぞれの２つの項の組について、片方の項を第一成分として持ち、もう片方の項及びその項の共通部に含まれない部分（本特許では差分部と呼ぶ。また差分部にあるリテラルからなる項を差分項と呼ぶ）の肯否を入れ替えた項の集合を第二成分として持つ順序対。
順序対の第一成分として出現する項それぞれの、その項のお互いに共通の変数が存在するがその共通の変数のいずれかの肯否が異なる（本特許ではこの部分を相補部と呼ぶ。また相補部にあるリテラルからなる項を相補項と呼ぶ）項同士について、対象の項の相補部に入らない部分を全て合わせた項（本特許ではこの全ての差分部を集めた部分を浸出部と呼ぶ。また浸出部にあるリテラルからなる項を浸出項と呼ぶ）を第一成分として持ち、対象の項及び対象の項の差分部の肯否を入れ替えた項（ただしお互い共通部の肯否が一致するものは含まない）の集合を第二成分として持つ順序対。
空集合を第一成分として持ち、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対。
【００１４】
上記問題を解決するため、本発明では、コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラムとした。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、共通項を第一成分として持ち、共通部を持つ項のいずれか一つの項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。
順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び相補項の肯否を入れ替えた項（ただし対象の項の相補部と肯否が一致するものは含まない）全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。
空集合を第一成分として持ち、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対。
【００１５】
また上記プログラムにおいて、ＣＮＦの項を第一成分とし空集合を第二成分として持つ順序対は入力のＣＮＦから容易に構成可能なため、入力をそのまま使用する場合や、出力に含まない場合がある。
【００１６】
また上記プログラムにおいて、空集合を第一成分として持ち要素として現れた項それぞれについてその項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対は他の順序対から容易に構成可能なため、計算を行わずに出力に含めない場合がある。
【００１７】
また上記プログラムにおいて、共通部や相補部に対応する順序対において、共通項や相補項に対応する項を持つ場合と持たない場合が混在する場合がある。
【００１８】
なお集合や順序対の構成は通常プログラムで行われる方法を用いる。項そのものを配列やテーブルなどのレコードで構築する場合もあり、項のデータを別に用意してそのデータへの参照を配列やテーブルなどのレコードで構築する場合もあるが、これらに限らない。
【００１９】
また上記プログラムにおいて、集合の集合を出力する代わりに、下記の項を持つＨｏｒｎＣＮＦを出力するプログラムとすることがある。順序対に含まれる項に代えてＨｏｒｎＣＮＦの変数とする。順序対に代えて、順序対の第一成分をＨｏｒｎＣＮＦの変数の肯定リテラルとし、順序対の第二成分の要素をＨｏｒｎＣＮＦの変数の否定リテラルとして持つＨｏｒｎＣＮＦの項とする。この場合、第一成分が空集合の順序対には目的項が対応し、第二成分が空集合の順序対には事実項が対応する。第一成分も第二成分も空集合にならない順序対は規則項に対応する。
【００２０】
このような順序対を構成することで、ＣＮＦの持つ構造を扱いやすい形に再構成するため、ＣＮＦＳＡＴを計算やその難易度の評価を簡単にすることができる。
【００２１】
なお、ＨｏｒｎＣＮＦは、変数が順序対の項に、項が順序対に対応するため、下記でも暗黙的にその対応関係を用いる場合がある。
【００２２】
また上記プログラムにおいて、後の計算の容易化のため、同じ変数から構成される項を要素として持つ順序対の集合を用意する場合がある。同様に、同じリテラルから構成される順序対の集合を用意する場合がある。このようにすることで、同じ変数からなる項や同じリテラルからなる項がどの順序対に存在するかを見つけやすくし、計算を容易化する。
【００２３】
また上記プログラムにおいて、集合の集合を出力する代わりに、下記の有向グラフを出力する場合がある。
順序対の要素を構成するのに代えて、有向グラフの頂点を構成する。順序対の第一成分と第二成分を構成するのに代えて、第二成分の集合に含まれる項に対応する頂点から第一成分の項に対応する頂点への有向辺を構成する。この場合、空集合も頂点として存在する。
【００２４】
なお、有向グラフは、頂点が順序対の項に、辺が順序対に対応するため、下記でも暗黙的にその対応関係を用いる場合がある。
【００２５】
このグラフは充足性について半順序を持つため、空集合に繋がる有向辺の起点となる頂点（目的項に対応する）を考えた時に、その頂点を終点とする経路（事実項と、それによって確定される規則項に対応する）が全て空集合起点となる場合は充足不可となるため、比較的容易に充足可否を判定することができる。
【００２６】
また上記プログラムにおいて、集合の集合を出力する代わりに、下記の値を出力する場合がある。順序対の数。順序対に含まれる要素の合計。浸出項の変数の最大値。浸出項の数。空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。前述をランダムに選択した標本から算出した値。
【００２７】
また上記問題を解決するため、コンピュータを、ＣＮＦの項のうち、相補部を持つ項同士の組合せの数を出力するとした。
【００２８】
この結果、ＣＮＦＳＡＴを実際に計算せずに難易度を評価することができる。
【００２９】
また上記プログラムにおいて、データを出力する代わりに、ＣＮＦＳＡＴを計算してその充足可否や充足条件の計算結果をデータとして出力することもある。
【００３０】
また、上記プログラムにおいて、論理式を受け取った時はＣＮＦまたは３ＣＮＦに変換することとしたプログラムとすることもある。
【発明の効果】
【００３１】
本発明により、ＣＮＦの持つ構造を活用して、コンピュータで取り扱いやすいデータ形式、特にＨｏｒｎＣＮＦや半順序を持つ有向グラフの形に変形することが可能となった。またその結果を用いて効率的にＳＡＴをコンピュータで処理することが可能となった。さらに、ＳＡＴの難易度を効率的に評価することが可能となった。
【図面の簡単な説明】
【００３２】
【図１】本発明の実施形態の一例を示す構成図である。
【図２】本発明の実施形態の一例を示す構成図である。
【発明を実施するための形態】
【００３３】
以下に本発明の実施形態の一つについて、図面に基づき説明する。図１は本発明のプログラムの構成図である。
【００３４】
本プログラムは以下の構成となる。論理式を受け取りＣＮＦに変換する入力部１１１。入力部１１１から受け取ったＣＮＦを元に、各項の関係を表すデータに変換する変換部１１２。変換したデータを出力する出力部１１３。また、変換部が作成したデータを元に充足可否を判定するＳＡＴ判定部１２１、及びＳＡＴ判定部１２１の結果を出力する判定結果出力部１２２が存在することもある。また、変換部が作成したデータを元にＳＡＴの難易度を評価するＳＡＴ評価部１３１、及びＳＡＴ評価部１３１の結果を出力する評価結果出力部１３２が存在することもある。
【００３５】
入力部１１１の詳細を説明する。入力部１１１はメモリ、ストレージ、ＩＯ、他のプログラムなど、通常のコンピュータで使用される入出力部からの入力を受け取る。
【００３６】
受け取った入力が論理式の条件を満たしている場合は入力をＣＮＦに変換して変換部１１２に出力する。プログラムによっては正規化を一段進めて３ＣＮＦに変換する場合もある。論理式からＣＮＦや３ＣＮＦへの変換は通常用いられる方法を用いる（例えば非特許文献３参照）。また、変換部１１２に出力する際に、ＣＮＦや３ＣＮＦを作成するときに付加した変数を識別可能なように渡すことがある。例えば変数にＣＮＦに変換するときに付加した変数、あるいは３ＣＮＦに変換するときに付加した変数であることがわかるように、変数に識別子を付けたり、変数の一覧を別途データとして渡したりすることがある。ＣＮＦを作成するときに付加する変数は肯定リテラルと否定リテラルの数が同数になり、また３ＣＮＦを作成する時に付加する変数は肯定リテラルと否定リテラルがそれぞれ一つの項にしか出てこない。よって、このような特徴を、充足可能性を判定するときに活用することで判定を効率化することができる。
【００３７】
入力は論理式及び論理式の変数の満たす条件で構成される。論理式や論理式を表すバイナリ列など、通常用いられる論理式の省略形を表現したデータを受け取ることも可能とするが、この内容に制限されない。
【００３８】
また、入力が論理式の条件を満たしていない場合は入力を拒否する。拒否の方法は通常のプログラムで計算失敗として行われている動作を用いる。例えば判定結果出力部１２２がある場合は充足不可として判定結果出力部１２２に出力する場合や、単に入力を無視する場合などである。また通常のプログラムで行われている動作（特殊な値の出力、例外の発行）なども行うことがあるが、この内容に制限されない。
【００３９】
変換部１１２の詳細を説明する。変換部１１２は、入力部１１１からの出力としてＣＮＦを受け取ると、ＣＮＦの項を共通の変数を持つ集合に分類する。そして共通の変数を持つ集合のうち、同じ肯否を持つ組合せと異なる肯否を持つ組合せを作成し、それぞれについて順序対を作成する。
【００４０】
ここで、順序対を作成する代わりに有向グラフを作成する場合がある。有向グラフは順序対の作成と同様の手順にて作成することができる。
【００４１】
順序対（あるいは有向グラフ）の作成は、下記の手順にて行う。
【００４２】
まずはＣＮＦから、ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対を作成する。この項はＨｏｒｎＣＮＦの事実項に対応する項でもあり、空集合を条件として持つ（無条件に真となる必要のある）条件を意味する。
【００４３】
ただし、この事実項に対応する順序対はＣＮＦの各項から容易に作成することができるため、ＣＮＦの各項を順序対の第一成分に読み替えて使用する場合もある。また、出力にこの順序対を含まずＣＮＦを含む場合、あるいはまったく含まない場合がある。
【００４４】
次に、これまでに作成した順序対の第一成分に含まれる項（入力のＣＮＦの項も含む）について、お互いに共通の変数を含む組合せを計算し、その組合せに関係する順序対を計算する。この順序対はＨｏｒｎＣＮＦの規則項に相当する。
【００４５】
まだ計算を行っていない組合せがある場合、共通の変数の全ての肯否が同じ場合と、共通の変数のいずれかの肯否が異なる場合の、全ての組合せについて順序対の計算を行う。
【００４６】
まず、共通の変数の全ての肯否が同じ場合の詳細を述べる。この場合、共通項は必ず真偽が同じになるため、ある項で共通部が真となる場合は別の項でも真となり、ある項で共通部が偽となる場合は別の項でも偽となる。この条件をＨｏｒｎＣＮＦの規則項を意識して順序対で構成すると次のようになる。共通部を持つ項同士のうちある項を第一成分とし、別の項の差分部の肯否全ての場合を集めた集合を第二成分とする。
【００４７】
例えば、順序対の第一成分に
（Ｘ０Ｖ¬Ｘ２ＶＸ４）と（Ｘ０Ｖ¬Ｘ２ＶＸ６）
があった場合、ある項を（Ｘ０Ｖ¬Ｘ２ＶＸ４）、別の項を（Ｘ０Ｖ¬Ｘ２ＶＸ６）とすると、この時の順序対は
（（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０Ｖ¬Ｘ２Ｖ Ｘ６），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ６））
となる。
当然、ある項を（Ｘ０Ｖ¬Ｘ２ＶＸ６）、別の項を（Ｘ０Ｖ¬Ｘ２ＶＸ４）とした場合も考慮する必要があり、この時の順序対は
（（Ｘ０Ｖ¬Ｘ２Ｖ Ｘ６），（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ４））
となる。
【００４８】
次に、共通の変数のいずれかの肯否が異なる場合の詳細を述べる。この場合、相補項が同時に真となることは無いため、対象の項が全て真になる場合は浸出部のいずれかが真となる。この条件をＨｏｒｎＣＮＦの規則項を意識して順序対で構成すると次のようになる。浸出項を第一成分とし、対象の項及び対象の項の差分部の肯否を入れ替えた項（ただしお互い共通部の肯否が一致するものは含まない）の集合を第二成分とする。この順序対の計算は、お互いに相補部を持つ項の組合せ全ての場合について行う必要がある。
【００４９】
例えば、順序対の第一成分に
（Ｘ０Ｖ¬Ｘ２ＶＸ４）と（Ｘ０ＶＸ２ＶＸ６）
があった場合、この順序対（の一つの例）は
（（Ｘ４ＶＸ６），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（¬Ｘ０Ｖ Ｘ２ＶＸ４），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ６），
（ Ｘ０Ｖ Ｘ２ＶＸ６））
となる。
当然、上記順序対の（¬Ｘ０Ｖ Ｘ２ＶＸ４）及び（¬Ｘ０Ｖ¬Ｘ２ＶＸ６）は恣意的に選択した項であり、この項である必要はない。例えば
（（Ｘ４ＶＸ６），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（¬Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ４），
（ Ｘ０Ｖ Ｘ２ＶＸ６））
（（Ｘ４ＶＸ６），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（¬Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ６），
（ Ｘ０Ｖ Ｘ２ＶＸ６））
などとすることもできる。
【００５０】
また、３つ以上の項の関係も２つの項の関係と同様に計算する必要がある。例えば、
（Ｘ０Ｖ¬Ｘ２ＶＸ４）（Ｘ０ＶＸ２ＶＸ６）（¬Ｘ０ＶＸ２Ｖ¬Ｘ８）
の場合、この順序対（の一つの例）は
（（Ｘ４ＶＸ６Ｖ¬Ｘ８），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（ Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ Ｘ２ＶＸ８），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ８））
となる。
当然、この場合でも２つの項の関係をそれぞれ別に計算する必要がある。
【００５１】
また、上記において効率化のために共通項・相補項を用意してその順序対とすることもできる。例えば上記の共通部については
（（Ｘ０Ｖ¬Ｘ２），（Ｘ０Ｖ¬Ｘ２ＶＸ６），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ６））
（（Ｘ０Ｖ¬Ｘ２），（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ４））
とすることができ、上記の相補部については
（（Ｘ４ＶＸ６），（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０ＶＸ２ＶＸ６），
（¬Ｘ０ＶＸ２），（¬Ｘ０Ｖ¬Ｘ２））
３つの項の場合は
（（Ｘ４ＶＸ６Ｖ¬Ｘ８），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（ Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ Ｘ２ＶＸ８），
（¬Ｘ０Ｖ¬Ｘ２Ｖ））
とすることができる。
【００５２】
全ての第一成分の項の組合せについて順序対の計算を行った後に、次の手順で順序対を計算する。この順序対はＨｏｒｎＣＮＦの目的項に相当する
【００５３】
これまでに作成した順序対に含まれる項全てについて、その項に含まれるリテラルの肯否全ての組合せの項全てを集めた集合を第二成分とし、空集合を第一成分とする順序対とする。
【００５４】
例えば、（¬Ｘ０Ｖ¬Ｘ２Ｖ）という項が含まれる場合、この順序対は
（φ，
（Ｘ０ＶＸ２Ｖ），（¬Ｘ０ＶＸ２Ｖ），（Ｘ０Ｖ¬Ｘ２Ｖ），（¬Ｘ０Ｖ¬Ｘ２Ｖ））
となる。
【００５５】
ただし、この目的項に相当する順序対は規則項から容易に作成することができるため、計算しない場合がある。また、出力としてこの順序対を含まない場合がある。前述の事実項に対応する順序対も含まない場合は、規則項に対応する順序対しか出力しないことになる。
【００６６】
なお、順序対は、順序対を構成する項をそれぞれの変数に、第一成分の項をその対応する変数の肯定リテラルとし、第二成分の集合に含まれる項をそれぞれ対応する変数の否定リテラルとする項に変換することで、容易にＨｏｒｎＣＮＦの項に変換することができる。よって、変換部１１２は順序対を出力する代わりにＨｏｒｎＣＮＦを計算して出力することがある。
【００５７】
なお、順序対の計算と同様の手順にて有向グラフを作成することができるため、変換部１１２は順序対を計算する代わりに有向グラフを計算して出力することがある。
【００５８】
また、変換部１１２は後の計算が容易になるよう、順序対（あるいは有向グラフ）に付加的な情報を追加することがある。例えば、同じ変数で構成される項の関係は重要となるため、その項を含む順序対（あるいは頂点）の集合を別途出力することがある。同様に、同じリテラルで構成される項の関係は重要となるため、その項を含む順序対の集合を別途出力することがある（これは有向グラフの頂点と一致する）。
【００５９】
変換部１１２は、このようにして構成したデータを出力部１１３、ＳＡＴ判定部１２１、ＳＡＴ評価部１３１に出力する。
【００６０】
出力部１１３の詳細を説明する。出力部１１３は、変換部１１２からの入力を変換したデータを受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、データ作成の途中で生成したデータなどを含むことがある。他のプログラムはこのデータを活用してＳＡＴ計算やデータ解析などの処理を行う。また、出力部１１３の出力したデータには、ＳＡＴの潜在的な構造が顕在化された形で表現されているため、このデータを用いることでＳＡＴの構造の解析が容易となっている。そのため、ＳＡＴの難易度の評価を、実際に計算を始める前に見積もることができる。
【００６１】
ＳＡＴ判定部１２１の詳細を説明する。
【００６２】
ＳＡＴ判定部１２１は、変換部１１２からデータを受け取ると、データを活用してＨｏｒｎＣＮＦに読み替えて充足可能性を判定する。変換部１１２のデータは、それぞれの部分を読み替えることでＨｏｒｎＣＮＦとして捉えることができる。
【００６３】
また、変換部１１２から有向グラフを受け取った場合は、空集合に繋がる有向辺の起点となる頂点（目的項に対応する）を考えた時に、その頂点を終点とする経路（事実項と、それによって確定される規則項に対応する）が全て空集合起点となる場合は充足不可となるため、このことを確認することで充足可否を判定することもできる。
【００６４】
なお、ここで作成した順序対（ＨｏｒｎＣＮＦ、有向グラフ）は、順序対の第一成分の増殖性からもわかるように、ＣＮＦの構造によっては最悪指数規模の規模となり、その規模を小さいものに変換することが本質的にできない。そのため、計算によってはある程度の計算難易度の見積りを行い、必要に応じて計算を打ち切る、あるいはデータ処理の優先順位を付けることが重要となる。
【００６５】
例えば、後述のＳＡＴ評価部１３１によるＳＡＴ難易度によって、本特許による順序対の構築を行わず、乱択アルゴリズムによる解法に切り替えるなどである。
【００６６】
ＳＡＴ判定部１２１は、判定結果を判定結果出力部１２２に出力する。
【００６７】
判定結果出力部１２２の詳細を説明する。判定結果出力部１２２は、ＳＡＴ判定部１２１から判定結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部１１１や変換部１１２、ＳＡＴ判定部１２１から計算過程・結果のデータを受け取ることがある。
【００６８】
ＳＡＴ評価部１３１の詳細を説明する。
【００６９】
ＳＡＴ評価部１３１は、変換部１１２からデータを受け取ると、データの構造から充足可能性の判定難易度を評価する。評価を行った後、その結果を評価結果出力部１３２に出力する。
【００７０】
前述の通り、ＣＮＦをＨｏｒｎＣＮＦに変換する時のＨｏｒｎＣＮＦの規模は浸出項の構造によって大きく変化する。そこで、ＳＡＴ評価部１３１は変換部１１２から受け取ったデータの浸出項の構造を分析し、ＣＮＦの難易度を評価する。
【００７１】
この難易度の評価にはいくつか方法がある。具体的には次の通りである。項の数を難易度とする。順序対の数を難易度とする。浸出項の数を難易度とする。浸出項を第一成分とする順序対の数を難易度とする。浸出項の第一成分とする順序対の数を難易度とする。などである。あるいは浸出項の変数の数の最大値を難易度とする、などのこともある。あるいは空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。などのこともある。またはこれらの評価を重み付きで組合せることで全体の評価を行うこともある。
【００７２】
また、前述の評価を行う際に、全ての場合について計算を行うのではなく、ランダムに選択した標本から計算することもある。この場合、乱択アルゴリズムなどを活用することがある。
【００７３】
評価結果出力部１３２の詳細を説明する。評価結果出力部１３２は、ＳＡＴ評価部１３１から評価結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部１１１や変換部１１２、ＳＡＴ評価部１３１から計算過程・結果のデータを受け取ることがある。
【００７４】
以下に本発明の別の実施形態について、図面に基づき説明する。図２は本発明のプログラムの構成図である。
【００７５】
本プログラムは以下の構成となる。論理式を受け取りＣＮＦに変換する入力部２１１。入力部２１１から受け取ったＣＮＦを元に、ＣＮＦＳＡＴの難易度を計算する評価部２１２。評価した結果を出力する出力部２１３。
【００７６】
入力部２１１は、入力部１１１と同様の機能となる。入力を受け取り、評価部２１２にＣＮＦを出力する。
【００７７】
出力部２１３は、出力部１１１と同様の機能となる。評価部２１２からデータを受け取り、出力を行う。
【００７８】
評価部２１２の詳細を説明する。評価部２１２はＣＮＦを受け取ると、ＣＮＦに含まれる項全てについて、それぞれ相補部を含む項同士の組合せの数を求める。その組合せの数を出力部２１３に送る。
【００７９】
このような構成とすることで、簡易的にＣＮＦＳＡＴの難易度を評価することができる。前述の例よりも難易度判定の精度が落ちるが、前述の例よりもはるかに短い時間で難易度の判定を行うことができる。
【産業上の利用可能性】
【００８０】
ＳＡＴに帰着可能な問題全般について、ＣＮＦの持つ構造を効果的に活用して、効率的に充足可能性を判定することができるようになった。ＣＮＦＳＡＴを取り扱いの容易な順序対やＨｏｒｎＳＡＴ、有向グラフに変更することにより、計算を効率的に行えるようにした。問題の持つ潜在的な構造を顕在化することによって、その解析を容易に行うことができるようになった。解析によってＳＡＴの難易度の評価を、実際に計算を始める前に見積もることができるようになった。
【符号の説明】
【００８１】
１１１ 入力部
１１２ 変換部
１１３ 出力部
１２１ ＳＡＴ判定部
１２２ 判定結果出力部
１３１ ＳＡＴ評価部
１３２ 評価結果出力部
２１１ 入力部
２１２ 評価部
２１３ 出力部
【技術分野】
【０００１】
本発明は、コンピュータにて論理式を変換するプログラム、及び充足可能性問題を扱うプログラム、及び充足可能性問題の難易度を評価するプログラムに関する
【背景技術】
【０００２】
従来、コンピュータでは様々な問題が扱われており、また論理式や充足可能性問題、恒真式問題など論理に関する問題も様々なものが扱われている。
【０００３】
特にＳＡＴ（充足可能性問題）は、ＮＰ完全問題として非決定性チューリングマシンと等価であることが判明しており、またその応用範囲も広い。そのため、コンピュータで自動的に解決する様々なＳＡＴ解法（ＳＡＴソルバ）が研究・実用化されている。
【０００４】
ＳＡＴは条件により様々な種類が存在する。特にＣＮＦ（乗法標準形）で構成されたＣＮＦＳＡＴと、３ＣＮＦ（項のリテラルが３つまでに限定されたＣＮＦ）で構成された３ＳＡＴが重要である。ＳＡＴはＣＮＦＳＡＴや３ＳＡＴに変換可能であり（例えば非特許文献３参照）、また変換後のＣＮＦや３ＣＮＦは取り扱いが容易なため、ＳＡＴ解法でも始めにＳＡＴをＣＮＦＳＡＴや３ＳＡＴに変換する手法が用いられている。
【０００５】
また、特別なＣＮＦの一つとしてＨｏｒｎＣＮＦと２ＣＮＦがある。ＨｏｒｎＣＮＦは各項に０または１の肯定リテラルが存在するＣＮＦである。本出願では１つの肯定リテラルのみからなる項を事実項、肯定リテラルが１つのみで残りが否定リテラルとなる項を規則項、否定リテラルのみからなる項を目的項と呼ぶこととする。また、２ＣＮＦは項の変数が２つまでに限定されたＣＮＦである。本出願ではＨｏｒｎＣＮＦと同様に規則項、目的項を定める。また、ＨｏｒｎＣＮＦには存在しない肯定リテラルを２つ含む項を関連項と呼ぶこととする。なお、式に含まれる全ての変数の肯否を入れ替えることによってＨｏｒｎＣＮＦにすることのできる論理式も存在する。本質的にはＨｏｒｎＣＮＦと同じとなるため、以降ではそのような論理式もＨｏｒｎＣＮＦとして扱う。
【０００６】
ＨｏｒｎＣＮＦや２ＣＮＦはコンピュータで効率的に充足可能性の判定を行うことが可能（例えばＤＰＬＬアルゴリズム）だが、ＣＮＦからＨｏｒｎＣＮＦや２ＣＮＦに効率的に変換する方法は存在しない。
【０００７】
またＳＡＴは本質的にコンピュータで計算するのが困難な問題であり、判定するのに問題の規模の指数倍の時間が必要になることがある。また、確率的な乱択アルゴリズムで充足可能なことを求める確率的ＳＡＴ解法もあるが、このようなＳＡＴ解法でも充足不可を判定するのは困難である。そのため、全ての可能性を判定し充足不可を明確化する完全ＳＡＴ解法の効率化が重要となる（例えば特許文献１参照）。またＳＡＴは問題毎に難易度が大幅に異なるため、難易度を評価することも重要となる。
【０００８】
しかし、従来の完全ＳＡＴ解法や確率的ＳＡＴ解法は、充足可能である条件から式を簡約するＤＰＬＬアルゴリズム（例えば非特許文献１参照）や、可能性のある真理値割当を実際に式に適用する手法などが主であり、問題の構造を活用して効率化する手法は少なかった。また、式の構造そのものに着目してＳＡＴ解法を効率化する手法はあったが（例えば非特許文献２参照）、特定の条件を満たす必要のあるものがほとんどであり応用範囲が狭かった。また、充足解の計算時間を調整することで、充足解を計算する時の負担を軽減する技術（例えば特許文献２参照）があるが、実際に計算を行う必要があるため、必ずしも効率化になるとは限らなかった。そして、ＳＡＴの難易度を効率的に評価する方法も無かったため、計算時間などを効率的に評価する方法も存在しなかった。
【０００９】
なお、ＳＡＴを効率良く扱うために、ＳＡＴで与えられた式をＳＡＴ解法のために効率の良い形に変更することも重要となるが、そのようなプログラムにおいて、論理式をＨｏｒｎＣＮＦに効率良く変換するプログラムは存在しなかった。
【先行技術文献】
【特許文献】
【００１０】
【特許文献１】特開２００４−３５５０３８
【特許文献２】特開２００５−２９３５７５
【００１１】
【非特許文献１】″Ａ Ｃｏｍｐｕｔｉｎｇ Ｐｒｏｃｅｄｕｒｅ ｆｏｒ Ｑｕａｎｔｉｆｉｃａｔｉｏｎ Ｔｈｅｏｒｙ″Ｍａｒｔｉｎ Ｄａｖｉｓ、Ｈｉｌａｒｙ Ｐｕｔｎａｍ Ｊｏｕｒｎａｌ ｏｆ ｔｈｅ ＡＣＭ ７ １９６０年 Ｐ２０１−２１５
【非特許文献２】「基本対称関数に基づく節をもつＣＮＦ論理式の充足可能性判定」馬野洋平，酒井正彦，西田直樹，坂部俊樹，草刈圭一朗 電子情報通信学会論文誌 Ｊ９３−Ｄ ２０１０年 Ｐ１−９
【非特許文献３】「オートマトン 言語理論 計算論 ＩＩ」Ｊ．ホップクロフト，Ｊ．ウルマン，Ｒ．モトワニ サイエンス社 ２００８年 Ｐ１４７−１５５
【発明の概要】
【発明が解決しようとする課題】
【００１２】
上記の通り、ＳＡＴの構造を活用して効率的に問題を判定する汎用性の高いＳＡＴ解法が存在しなかった。論理式の充足可能性を効率的に求めることのできるＨｏｒｎＣＮＦの形式に変換するプログラムが存在しなかった。ＳＡＴの難易度を効率的に評価するプログラムが存在しなかった。
【課題を解決するための手段】
【００１３】
上記問題を解決するため、本発明では、コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラムとした。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項それぞれの、その項のお互いに共通の変数が存在しかつ共通の変数の肯否が全て一致する（本特許ではこの部分を共通部と呼ぶ。また共通部にあるリテラルからなる項を共通項と呼ぶ）項同士について、それぞれの２つの項の組について、片方の項を第一成分として持ち、もう片方の項及びその項の共通部に含まれない部分（本特許では差分部と呼ぶ。また差分部にあるリテラルからなる項を差分項と呼ぶ）の肯否を入れ替えた項の集合を第二成分として持つ順序対。
順序対の第一成分として出現する項それぞれの、その項のお互いに共通の変数が存在するがその共通の変数のいずれかの肯否が異なる（本特許ではこの部分を相補部と呼ぶ。また相補部にあるリテラルからなる項を相補項と呼ぶ）項同士について、対象の項の相補部に入らない部分を全て合わせた項（本特許ではこの全ての差分部を集めた部分を浸出部と呼ぶ。また浸出部にあるリテラルからなる項を浸出項と呼ぶ）を第一成分として持ち、対象の項及び対象の項の差分部の肯否を入れ替えた項（ただしお互い共通部の肯否が一致するものは含まない）の集合を第二成分として持つ順序対。
空集合を第一成分として持ち、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対。
【００１４】
上記問題を解決するため、本発明では、コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラムとした。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、共通項を第一成分として持ち、共通部を持つ項のいずれか一つの項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。
順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び相補項の肯否を入れ替えた項（ただし対象の項の相補部と肯否が一致するものは含まない）全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。
空集合を第一成分として持ち、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対。
【００１５】
また上記プログラムにおいて、ＣＮＦの項を第一成分とし空集合を第二成分として持つ順序対は入力のＣＮＦから容易に構成可能なため、入力をそのまま使用する場合や、出力に含まない場合がある。
【００１６】
また上記プログラムにおいて、空集合を第一成分として持ち要素として現れた項それぞれについてその項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対は他の順序対から容易に構成可能なため、計算を行わずに出力に含めない場合がある。
【００１７】
また上記プログラムにおいて、共通部や相補部に対応する順序対において、共通項や相補項に対応する項を持つ場合と持たない場合が混在する場合がある。
【００１８】
なお集合や順序対の構成は通常プログラムで行われる方法を用いる。項そのものを配列やテーブルなどのレコードで構築する場合もあり、項のデータを別に用意してそのデータへの参照を配列やテーブルなどのレコードで構築する場合もあるが、これらに限らない。
【００１９】
また上記プログラムにおいて、集合の集合を出力する代わりに、下記の項を持つＨｏｒｎＣＮＦを出力するプログラムとすることがある。順序対に含まれる項に代えてＨｏｒｎＣＮＦの変数とする。順序対に代えて、順序対の第一成分をＨｏｒｎＣＮＦの変数の肯定リテラルとし、順序対の第二成分の要素をＨｏｒｎＣＮＦの変数の否定リテラルとして持つＨｏｒｎＣＮＦの項とする。この場合、第一成分が空集合の順序対には目的項が対応し、第二成分が空集合の順序対には事実項が対応する。第一成分も第二成分も空集合にならない順序対は規則項に対応する。
【００２０】
このような順序対を構成することで、ＣＮＦの持つ構造を扱いやすい形に再構成するため、ＣＮＦＳＡＴを計算やその難易度の評価を簡単にすることができる。
【００２１】
なお、ＨｏｒｎＣＮＦは、変数が順序対の項に、項が順序対に対応するため、下記でも暗黙的にその対応関係を用いる場合がある。
【００２２】
また上記プログラムにおいて、後の計算の容易化のため、同じ変数から構成される項を要素として持つ順序対の集合を用意する場合がある。同様に、同じリテラルから構成される順序対の集合を用意する場合がある。このようにすることで、同じ変数からなる項や同じリテラルからなる項がどの順序対に存在するかを見つけやすくし、計算を容易化する。
【００２３】
また上記プログラムにおいて、集合の集合を出力する代わりに、下記の有向グラフを出力する場合がある。
順序対の要素を構成するのに代えて、有向グラフの頂点を構成する。順序対の第一成分と第二成分を構成するのに代えて、第二成分の集合に含まれる項に対応する頂点から第一成分の項に対応する頂点への有向辺を構成する。この場合、空集合も頂点として存在する。
【００２４】
なお、有向グラフは、頂点が順序対の項に、辺が順序対に対応するため、下記でも暗黙的にその対応関係を用いる場合がある。
【００２５】
このグラフは充足性について半順序を持つため、空集合に繋がる有向辺の起点となる頂点（目的項に対応する）を考えた時に、その頂点を終点とする経路（事実項と、それによって確定される規則項に対応する）が全て空集合起点となる場合は充足不可となるため、比較的容易に充足可否を判定することができる。
【００２６】
また上記プログラムにおいて、集合の集合を出力する代わりに、下記の値を出力する場合がある。順序対の数。順序対に含まれる要素の合計。浸出項の変数の最大値。浸出項の数。空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。前述をランダムに選択した標本から算出した値。
【００２７】
また上記問題を解決するため、コンピュータを、ＣＮＦの項のうち、相補部を持つ項同士の組合せの数を出力するとした。
【００２８】
この結果、ＣＮＦＳＡＴを実際に計算せずに難易度を評価することができる。
【００２９】
また上記プログラムにおいて、データを出力する代わりに、ＣＮＦＳＡＴを計算してその充足可否や充足条件の計算結果をデータとして出力することもある。
【００３０】
また、上記プログラムにおいて、論理式を受け取った時はＣＮＦまたは３ＣＮＦに変換することとしたプログラムとすることもある。
【発明の効果】
【００３１】
本発明により、ＣＮＦの持つ構造を活用して、コンピュータで取り扱いやすいデータ形式、特にＨｏｒｎＣＮＦや半順序を持つ有向グラフの形に変形することが可能となった。またその結果を用いて効率的にＳＡＴをコンピュータで処理することが可能となった。さらに、ＳＡＴの難易度を効率的に評価することが可能となった。
【図面の簡単な説明】
【００３２】
【図１】本発明の実施形態の一例を示す構成図である。
【図２】本発明の実施形態の一例を示す構成図である。
【発明を実施するための形態】
【００３３】
以下に本発明の実施形態の一つについて、図面に基づき説明する。図１は本発明のプログラムの構成図である。
【００３４】
本プログラムは以下の構成となる。論理式を受け取りＣＮＦに変換する入力部１１１。入力部１１１から受け取ったＣＮＦを元に、各項の関係を表すデータに変換する変換部１１２。変換したデータを出力する出力部１１３。また、変換部が作成したデータを元に充足可否を判定するＳＡＴ判定部１２１、及びＳＡＴ判定部１２１の結果を出力する判定結果出力部１２２が存在することもある。また、変換部が作成したデータを元にＳＡＴの難易度を評価するＳＡＴ評価部１３１、及びＳＡＴ評価部１３１の結果を出力する評価結果出力部１３２が存在することもある。
【００３５】
入力部１１１の詳細を説明する。入力部１１１はメモリ、ストレージ、ＩＯ、他のプログラムなど、通常のコンピュータで使用される入出力部からの入力を受け取る。
【００３６】
受け取った入力が論理式の条件を満たしている場合は入力をＣＮＦに変換して変換部１１２に出力する。プログラムによっては正規化を一段進めて３ＣＮＦに変換する場合もある。論理式からＣＮＦや３ＣＮＦへの変換は通常用いられる方法を用いる（例えば非特許文献３参照）。また、変換部１１２に出力する際に、ＣＮＦや３ＣＮＦを作成するときに付加した変数を識別可能なように渡すことがある。例えば変数にＣＮＦに変換するときに付加した変数、あるいは３ＣＮＦに変換するときに付加した変数であることがわかるように、変数に識別子を付けたり、変数の一覧を別途データとして渡したりすることがある。ＣＮＦを作成するときに付加する変数は肯定リテラルと否定リテラルの数が同数になり、また３ＣＮＦを作成する時に付加する変数は肯定リテラルと否定リテラルがそれぞれ一つの項にしか出てこない。よって、このような特徴を、充足可能性を判定するときに活用することで判定を効率化することができる。
【００３７】
入力は論理式及び論理式の変数の満たす条件で構成される。論理式や論理式を表すバイナリ列など、通常用いられる論理式の省略形を表現したデータを受け取ることも可能とするが、この内容に制限されない。
【００３８】
また、入力が論理式の条件を満たしていない場合は入力を拒否する。拒否の方法は通常のプログラムで計算失敗として行われている動作を用いる。例えば判定結果出力部１２２がある場合は充足不可として判定結果出力部１２２に出力する場合や、単に入力を無視する場合などである。また通常のプログラムで行われている動作（特殊な値の出力、例外の発行）なども行うことがあるが、この内容に制限されない。
【００３９】
変換部１１２の詳細を説明する。変換部１１２は、入力部１１１からの出力としてＣＮＦを受け取ると、ＣＮＦの項を共通の変数を持つ集合に分類する。そして共通の変数を持つ集合のうち、同じ肯否を持つ組合せと異なる肯否を持つ組合せを作成し、それぞれについて順序対を作成する。
【００４０】
ここで、順序対を作成する代わりに有向グラフを作成する場合がある。有向グラフは順序対の作成と同様の手順にて作成することができる。
【００４１】
順序対（あるいは有向グラフ）の作成は、下記の手順にて行う。
【００４２】
まずはＣＮＦから、ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対を作成する。この項はＨｏｒｎＣＮＦの事実項に対応する項でもあり、空集合を条件として持つ（無条件に真となる必要のある）条件を意味する。
【００４３】
ただし、この事実項に対応する順序対はＣＮＦの各項から容易に作成することができるため、ＣＮＦの各項を順序対の第一成分に読み替えて使用する場合もある。また、出力にこの順序対を含まずＣＮＦを含む場合、あるいはまったく含まない場合がある。
【００４４】
次に、これまでに作成した順序対の第一成分に含まれる項（入力のＣＮＦの項も含む）について、お互いに共通の変数を含む組合せを計算し、その組合せに関係する順序対を計算する。この順序対はＨｏｒｎＣＮＦの規則項に相当する。
【００４５】
まだ計算を行っていない組合せがある場合、共通の変数の全ての肯否が同じ場合と、共通の変数のいずれかの肯否が異なる場合の、全ての組合せについて順序対の計算を行う。
【００４６】
まず、共通の変数の全ての肯否が同じ場合の詳細を述べる。この場合、共通項は必ず真偽が同じになるため、ある項で共通部が真となる場合は別の項でも真となり、ある項で共通部が偽となる場合は別の項でも偽となる。この条件をＨｏｒｎＣＮＦの規則項を意識して順序対で構成すると次のようになる。共通部を持つ項同士のうちある項を第一成分とし、別の項の差分部の肯否全ての場合を集めた集合を第二成分とする。
【００４７】
例えば、順序対の第一成分に
（Ｘ０Ｖ¬Ｘ２ＶＸ４）と（Ｘ０Ｖ¬Ｘ２ＶＸ６）
があった場合、ある項を（Ｘ０Ｖ¬Ｘ２ＶＸ４）、別の項を（Ｘ０Ｖ¬Ｘ２ＶＸ６）とすると、この時の順序対は
（（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０Ｖ¬Ｘ２Ｖ Ｘ６），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ６））
となる。
当然、ある項を（Ｘ０Ｖ¬Ｘ２ＶＸ６）、別の項を（Ｘ０Ｖ¬Ｘ２ＶＸ４）とした場合も考慮する必要があり、この時の順序対は
（（Ｘ０Ｖ¬Ｘ２Ｖ Ｘ６），（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ４））
となる。
【００４８】
次に、共通の変数のいずれかの肯否が異なる場合の詳細を述べる。この場合、相補項が同時に真となることは無いため、対象の項が全て真になる場合は浸出部のいずれかが真となる。この条件をＨｏｒｎＣＮＦの規則項を意識して順序対で構成すると次のようになる。浸出項を第一成分とし、対象の項及び対象の項の差分部の肯否を入れ替えた項（ただしお互い共通部の肯否が一致するものは含まない）の集合を第二成分とする。この順序対の計算は、お互いに相補部を持つ項の組合せ全ての場合について行う必要がある。
【００４９】
例えば、順序対の第一成分に
（Ｘ０Ｖ¬Ｘ２ＶＸ４）と（Ｘ０ＶＸ２ＶＸ６）
があった場合、この順序対（の一つの例）は
（（Ｘ４ＶＸ６），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（¬Ｘ０Ｖ Ｘ２ＶＸ４），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ６），
（ Ｘ０Ｖ Ｘ２ＶＸ６））
となる。
当然、上記順序対の（¬Ｘ０Ｖ Ｘ２ＶＸ４）及び（¬Ｘ０Ｖ¬Ｘ２ＶＸ６）は恣意的に選択した項であり、この項である必要はない。例えば
（（Ｘ４ＶＸ６），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（¬Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ４），
（ Ｘ０Ｖ Ｘ２ＶＸ６））
（（Ｘ４ＶＸ６），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（¬Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ６），
（ Ｘ０Ｖ Ｘ２ＶＸ６））
などとすることもできる。
【００５０】
また、３つ以上の項の関係も２つの項の関係と同様に計算する必要がある。例えば、
（Ｘ０Ｖ¬Ｘ２ＶＸ４）（Ｘ０ＶＸ２ＶＸ６）（¬Ｘ０ＶＸ２Ｖ¬Ｘ８）
の場合、この順序対（の一つの例）は
（（Ｘ４ＶＸ６Ｖ¬Ｘ８），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（ Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ Ｘ２ＶＸ８），
（¬Ｘ０Ｖ¬Ｘ２ＶＸ８））
となる。
当然、この場合でも２つの項の関係をそれぞれ別に計算する必要がある。
【００５１】
また、上記において効率化のために共通項・相補項を用意してその順序対とすることもできる。例えば上記の共通部については
（（Ｘ０Ｖ¬Ｘ２），（Ｘ０Ｖ¬Ｘ２ＶＸ６），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ６））
（（Ｘ０Ｖ¬Ｘ２），（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０Ｖ¬Ｘ２Ｖ¬Ｘ４））
とすることができ、上記の相補部については
（（Ｘ４ＶＸ６），（Ｘ０Ｖ¬Ｘ２ＶＸ４），（Ｘ０ＶＸ２ＶＸ６），
（¬Ｘ０ＶＸ２），（¬Ｘ０Ｖ¬Ｘ２））
３つの項の場合は
（（Ｘ４ＶＸ６Ｖ¬Ｘ８），
（ Ｘ０Ｖ¬Ｘ２ＶＸ４），
（ Ｘ０Ｖ Ｘ２ＶＸ６），
（¬Ｘ０Ｖ Ｘ２ＶＸ８），
（¬Ｘ０Ｖ¬Ｘ２Ｖ））
とすることができる。
【００５２】
全ての第一成分の項の組合せについて順序対の計算を行った後に、次の手順で順序対を計算する。この順序対はＨｏｒｎＣＮＦの目的項に相当する
【００５３】
これまでに作成した順序対に含まれる項全てについて、その項に含まれるリテラルの肯否全ての組合せの項全てを集めた集合を第二成分とし、空集合を第一成分とする順序対とする。
【００５４】
例えば、（¬Ｘ０Ｖ¬Ｘ２Ｖ）という項が含まれる場合、この順序対は
（φ，
（Ｘ０ＶＸ２Ｖ），（¬Ｘ０ＶＸ２Ｖ），（Ｘ０Ｖ¬Ｘ２Ｖ），（¬Ｘ０Ｖ¬Ｘ２Ｖ））
となる。
【００５５】
ただし、この目的項に相当する順序対は規則項から容易に作成することができるため、計算しない場合がある。また、出力としてこの順序対を含まない場合がある。前述の事実項に対応する順序対も含まない場合は、規則項に対応する順序対しか出力しないことになる。
【００６６】
なお、順序対は、順序対を構成する項をそれぞれの変数に、第一成分の項をその対応する変数の肯定リテラルとし、第二成分の集合に含まれる項をそれぞれ対応する変数の否定リテラルとする項に変換することで、容易にＨｏｒｎＣＮＦの項に変換することができる。よって、変換部１１２は順序対を出力する代わりにＨｏｒｎＣＮＦを計算して出力することがある。
【００５７】
なお、順序対の計算と同様の手順にて有向グラフを作成することができるため、変換部１１２は順序対を計算する代わりに有向グラフを計算して出力することがある。
【００５８】
また、変換部１１２は後の計算が容易になるよう、順序対（あるいは有向グラフ）に付加的な情報を追加することがある。例えば、同じ変数で構成される項の関係は重要となるため、その項を含む順序対（あるいは頂点）の集合を別途出力することがある。同様に、同じリテラルで構成される項の関係は重要となるため、その項を含む順序対の集合を別途出力することがある（これは有向グラフの頂点と一致する）。
【００５９】
変換部１１２は、このようにして構成したデータを出力部１１３、ＳＡＴ判定部１２１、ＳＡＴ評価部１３１に出力する。
【００６０】
出力部１１３の詳細を説明する。出力部１１３は、変換部１１２からの入力を変換したデータを受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、データ作成の途中で生成したデータなどを含むことがある。他のプログラムはこのデータを活用してＳＡＴ計算やデータ解析などの処理を行う。また、出力部１１３の出力したデータには、ＳＡＴの潜在的な構造が顕在化された形で表現されているため、このデータを用いることでＳＡＴの構造の解析が容易となっている。そのため、ＳＡＴの難易度の評価を、実際に計算を始める前に見積もることができる。
【００６１】
ＳＡＴ判定部１２１の詳細を説明する。
【００６２】
ＳＡＴ判定部１２１は、変換部１１２からデータを受け取ると、データを活用してＨｏｒｎＣＮＦに読み替えて充足可能性を判定する。変換部１１２のデータは、それぞれの部分を読み替えることでＨｏｒｎＣＮＦとして捉えることができる。
【００６３】
また、変換部１１２から有向グラフを受け取った場合は、空集合に繋がる有向辺の起点となる頂点（目的項に対応する）を考えた時に、その頂点を終点とする経路（事実項と、それによって確定される規則項に対応する）が全て空集合起点となる場合は充足不可となるため、このことを確認することで充足可否を判定することもできる。
【００６４】
なお、ここで作成した順序対（ＨｏｒｎＣＮＦ、有向グラフ）は、順序対の第一成分の増殖性からもわかるように、ＣＮＦの構造によっては最悪指数規模の規模となり、その規模を小さいものに変換することが本質的にできない。そのため、計算によってはある程度の計算難易度の見積りを行い、必要に応じて計算を打ち切る、あるいはデータ処理の優先順位を付けることが重要となる。
【００６５】
例えば、後述のＳＡＴ評価部１３１によるＳＡＴ難易度によって、本特許による順序対の構築を行わず、乱択アルゴリズムによる解法に切り替えるなどである。
【００６６】
ＳＡＴ判定部１２１は、判定結果を判定結果出力部１２２に出力する。
【００６７】
判定結果出力部１２２の詳細を説明する。判定結果出力部１２２は、ＳＡＴ判定部１２１から判定結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部１１１や変換部１１２、ＳＡＴ判定部１２１から計算過程・結果のデータを受け取ることがある。
【００６８】
ＳＡＴ評価部１３１の詳細を説明する。
【００６９】
ＳＡＴ評価部１３１は、変換部１１２からデータを受け取ると、データの構造から充足可能性の判定難易度を評価する。評価を行った後、その結果を評価結果出力部１３２に出力する。
【００７０】
前述の通り、ＣＮＦをＨｏｒｎＣＮＦに変換する時のＨｏｒｎＣＮＦの規模は浸出項の構造によって大きく変化する。そこで、ＳＡＴ評価部１３１は変換部１１２から受け取ったデータの浸出項の構造を分析し、ＣＮＦの難易度を評価する。
【００７１】
この難易度の評価にはいくつか方法がある。具体的には次の通りである。項の数を難易度とする。順序対の数を難易度とする。浸出項の数を難易度とする。浸出項を第一成分とする順序対の数を難易度とする。浸出項の第一成分とする順序対の数を難易度とする。などである。あるいは浸出項の変数の数の最大値を難易度とする、などのこともある。あるいは空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。などのこともある。またはこれらの評価を重み付きで組合せることで全体の評価を行うこともある。
【００７２】
また、前述の評価を行う際に、全ての場合について計算を行うのではなく、ランダムに選択した標本から計算することもある。この場合、乱択アルゴリズムなどを活用することがある。
【００７３】
評価結果出力部１３２の詳細を説明する。評価結果出力部１３２は、ＳＡＴ評価部１３１から評価結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部１１１や変換部１１２、ＳＡＴ評価部１３１から計算過程・結果のデータを受け取ることがある。
【００７４】
以下に本発明の別の実施形態について、図面に基づき説明する。図２は本発明のプログラムの構成図である。
【００７５】
本プログラムは以下の構成となる。論理式を受け取りＣＮＦに変換する入力部２１１。入力部２１１から受け取ったＣＮＦを元に、ＣＮＦＳＡＴの難易度を計算する評価部２１２。評価した結果を出力する出力部２１３。
【００７６】
入力部２１１は、入力部１１１と同様の機能となる。入力を受け取り、評価部２１２にＣＮＦを出力する。
【００７７】
出力部２１３は、出力部１１１と同様の機能となる。評価部２１２からデータを受け取り、出力を行う。
【００７８】
評価部２１２の詳細を説明する。評価部２１２はＣＮＦを受け取ると、ＣＮＦに含まれる項全てについて、それぞれ相補部を含む項同士の組合せの数を求める。その組合せの数を出力部２１３に送る。
【００７９】
このような構成とすることで、簡易的にＣＮＦＳＡＴの難易度を評価することができる。前述の例よりも難易度判定の精度が落ちるが、前述の例よりもはるかに短い時間で難易度の判定を行うことができる。
【産業上の利用可能性】
【００８０】
ＳＡＴに帰着可能な問題全般について、ＣＮＦの持つ構造を効果的に活用して、効率的に充足可能性を判定することができるようになった。ＣＮＦＳＡＴを取り扱いの容易な順序対やＨｏｒｎＳＡＴ、有向グラフに変更することにより、計算を効率的に行えるようにした。問題の持つ潜在的な構造を顕在化することによって、その解析を容易に行うことができるようになった。解析によってＳＡＴの難易度の評価を、実際に計算を始める前に見積もることができるようになった。
【符号の説明】
【００８１】
１１１ 入力部
１１２ 変換部
１１３ 出力部
１２１ ＳＡＴ判定部
１２２ 判定結果出力部
１３１ ＳＡＴ評価部
１３２ 評価結果出力部
２１１ 入力部
２１２ 評価部
２１３ 出力部
【特許請求の範囲】
【請求項１】
コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラム。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、それぞれの２つの項の組について、片方の項を第一成分として持ち、もう片方の項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。
順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び対象の項の差分部の肯否を入れ替えた項（ただしお互い相補部（共通部）の肯否が一致するものは含まない）全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。
【請求項２】
コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラム。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、共通項を第一成分として持ち、共通部を持つ項のいずれか一つの項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。
順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び相補項の肯否を入れ替えた項（ただし対象の項の相補部と肯否が一致するものは含まない）全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。
【請求項３】
請求項１、２において、ＣＮＦの項を第一成分とし空集合を第二成分として持つ順序対を計算する代わりに、ＣＮＦの項をそのまま順序対の代用として使用して計算を行うプログラム。
【請求項４】
請求項１、２、３において、空集合を第一成分とし、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対を計算するプログラム。
【請求項５】
請求項１、２、３、４において、集合の集合を出力する代わりに、下記の項を持つＨｏｒｎＣＮＦを出力するプログラム。
順序対に含まれる項に代えてＨｏｒｎＣＮＦの変数とする。順序対に代えて、順序対の第一成分をＨｏｒｎＣＮＦの変数の肯定リテラルとし、順序対の第二成分の要素をＨｏｒｎＣＮＦの変数の否定リテラルとして持つＨｏｒｎＣＮＦの項とする。
【請求項６】
請求項１、２、３、４において、集合の集合を出力する代わりに、下記の有向グラフを出力するプログラム。
順序対の要素を構成するのに代えて、有向グラフの頂点を構成する。順序対を構成するのに代えて、第二成分の集合に含まれる項に対応する頂点から第一成分の項に対応する頂点への有向辺を構成する。
【請求項７】
請求項１、２、３、４において、集合の集合を出力する代わりに、下記の値を出力するプログラム。順序対の数。順序対に含まれる要素の合計。浸出項の変数の最大値。浸出項の数。空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。前述をランダムに選択した標本から算出した値。
【請求項８】
コンピュータを、入力としてＣＮＦを受け取り、出力として下記の値を出力するプログラム。ＣＮＦの項のうち、相補部を持つ項同士の組合せの数。
【請求項９】
請求項１、２、３、４、５、６において、データを出力する代わりに、ＣＮＦＳＡＴの計算結果を出力するプログラム。
【請求項１】
コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラム。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、それぞれの２つの項の組について、片方の項を第一成分として持ち、もう片方の項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。
順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び対象の項の差分部の肯否を入れ替えた項（ただしお互い相補部（共通部）の肯否が一致するものは含まない）全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。
【請求項２】
コンピュータを、入力としてＣＮＦを受け取り、出力として下記の集合の集合を出力するプログラム。
ＣＮＦの項を第一成分とし、空集合を第二成分として持つ順序対。
順序対の第一成分として出現する項のうちお互いに共通部を持つ項同士について、共通項を第一成分として持ち、共通部を持つ項のいずれか一つの項及びその項の差分部の肯否を入れ替えた項全ての集合を第二成分として持つ順序対。そして共通部を持つ項全ての項についても同様に作成した順序対。
順序対の第一成分として出現する項のうちお互いに相補部を持つ項同士について、その項の浸出項を第一成分として持ち、対象の項及び相補項の肯否を入れ替えた項（ただし対象の項の相補部と肯否が一致するものは含まない）全ての集合を第二成分として持つ順序対。そして異なる浸出部となる項同士の全ての組合せについても同様に作成した順序対。
【請求項３】
請求項１、２において、ＣＮＦの項を第一成分とし空集合を第二成分として持つ順序対を計算する代わりに、ＣＮＦの項をそのまま順序対の代用として使用して計算を行うプログラム。
【請求項４】
請求項１、２、３において、空集合を第一成分とし、要素として現れた項それぞれについて、その項及びその項の肯否を入れ替えた項の集合を第二成分として持つ順序対を計算するプログラム。
【請求項５】
請求項１、２、３、４において、集合の集合を出力する代わりに、下記の項を持つＨｏｒｎＣＮＦを出力するプログラム。
順序対に含まれる項に代えてＨｏｒｎＣＮＦの変数とする。順序対に代えて、順序対の第一成分をＨｏｒｎＣＮＦの変数の肯定リテラルとし、順序対の第二成分の要素をＨｏｒｎＣＮＦの変数の否定リテラルとして持つＨｏｒｎＣＮＦの項とする。
【請求項６】
請求項１、２、３、４において、集合の集合を出力する代わりに、下記の有向グラフを出力するプログラム。
順序対の要素を構成するのに代えて、有向グラフの頂点を構成する。順序対を構成するのに代えて、第二成分の集合に含まれる項に対応する頂点から第一成分の項に対応する頂点への有向辺を構成する。
【請求項７】
請求項１、２、３、４において、集合の集合を出力する代わりに、下記の値を出力するプログラム。順序対の数。順序対に含まれる要素の合計。浸出項の変数の最大値。浸出項の数。空集合から空集合に到達する経路の最短距離、空集合から空集合に到達する経路の最長距離。空集合から空集合に到達する経路の本数。前述をランダムに選択した標本から算出した値。
【請求項８】
コンピュータを、入力としてＣＮＦを受け取り、出力として下記の値を出力するプログラム。ＣＮＦの項のうち、相補部を持つ項同士の組合せの数。
【請求項９】
請求項１、２、３、４、５、６において、データを出力する代わりに、ＣＮＦＳＡＴの計算結果を出力するプログラム。
【図１】
【図２】
【図２】
【公開番号】特開２０１２−１４１９４０（Ｐ２０１２−１４１９４０Ａ）
【公開日】平成２４年７月２６日（２０１２．７．２６）
【国際特許分類】
【出願番号】特願２０１１−１０２５７（Ｐ２０１１−１０２５７）
【出願日】平成２３年１月１日（２０１１．１．１）
【出願人】（５９８１０８０７６）
【Ｆターム（参考）】
【公開日】平成２４年７月２６日（２０１２．７．２６）
【国際特許分類】
【出願日】平成２３年１月１日（２０１１．１．１）
【出願人】（５９８１０８０７６）
【Ｆターム（参考）】
[ Back to top ]