(57)【要約】【課題】充足可能性問題は、その対象となる式の構造により難易度が変わるが、ＳＡＴの式の対称性を活用して効率化する汎用性の高いＳＡＴ解法が存在しなかった。また、ＣＮＦをＨｏｒｎＣＮＦに変換するプログラムが存在しなかった。【解決手段】ＣＮＦの持つ変数の対称性とリテラルの対称性を活用してＳＡＴを整理し、与えられた式をＨｏｒｎＣＮＦ相当に変換することとした。また、そのＨｏｒｎＣＮＦ相当に変換したＳＡＴを使用することで効率的に問題を解くこととした。【選択図】図１
2012003733.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを、ＳＡＴを受け取りＣＮＦＳＡＴに変換する入力部、入力部からＣＮＦＳＡＴを受け取り、ＣＮＦＳＡＴを構成するＣＮＦの各項の変数の組合せによって定まる変数組を構築し、各項の構成変数とリテラル構成によって定まるリテラル組を変数組と関連付けて構築し、共通の変数を持つ変数組同士を直接または間接に関連付けて構築したデータを出力する変換部、変換部が構築したデータを出力する出力部、として機能させるためのプログラム
【請求項２】
請求項１において、出力部を、変換部が構築したデータにおいて変数組を目的項、リテラル組を事実項、共通した変数を持つ変数組同士の関係を規則項に変換し、さらに目的項、事実項、規則項を論理積で結合したＨｏｒｎＣＮＦに変換したデータを出力する出力部、としたプログラム
【請求項３】
コンピュータを、ＳＡＴを受け取りＣＮＦＳＡＴに変換する入力部、入力部からＣＮＦＳＡＴを受け取り、ＣＮＦＳＡＴを構成するＣＮＦの各項の構成変数の組合せによって定まる変数組を構築し、各項の構成変数とリテラル構成によって定まるリテラル組を変数組と関連付けて構築し、共通の変数を持つ変数組同士を直接または間接に関連付けて構築したデータを出力する変換部、変換部の出力したデータにおいて変数組を目的項、リテラル組を事実項、共通した変数を持つ変数組同士の関係を規則項として読み替え、さらに目的項、事実項、規則項を論理積で結合したＨｏｒｎＣＮＦに読み替えてＳＡＴ判定を行うＳＡＴ判定部、ＳＡＴ判定部の判定結果を出力する判定結果出力部、として機能させるためのプログラム
【請求項４】
請求項１、２、３において、変換部にてデータを作成する際に、変数の組合せをキーとし変数組を値とするインデックスを構築することとしたプログラム
【請求項５】
請求項１、２、３、４において、変換部にてデータを作成する際に、変数組同士を関連付けて構築したデータに共通の変数あるいは共通でない変数のデータを関連付けることとしたプログラム
【請求項６】
請求項１、２、３、４、５において、入力部を、ＳＡＴを受け取り３ＳＡＴに変換する入力部、としたプログラム
【請求項７】
請求項６において、変換部にてデータを作成する際に、変数組同士を関連付けて構築したデータに、変数組同士の共通変数が１つの場合はその変数を、変数組同士の共通でない変数が１つの場合はその変数を関連付けることとしたプログラム
【発明の詳細な説明】
【技術分野】
【０００１】本発明は、コンピュータにて論理式を変換するプログラム、及び充足可能性問題を扱うプログラムに関する
【背景技術】
【０００２】従来、コンピュータでは様々な問題が扱われており、また論理式や充足可能性問題、恒真式問題など論理に関する問題も様々なものが扱われている。【０００３】特にＳＡＴ（充足可能性問題）は、ＮＰ完全問題として非決定性チューリングマシンと等価な問題であることが判明しており、またその応用範囲も広い。そのため、以前よりコンピュータで自動的に解決するＳＡＴソルバ（本出願ではＳＡＴ解法と呼ぶ）が研究・実用化されてきた。【０００４】ＳＡＴには式の条件によって様々な種類が存在する。特にＣＮＦ（乗法標準形）で構成されたＣＮＦＳＡＴと、３ＣＮＦ（項の変数が３つまでに限定されたＣＮＦ）で構成された３ＳＡＴが重要である。ＳＡＴはＣＮＦＳＡＴや３ＳＡＴに容易に変換可能であり（例えば非特許文献３参照）、また変換後のＣＮＦや３ＣＮＦは取り扱いが容易なため、ＳＡＴ解法でも始めにＳＡＴをＣＮＦＳＡＴや３ＳＡＴに変換する手法が用いられている。また、特別なＣＮＦの一つとしてＨｏｒｎＣＮＦ（ホーン式）がある。ＨｏｒｎＣＮＦは各項に０または１の肯定リテラルが存在するＣＮＦである（本出願では１つの肯定リテラルのみからなる項を事実項、肯定リテラルが１つのみで残りが否定リテラルとなる項を規則項、否定リテラルのみからなる項を目的項と呼ぶ）。ＨｏｒｎＣＮＦはコンピュータで効率的に充足可能性の判定を行うことが可能（例えばＤＰＬＬアルゴリズム）だが、ＣＮＦからＨｏｒｎＣＮＦに効率的に変換する方法は見つかっていない。【０００５】またＳＡＴは本質的にコンピュータで計算するのが困難な問題であり、判定するのに実質不可能な指数時間が必要になることがある。また、このような問題に対して確率的な局所探索で充足可能なことを求める確率的ＳＡＴ解法もあるが、このようなＳＡＴ解法でも充足不可なことを確認するのは困難である。そのため、全ての可能性を判定し充足不可を明確化する完全ＳＡＴ解法の効率化が重要となる（例えば特許文献１参照）。【０００６】しかし、従来の完全ＳＡＴ解法や確率的ＳＡＴ解法は、充足可能である条件から式を簡約するＤＰＬＬアルゴリズム（例えば非特許文献１参照）や、可能性のある真理値割当を実際に式に適用する手法などが主であり、式の対称性を用いて効率化する手法は少なかった。また、式の対称性を用いてＳＡＴ解法を効率化する手法はあったが（例えば非特許文献２参照）、特定の条件を満たす必要のあるものがほとんどであり応用範囲が狭かった。また、充足解の計算時間をスケジューリングすることで、充足解を計算する時の負担を軽減する技術（例えば特許文献２参照）があるが、実際に計算を行う必要があるため、必ずしも効率化になるとは限らなかった。【０００７】なお、ＳＡＴを効率良く扱うために、ＳＡＴで与えられた式をＳＡＴ解法のために効率の良い形に変更することも重要となるが、そのようなプログラムにおいて、論理式をＨｏｒｎＣＮＦに効率良く変換するプログラムは存在しなかった。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２００４−３５５０３８
【特許文献２】特開２００５−２９３５７５
【０００９】
【非特許文献１】“Ａ  Ｃｏｍｐｕｔｉｎｇ  Ｐｒｏｃｅｄｕｒｅ  ｆｏｒ  Ｑｕａｎｔｉｆｉｃａｔｉｏｎ  Ｔｈｅｏｒｙ”Ｍａｒｔｉｎ  Ｄａｖｉｓ、Ｈｉｌａｒｙ  Ｐｕｔｎａｍ  Ｊｏｕｒｎａｌ  ｏｆ  ｔｈｅ  ＡＣＭ  ７  １９６０年  Ｐ２０１−２１５
【非特許文献２】「基本対称関数に基づく節をもつＣＮＦ論理式の充足可能性判定」馬野洋平，酒井正彦，西田直樹，坂部俊樹，草刈圭一朗  電子情報通信学会論文誌  Ｊ９３−Ｄ  ２０１０年  Ｐ１−９
【非特許文献３】「オートマトン  言語理論  計算論  ＩＩ」Ｊ．ホップクロフト，Ｊ．ウルマン，Ｒ．モトワニ  サイエンス社  ２００８年  Ｐ１４７−１５５
【発明の概要】
【発明が解決しようとする課題】
【００１０】上記の通り、論理式の対称性を活用して効率化する汎用性の高いＳＡＴ解法が存在しなかった。また、論理式の充足可能性を効率的に求めることのできるＨｏｒｎＣＮＦの形式に変換するプログラムが存在しなかった。
【課題を解決するための手段】
【００１１】上記の問題を解決するため、本発明では、ＣＮＦを下記の手順にてＨｏｒｎＣＮＦに変更することとした。まず始めにＣＮＦの各項を事実項に読み替える。次に事実項の満たすべき制約を、次の２つの制約条件からＨｏｒｎＣＮＦの充足可能性に読み替える。一つは各項のリテラルの肯定否定を変更した項の全ての場合を論理積にした式の充足可能性を満たすことから導かれる目的項であり、もう一つは共通変数を持つ項同士の共通変数部分の満たす必要のある同一性から導かれる規則項である。そして、上記の事実項、目的項、規則項を論理積で結合しＨｏｒｎＣＮＦにする。【００１２】また、上記の問題を解決するため、本発明では、コンピュータを、ＳＡＴを受け取りＣＮＦＳＡＴに変換する入力部、入力部からＣＮＦＳＡＴを受け取り、ＣＮＦＳＡＴを構成するＣＮＦの各項の変数の組合せによって定まる変数組を構築し、各項の構成変数とリテラル構成によって定まるリテラル組を変数組と関連付けて構築し、共通の変数を持つ変数組同士を直接または間接に関連付けて構築したデータを出力する変換部、変換部が構築したデータを出力する出力部、として機能させるためのプログラムとした。【００１３】また、上記のプログラムにおいて、出力部を、変換部が構築したデータにおいて変数組を目的項、リテラル組を事実項、共通した変数を持つ変数組同士の関係を規則項に変換し、さらに目的項、事実項、規則項を論理積で結合したＨｏｒｎＣＮＦに変換したデータを出力する出力部、としたプログラムとすることもある。【００１４】また同様に、コンピュータを、ＳＡＴを受け取りＣＮＦＳＡＴに変換する入力部、入力部からＣＮＦＳＡＴを受け取り、ＣＮＦＳＡＴを構成するＣＮＦの各項の構成変数の組合せによって定まる変数組を構築し、各項の構成変数とリテラル構成によって定まるリテラル組を変数組と関連付けて構築し、共通の変数を持つ変数組同士を直接または間接に関連付けて構築したデータを出力する変換部、変換部の出力したデータにおいて変数組を目的項、リテラル組を事実項、共通した変数を持つ変数組同士の関係を規則項として読み替え、さらに目的項、事実項、規則項を論理積で結合したＨｏｒｎＣＮＦに読み替えてＳＡＴ判定を行うＳＡＴ判定部、ＳＡＴ判定部の判定結果を出力する判定結果出力部、として機能させるためのプログラムとした。【００１５】また、上記のプログラムにおいて、変換部にてデータを作成する際に、変数の組合せをキーとし変数組を値とするインデックスを構築することとしたプログラムとすることもある。【００１６】また、上記のプログラムにおいて、変換部にてデータを作成する際に、変数組同士を関連付けて構築したデータに共通の変数あるいは共通でない変数のデータを関連付けることとしたプログラムとすることもある。【００１７】また、上記のプログラムにおいて、入力部を、ＳＡＴを受け取り３ＳＡＴに変換する入力部、としたプログラムとすることもある。【００１８】また、上記のプログラムにおいて、変換部にてデータを作成する際に、変数組同士を関連付けて構築したデータに、変数組同士の共通変数が１つの場合はその変数を、変数組同士の共通でない変数が１つの場合はその変数を関連付けることとしたプログラムとすることもある。
【発明の効果】
【００１９】本発明により、ＳＡＴの持つ変数の対称性を活用して、コンピュータで取り扱いやすいＨｏｒｎＣＮＦの形で処理することが可能となった。またその結果を用いて効率的にＳＡＴをコンピュータで処理することが可能となった。
【図面の簡単な説明】
【００２０】
【図１】本発明の実施形態の一例を示す構成図である。
【図２】本発明の実施形態の一例で使用するデータ構造の構成図である。
【図３】本発明の実施形態の一例で使用するデータ構造の構成図である。
【発明を実施するための形態】
【００２１】以下に本発明の実施形態の一つについて、図面に基づき説明する。図１は本発明のプログラムの構成図である。
【００２２】本プログラムは、ＳＡＴを受け取る入力部１１１、入力部１１１から受け取った問題を元に、ＳＡＴをＣＮＦＳＡＴに変換した後に各項を変数ごとに分類する変換部１１２、変換したデータを出力するデータ出力部１１３からなる。また、データ出力部１１３に替えて、変換部が作成したデータを直接受け取って充足可能性を判定するＳＡＴ判定部１２１、及びＳＡＴ判定部１２１の結果を出力する判定結果出力部１２２があることもある。
【００２３】入力部１１１の詳細を説明する。入力部１１１はメモリ、ストレージ、ＩＯ、他のプログラムなど、通常のコンピュータで使用される入出力部からの入力を受け取る。
【００２４】受け取った入力がＳＡＴの条件を満たしている場合は入力をＣＮＦＳＡＴに変換して変換部１１２に出力する。ＳＡＴからＣＮＦＳＡＴへの変換は広く知られている方法を用いる（例えば非特許文献３参照）。プログラムによっては正規化を一段進めて３ＳＡＴに変換する場合もある。また、変換部１１２に出力する際に、ＣＮＦや３ＣＮＦを作成するときに付加した変数を識別可能なように渡すことがある。例えば変数にＣＮＦに変換するときに付加した変数、あるいは３ＣＮＦに変換するときに付加した変数であることがわかるように、変数に識別子を付けたり、変数の一覧を別途データとして渡したりすることがある。ＣＮＦを作成するときに付加する変数は肯定リテラルと否定リテラルの数が同数になる。また３ＣＮＦを作成する時に付加する変数は肯定リテラルと否定リテラルがそれぞれ一つの項にしか出て来ない。よって、このような特徴を、充足可能性を判定するときに活用することで判定を効率化することができる。
【００２５】また、入力がＳＡＴの条件を満たしていない場合は入力を拒絶する。拒絶の方法は一般的なプログラムで計算失敗として行われている動作を用いる。例えば判定結果出力部１２２がある場合は充足不可として判定結果出力部１２２に出力する場合もあるし、単に入力を無視することもある。また通常のプログラムで行われている動作（特殊な値の出力、例外の発行）なども行うことがあるが、この内容に制限されない。
【００２６】なお、入力は論理式及び論理式の変数の満たす条件で構成されている。論理式や論理式を表すバイナリ列など、一般的に論理の問題の省略形の表現に使用するデータを受け取ることも可能とするが、この内容に制限されない。
【００２７】また、簡単化のため、本例のＣＮＦでは変数の肯定リテラルに偶数番号を付けることとする。否定リテラルを表現する場合は、単に否定演算を付ける場合もあるが、変数の番号に１を加えた奇数番号で表現することもある。
【００２８】変換部１１２の詳細を説明する。
【００２９】変換部１１２は、入力部１１１からの出力としてＣＮＦを受け取ると、ＣＮＦの項を変数の組合せごとに分類し、さらに変数のリテラルにより分類する。そして、その分類結果をデータとして記憶する。
【００３０】変換部１１２の作成するデータ構造の例を図２に示す。データ構造にはＣＮＦの各項を変数の対称性から整理したデータがある。各変数の組み合わせに関連する情報をまとめたデータ（本出願ではこのデータを変数組と呼ぶ）があり、そこには組になっている変数を表すデータがある。図２の例では、変数組２１１には（Ｘ０，Ｘ２，Ｘ４）が、変数組２２１には（Ｘ２，Ｘ４，Ｘ６）が、変数組２３１には（Ｘ４，Ｘ６，Ｘ８）がデータとしてある。なお、この変数のデータは後述のインデックスと共有することがある。
【００３１】また、さらなる正規化のため、例えば変数組２４１のように、項としては存在しないが各項の共通変数としては存在する変数組を用意することがある。その時のデータ構造を図３に示す。特に、同じ共通変数を持つ項が３つ以上になる場合、共通変数の変数組を用意した方が変数組同士の組合せがより少なくなるため（３つでほぼ同等の組合せ数）、同じ共通変数を持つ項が２つしか存在しない場合は共通変数の変数組を用意せず、同じ共通変数を持つ項が３つ以上になってから初めて共通変数の変数組を用意する機能になっていることがある。
【００３２】なお、変数組の検索を容易にするため、変数の組合せに対応する変数組へのインデックスが存在する場合がある。インデックス構造は、従来から索引用の構造として良く使われるツリー構造やハッシュテーブル、配列、連想配列などが使われるが、これに限定するものではない。また、インデックスのキー情報も、変数組に関連付けられた変数全ての組合せだけではなく、変数の部分集合も含むことがある。変数の部分集合も含むことによって、変数組の共通変数を容易に検索することができるようになり、既に同じ共通変数を持つ変数組が存在するか、存在するとしたらどの変数組になるかを確認することも容易となり、インデックスの検索結果から、実際に変数組２４１のような共通変数のみからなる変数組を用意する必要があるかどうかの判断も容易に行うことができるようになる。
また、変数組２４１のような共通変数のみの変数組を検索するのも容易となる。
【００３３】また、変数組の変数の情報には変数名以外の情報が含まれることがある。例えば、入力部１１１から入手した、ＣＮＦや３ＣＮＦに変換するときに追加した変数かどうかを示す情報などである。
【００３４】変数組には、ＣＮＦに含まれる同じ変数の項の肯定否定リテラルがどのようになっているかを表すデータ（本出願ではこのデータをリテラル組と呼ぶ）が関連付けられている。リテラル組は、変数組とセットで各項の構成を表す。リテラル組２１３は（肯定・否定・否定）の組（Ｘ０∨¬Ｘ２∨¬Ｘ４）を、リテラル組２１４は（肯定・否定・肯定）の組（Ｘ０∨¬Ｘ２∨Ｘ４）を、リテラル組２２３は（肯定・否定・肯定）の組（Ｘ２∨¬Ｘ４∨Ｘ６）を、リテラル組２３３は（肯定・否定・肯定）の組（Ｘ４∨¬Ｘ６∨Ｘ８）を、それぞれ表す。変数組２４１のように実際の項が存在しない変数組にはリテラル組が関連付けられていない。
【００３５】変数組には、自分と持つ変数と共通の変数を持つ変数組との関係が記録されている。例えば変数組２１１は変数組２２１と（Ｘ０，Ｘ２）が、変数組２３１と（Ｘ４）が共通になっている。そのため、変数組２１１には変数組２２１と変数組２３１への参照が含まれている。なお、変数組２２１にも同様に変数組２１１と変数組２３１への参照が、変数組２３１にも同様に変数組２１１と変数組２２１への参照が含まれている。なお、複雑になるのを防ぐために、変数組２１１と変数組２２１同士の参照を、変数組２４１のような共通変数のみからなる変数組との関係に置き換える場合がある。特に、同じ共通変数を持つ項が２つしか存在しない場合は共通変数の変数組を用意せず、同じ共通変数を持つ項が３つ以上になってから初めて共通変数の変数組との関係に置き換える手順になっていることがある。
【００３６】なお、データのサイズの節約のために、共通変数を持つ変数組同士の参照が両方向ではなく片方向になっている場合がある。
【００３７】なお、この変数組同士の関係を表す情報には、共通変数を持つ変数組への参照以外の情報が含まれることがある。例えば、参照を保存する構造を、参照元として鍵となる変数ごとに整理する構造にすることで、参照に情報を付加することができる。また参照先を単に変数組にするのではなく、参照先の変数組の変数に関連付けられたデータへの参照とすることで、参照先として鍵となる変数がわかるようにすることもできる。当然、このような情報がなくてもお互いの変数組の変数のデータを比較することで共通変数と共通でない変数を確定することができるが、あらかじめデータとして持つことで計算を効率化することができる。
【００３８】具体的として、参照に変数組同士に共通しない変数の情報を追加したものを挙げる。参照元が変数組２３１で参照先が変数組２２１の参照において、参照自体を変数組２３１の変数Ｘ８に関連付けられた配列に保存し、参照先として変数組２２１の変数Ｘ２を参照するようにする。すると、実際にこの参照を辿る時には変数組２３１の変数Ｘ８という情報と変数組２２１の変数Ｘ２という情報を得ることができる。そして元の変数組２３１の変数構成の情報を活用することにより、変数組２２１と変数組２３１の共通する変数（Ｘ４、Ｘ６）と異なる変数（Ｘ２）（Ｘ８）を明らかにすることができる。このように、変数組同士の関係に、共通しない変数の情報が含まれることがある。なお、共通しない変数が複数の場合などのように、参照元・参照先の情報が複数変数の組合せになることがある。また、通常用いられるデータ構造（参照と変数をセットにしたデータなど）で情報を含むことがある。
【００３９】なお、変数組２４１と変数組２１１のように、片方の変数組の変数がもう片方の変数組の変数の部分集合の場合、そのことを表す特別な記号（空白など）やデータ構造（変数を表す配列の先頭は常に特別扱いにするなど）で対応する場合がある。
【００４０】また同様に、変数組同士の関係を表す情報に、共通する変数の情報を追加することがある。参照元が変数組２３１で参照先が変数組２１１の参照において、参照自体を変数組２３１の変数Ｘ４を表す配列に保存し、参照先として変数組２１１の変数Ｘ４を参照するようにする。すると、実際にこの参照を辿る時には変数組２３１の変数Ｘ４という情報と変数組２１１の変数Ｘ４という情報を得ることができる。ここで、参照元と参照先の変数が同一であることがわかるため、あらかじめ参照元と参照先の変数が同一の時は変数組の共通変数を表すものと定めておけば、参照元の変数組２３１と参照先の変数組２１１の変数構成の情報を活用して、変数組２１１と変数組２３１の共通する変数（Ｘ４）と異なる変数（Ｘ０、Ｘ２）（Ｘ６、Ｘ８）を明らかにすることができる。このように、変数組同士の関係に、共通する変数の情報が含まれることがある。なお、共通する変数が複数の場合などのように、参照元・参照先の情報が複数変数の組合せになることがある。
また、通常用いられるデータ構造（参照と変数をセットにしたデータなど）で情報を含むことがある。
【００４１】なお、３ＳＡＴの場合、項同士の変数の関係は、一つの変数が共通になるか、あるいは一つの変数が異なるか、の２通りしか無い。そのため、参照元の変数と参照先の変数が同じかどうかを確認することによって、その変数が共通変数なのかどうかを容易に判断することができる。具体的には、参照元の変数と参照先の変数が同じ場合は共通の変数を表し、異なる場合は共通でない変数を表すことにすることで識別することができる。
よって、変換部１１２が３ＳＡＴを受け取った場合は、上記の手法で共通変数と共通でない変数を示すことがある。
【００４２】変換部１１２は、このようにして構成したデータをデータ出力部１１３、ＳＡＴ判定部１２１に出力する。なお、データには変数の組合せから変数組へのインデックスなど、データ作成の途中で生成したデータを一緒に出力することがある。また、変換部１１２は、後のＳＡＴ判定で効率が良くなるように、変数組に優先度を付ける場合がある。
例えば、変数組において、変数組の変数に対してリテラル組の比率が高い変数組の優先度を高くする／共通変数となる変数組が多い変数組の優先度を上げるなどである。
【００４３】データ出力部１１３の詳細を説明する。データ出力部１１３は、変換部１１２からの入力を変換したデータを受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、データ作成の途中で生成したデータなどを含むことがある。他のプログラムはこのデータを活用してＳＡＴ計算やデータ解析などの処理を行う。また、データ出力部１１３の出力したデータには、ＳＡＴの潜在的な構造や対称性が顕在化された形で表現されているため、このデータを用いることでＳＡＴの構造の解析が容易となっている。そのため、ＳＡＴの難易度の評価を、実際に計算を始める前に見積もることができる。
【００４４】なお、データ出力部１１３は、変換部１１２で作成したデータを、後述のＳＡＴ判定部１２１の機能として説明しているＨｏｒｎＣＮＦ変換手順にてＨｏｒｎＣＮＦを作成して出力する場合がある。
【００４５】ＳＡＴ判定部１２１の詳細を説明する。
【００４６】ＳＡＴ判定部１２１は、変換部１１２からデータを受け取ると、データをＨｏｒｎＣＮＦに読み替えて充足可能性を判定する。変換部１１２のデータは、それぞれの部分を読み替えることでＨｏｒｎＣＮＦとして捉えることができる。
【００４７】まず、各変数組のリテラル組をそれぞれ一つの変数に読み替える。変数組２１１のリテラル組２１３はＹ０３５に、リテラル組２１４はＹ０３４に読み替える。ただし、元の項は下記の条件で充足不可となることを考える必要がある。
（  Ｘ０∨  Ｘ２∨  Ｘ４）∧（¬Ｘ０∨  Ｘ２∨  Ｘ４）∧
（  Ｘ０∨¬Ｘ２∨  Ｘ４）∧（  Ｘ０∨  Ｘ２∨¬Ｘ４）∧
（  Ｘ０∨¬Ｘ２∨¬Ｘ４）∧（¬Ｘ０∨  Ｘ２∨¬Ｘ４）∧
（¬Ｘ０∨¬Ｘ２∨  Ｘ４）∧（¬Ｘ０∨¬Ｘ２∨¬Ｘ４）
＝矛盾
ここで、変数組に存在する可能性のある項毎に下記のように変数を割り当てる。
（  Ｘ０∨  Ｘ２∨  Ｘ４）＝Ｙ０２４、
（¬Ｘ０∨  Ｘ２∨  Ｘ４）＝Ｙ１２４、
（  Ｘ０∨¬Ｘ２∨  Ｘ４）＝Ｙ０３４、
（  Ｘ０∨  Ｘ２∨¬Ｘ４）＝Ｙ０２５、
（  Ｘ０∨¬Ｘ２∨¬Ｘ４）＝Ｙ０３５、
（¬Ｘ０∨  Ｘ２∨¬Ｘ４）＝Ｙ１２５、
（¬Ｘ０∨¬Ｘ２∨  Ｘ４）＝Ｙ１３４、
（¬Ｘ０∨¬Ｘ２∨¬Ｘ４）＝Ｙ１３５
（本出願では上記のような変数組に対応する項を変数組項、変数組項に対応する変数を変数組変数、変数組項のうちでリテラル組に対応する項をリテラル組項、リテラル組項に対応する変数組変数をリテラル組変数と呼ぶ）
とすると、変数組変数は下記の条件を満たす必要がある。
Ｙ０２４∧Ｙ１２４∧Ｙ０３４∧Ｙ０２５∧
Ｙ０３５∧Ｙ１２５∧Ｙ１３４∧Ｙ１３５
＝矛盾
¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ０２５∨
¬Ｙ０３５∨¬Ｙ１２５∨¬Ｙ１３４∨¬Ｙ１３５
＝恒真
よって、リテラル組２１３とリテラル組２１４の表していたＣＮＦが充足するのは、
［変数組２１１の成立条件］＝
（Ｘ０∨¬Ｘ２∨¬Ｘ４）∧（Ｘ０∨¬Ｘ２∨Ｘ４）
＝Ｙ０３５∧Ｙ０３４
∧（¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ０２５∨¬Ｙ０３５∨¬Ｙ１２５∨¬Ｙ１３４∨¬Ｙ１３５）
というＨｏｒｎＣＮＦが充足するときのみである。
【００４８】上記は下記の手順を適用した結果である。各変数組に対応する変数を全て含む項を用意し、その項の肯定否定リテラル全ての組合せとなる変数組項を用意し、その項毎に変数組変数を割り当てる。そしてリテラル組で表現されるリテラル組項を変数組変数に変更して事実項とする。ただし、変数組変数には変数組項の持つ充足可能性に関する制約条件があるため、変数組変数に置き換えたＣＮＦとその制約条件となる（その変数組の全ての変数組変数を含む）目的項の論理積とする。こうすることによって、変換部１１２から受け取ったデータをＨｏｒｎＣＮＦ（の一部）として読み替えることができる。
【００４９】ただし、上記のＨｏｒｎＣＮＦは変数組の変数の一部重複を考慮していない、変数組が全て独立している場合のＨｏｒｎＣＮＦとなる。変数組の変数の重複を考慮すると、下記の条件を追加する必要がある。
【００５０】まず始めに、変数組２１１と変数組２２１のように、変数が２つ重複する場合を示す。なお、変数組２２１の変数組項及び変数組変数は下記の通りとする。
（  Ｘ２∨  Ｘ４∨  Ｘ６）＝Ｙ２４６、
（¬Ｘ２∨  Ｘ４∨  Ｘ６）＝Ｙ３４６、
（  Ｘ２∨¬Ｘ４∨  Ｘ６）＝Ｙ２５６、
（  Ｘ２∨  Ｘ４∨¬Ｘ６）＝Ｙ２４７、
（  Ｘ２∨¬Ｘ４∨¬Ｘ６）＝Ｙ２５７、
（¬Ｘ２∨  Ｘ４∨¬Ｘ６）＝Ｙ３４７、
（¬Ｘ２∨¬Ｘ４∨  Ｘ６）＝Ｙ３５６、
（¬Ｘ２∨¬Ｘ４∨¬Ｘ６）＝Ｙ３５７
【００５１】重複部分の取り得る値を考えると、（Ｘ２∨Ｘ４）が真かつ偽となることは有り得ないため、
¬（Ｘ２∨Ｘ４∨Ｘ６）
∧（Ｘ０∨Ｘ２∨Ｘ４）∧（¬Ｘ０∨Ｘ２∨Ｘ４）
＝矛盾
よって
（Ｘ２∨Ｘ４∨Ｘ６）∨¬（Ｘ０∨Ｘ２∨Ｘ４）∨¬（¬Ｘ０∨Ｘ２∨Ｘ４）
＝Ｙ２４６∨¬Ｙ０２４∨¬Ｙ１２４
＝恒真
という条件を満たす必要がある。この関係は全ての変数組変数について成立するから、
恒真
＝Ｙ２４６∨¬Ｙ０２４∨¬Ｙ１２４＝Ｙ２４７∨¬Ｙ０２４∨¬Ｙ１２４
＝Ｙ３４６∨¬Ｙ０３４∨¬Ｙ１３４＝Ｙ３４７∨¬Ｙ０３４∨¬Ｙ１３４
＝Ｙ２５６∨¬Ｙ０２５∨¬Ｙ１２５＝Ｙ２５７∨¬Ｙ０２５∨¬Ｙ１２５
＝Ｙ３５６∨¬Ｙ０３５∨¬Ｙ１３５＝Ｙ３５７∨¬Ｙ０３５∨¬Ｙ１３５
＝Ｙ０２４∨¬Ｙ２４６∨¬Ｙ２４７＝Ｙ１２４∨¬Ｙ２４６∨¬Ｙ２４７
＝Ｙ０３４∨¬Ｙ３４６∨¬Ｙ３４７＝Ｙ１３４∨¬Ｙ３４６∨¬Ｙ３４７
＝Ｙ０２５∨¬Ｙ２５６∨¬Ｙ２５７＝Ｙ１２５∨¬Ｙ２５６∨¬Ｙ２５７
＝Ｙ０３５∨¬Ｙ３５６∨¬Ｙ３５７＝Ｙ０３５∨¬Ｙ３５６∨¬Ｙ３５７
となる必要がある。
【００５２】つまり、変数組２１１と変数組２２１の関係が成立するのは
［変数組２１１と変数組２２１の重複部分の成立条件］＝
（Ｙ２４６∨¬Ｙ０２４∨¬Ｙ１２４）∧（Ｙ２４７∨¬Ｙ０２４∨¬Ｙ１２４）∧
（Ｙ３４６∨¬Ｙ０３４∨¬Ｙ１３４）∧（Ｙ３４７∨¬Ｙ０３４∨¬Ｙ１３４）∧
（Ｙ２５６∨¬Ｙ０２５∨¬Ｙ１２５）∧（Ｙ２５７∨¬Ｙ０２５∨¬Ｙ１２５）∧
（Ｙ３５６∨¬Ｙ０３５∨¬Ｙ１３５）∧（Ｙ３５７∨¬Ｙ０３５∨¬Ｙ１３５）∧
（Ｙ０２４∨¬Ｙ２４６∨¬Ｙ２４７）∧（Ｙ１２４∨¬Ｙ２４６∨¬Ｙ２４７）∧
（Ｙ０３４∨¬Ｙ３４６∨¬Ｙ３４７）∧（Ｙ１３４∨¬Ｙ３４６∨¬Ｙ３４７）∧
（Ｙ０２５∨¬Ｙ２５６∨¬Ｙ２５７）∧（Ｙ１２５∨¬Ｙ２５６∨¬Ｙ２５７）∧
（Ｙ０３５∨¬Ｙ３５６∨¬Ｙ３５７）∧（Ｙ０３５∨¬Ｙ３５６∨¬Ｙ３５７）
というＨｏｒｎＣＮＦが充足するときのみである。
【００５３】同様に、変数組２１１と変数組２３１のように、変数が１つ重複する場合を示す。なお、変数組２３１の変数組項と変数組変数は下記の通りとする。
（  Ｘ４∨  Ｘ６∨  Ｘ８）＝Ｙ４６８、
（¬Ｘ４∨  Ｘ６∨  Ｘ８）＝Ｙ５６８、
（  Ｘ４∨¬Ｘ６∨  Ｘ８）＝Ｙ４７８、
（  Ｘ４∨  Ｘ６∨¬Ｘ８）＝Ｙ４６９、
（  Ｘ４∨¬Ｘ６∨¬Ｘ８）＝Ｙ４７９、
（¬Ｘ４∨  Ｘ６∨¬Ｘ８）＝Ｙ５６９、
（¬Ｘ４∨¬Ｘ６∨  Ｘ８）＝Ｙ５７８、
（¬Ｘ４∨¬Ｘ６∨¬Ｘ８）＝Ｙ５７９
【００５４】重複部分の取り得る値を考えると、（Ｘ４）が真かつ偽となることは有り得ないため、
¬（Ｘ４∨Ｘ６∨Ｘ８）
∧（  Ｘ０∨  Ｘ２∨Ｘ４）∧（¬Ｘ０∨  Ｘ２∨Ｘ４）
∧（  Ｘ０∨¬Ｘ２∨Ｘ４）∧（¬Ｘ０∨¬Ｘ２∨Ｘ４）
＝矛盾
よって
（Ｘ４∨Ｘ６∨Ｘ８）
∨¬（  Ｘ０∨  Ｘ２∨Ｘ４）∨¬（¬Ｘ０∨  Ｘ２∨Ｘ４）
∨¬（  Ｘ０∨¬Ｘ２∨Ｘ４）∨¬（¬Ｘ０∨¬Ｘ２∨Ｘ４）
＝Ｙ４６８∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４
＝恒真
という条件を満たす必要がある。この関係は全ての変数組変数について成立するから、
恒真
＝Ｙ４６８∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４
＝Ｙ４７８∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４
＝Ｙ４６９∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４
＝Ｙ４７９∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４
＝Ｙ５６８∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５
＝Ｙ５７８∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５
＝Ｙ５６９∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５
＝Ｙ５７９∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５
＝Ｙ０２４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９
＝Ｙ１２４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９
＝Ｙ０３４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９
＝Ｙ１３４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９
＝Ｙ０２５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９
＝Ｙ１２５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９
＝Ｙ０３５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９
＝Ｙ１３５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９
となる必要がある。
【００５５】つまり、変数組２１１と変数組２３１の関係が成立するのは、
［変数組２１１と変数組２３１の重複部分の成立条件］＝
（Ｙ４６８∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４）∧
（Ｙ４７８∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４）∧
（Ｙ４６９∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４）∧
（Ｙ４７９∨¬Ｙ０２４∨¬Ｙ１２４∨¬Ｙ０３４∨¬Ｙ１３４）∧
（Ｙ５６８∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５）∧
（Ｙ５７８∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５）∧
（Ｙ５６９∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５）∧
（Ｙ５７９∨¬Ｙ０２５∨¬Ｙ１２５∨¬Ｙ０３５∨¬Ｙ１３５）∧
（Ｙ０２４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９）∧
（Ｙ１２４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９）∧
（Ｙ０３４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９）∧
（Ｙ１３４∨¬Ｙ４６８∨¬Ｙ４７８∨¬Ｙ４６９∨¬Ｙ４７９）∧
（Ｙ０２５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９）∧
（Ｙ１２５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９）∧
（Ｙ０３５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９）∧
（Ｙ１３５∨¬Ｙ５６８∨¬Ｙ５７８∨¬Ｙ５６９∨¬Ｙ５７９）
というＨｏｒｎＣＮＦが充足するときのみである。
【００５６】なお、変数組２１１と変数組２２１の関係を直接表さず、共通部分の変数組２４１を介することで表現することもできる。この場合、変数組２１１と変数組２２１の関係は、変数組２１１と変数組２４１の関係及び変数組２２１と変数組２４１の関係の２つの関係として表現される。
【００５７】上記の例として変数組２１１と変数組２４１の関係を表すことを示す。なお、変数組２４１の変数組項と変数組変数は下記の通りとする。
（  Ｘ２∨  Ｘ４∨）＝Ｙ２４、（¬Ｘ２∨  Ｘ４∨）＝Ｙ３４、
（  Ｘ２∨¬Ｘ４∨）＝Ｙ２５、（¬Ｘ２∨¬Ｘ４∨）＝Ｙ３５
【００５８】重複部分の取り得る値を考えると、（Ｘ２∨Ｘ４）が真かつ偽となることは有り得ないため、
¬（Ｘ２∨Ｘ４）∧（Ｘ０∨Ｘ２∨Ｘ４）∧（¬Ｘ０∨Ｘ２∨Ｘ４）＝矛盾
よって
（Ｘ２∨Ｘ４）∨¬（Ｘ０∨Ｘ２∨Ｘ４）∨¬（¬Ｘ０∨Ｘ２∨Ｘ４）
＝Ｙ２４∨¬Ｙ０２４∨¬Ｙ１２４＝恒真
という条件を満たす必要がある。逆についても同様に、
¬（Ｘ０∨Ｘ２∨Ｘ４）∧（Ｘ２∨Ｘ４）＝矛盾
よって
¬（Ｘ０∨Ｘ２∨Ｘ４）∧（Ｘ２∨Ｘ４）＝矛盾
（Ｘ０∨Ｘ２∨Ｘ４）∨¬（Ｘ２∨Ｘ４）＝Ｙ０２４∨¬Ｙ２４＝恒真
となる。この関係は全ての変数組変数について成立するから、
恒真
＝Ｙ２４∨¬Ｙ０２４∨¬Ｙ１２４
＝Ｙ３４∨¬Ｙ０３４∨¬Ｙ１３４
＝Ｙ２５∨¬Ｙ０２５∨¬Ｙ１２５
＝Ｙ３５∨¬Ｙ０３５∨¬Ｙ１３５
＝Ｙ０２４∨¬Ｙ２４
＝Ｙ０３４∨¬Ｙ３４
＝Ｙ０２５∨¬Ｙ２５
＝Ｙ０３５∨¬Ｙ３５
＝Ｙ１２４∨¬Ｙ２４
＝Ｙ１３４∨¬Ｙ３４
＝Ｙ１２５∨¬Ｙ２５
＝Ｙ１３５∨¬Ｙ３５
となる必要がある。
【００５９】つまり、変数組２１１と変数組２４１の関係が成立するのは
［変数組２１１と変数組２４１の重複部分の成立条件］＝
（Ｙ２４∨¬Ｙ０２４∨¬Ｙ１２４）∧
（Ｙ３４∨¬Ｙ０３４∨¬Ｙ１３４）∧
（Ｙ２５∨¬Ｙ０２５∨¬Ｙ１２５）∧
（Ｙ３５∨¬Ｙ０３５∨¬Ｙ１３５）∧
（Ｙ０２４∨¬Ｙ２４）∧（Ｙ０３４∨¬Ｙ３４）∧
（Ｙ０２５∨¬Ｙ２５）∧（Ｙ０３５∨¬Ｙ３５）∧
（Ｙ１２４∨¬Ｙ２４）∧（Ｙ１３４∨¬Ｙ３４）∧
（Ｙ１２５∨¬Ｙ２５）∧（Ｙ１３５∨¬Ｙ３５）
というＨｏｒｎＣＮＦが充足するときのみである。
【００６０】このように、変換部１１２によってお互いに関連つけられた２つの変数組それぞれについて、お互いの共通変数が同時に真と偽になることがないという制約条件から、変数組変数の満たす必要のある制約条件を規則項からなるＨｏｒｎＣＮＦの充足可能性として表現する。具体的には、まず片方の変数組変数（仮にＸと呼ぶ）の否定と、もう片方の変数組変数でＸの共通変数部分の論理和が真でないと式全体も真にならないように組んだ変数組変数の論理積（仮にＹと呼ぶ）を作成し、¬Ｘ∧Ｙ＝矛盾→Ｘ∨¬Ｙ＝恒真とすることで制約条件を規則項からなるＨｏｒｎＣＮＦの充足可能性に読み替える。
【００６１】なお、上記の関係は３ＣＮＦについてだが、同様にして４変数以上の項を扱うことができる。つまり、４変数以上の変数組についても、変換部１１２によってお互いに関連つけられた２つの変数組それぞれについて、お互いの共通変数が同時に真と偽になることがないという制約条件から変数組変数の満たす必要のある制約条件を規則項からなるＨｏｒｎＣＮＦの充足可能性として表現する。具体的には、まず片方の変数組変数（仮にＸと呼ぶ）の否定と、もう片方の変数組変数でＸの共通変数部分の論理和が真でないと式全体も真にならないように組んだ変数組変数の論理積（仮にＹと呼ぶ）を作成し、¬Ｘ∧Ｙ＝矛盾→Ｘ∨¬Ｙ＝恒真とすることで制約条件を規則項からなるＨｏｒｎＣＮＦの充足可能性に読み替える。そして全ての変数についてその規則項を読み替える。
【００６２】上記のように、変数組及び変数組同士の関係を、規則項からなるＨｏｒｎＣＮＦに読み替えることができる。また、変数組及び変数組同士の関係はＣＮＦを表しているから、すなわちＣＮＦをＨｏｒｎＣＮＦに読み替えることができる。なお、この読み替えは変換部１１２から受け取ったデータを実際に書き換える必要はなく、単にデータを読み替えるだけでＨｏｒｎＣＮＦと解釈することが可能である。
【００６３】また、ＳＡＴ判定部１２１の一例では、変換部１１２から受け取ったデータを上記の手順に従い実際のＨｏｒｎＣＮＦに変換し、そのＨｏｒｎＣＮＦの充足可能性を判定することで元のＳＡＴの判定を行ことがある。なお、このようなＨｏｒｎＣＮＦを直接判定するＳＡＴ判定部１２１の場合、判定前に全てＨｏｒｎＣＮＦに変換するのではなく、実際に計算を行う部分だけデータをＨｏｒｎＣＮＦに変換する、あるいはまったくＨｏｒｎＣＮＦに変換せずに計算する場合がある。
【００６４】またＳＡＴ判定部１２１は、効率化のために以下の機能を持つ場合がある。
【００６５】変換部１１２によって高い優先度の付けられた変数組を優先して処理することがある。変換部１１２では多くのリテラル組を含む変数組や、関係する他の変数組の多い変数組の優先度を高く設定することがある。これらの変数組は、ＳＡＴにおいて充足不可となる部分集合の一部となることが多いため、優先して判定を行うことでＳＡＴ判定を効率化できる可能性がある。
【００６６】同様にＳＡＴ判定部１２１は、ＨｏｒｎＣＮＦの充足可能性を判定する時の履歴を記憶し、その履歴に応じて優先して処理する変数組を変更することがある。例えば、ＳＡＴ判定の時に、繰り返し対象となる変数組を優先して処理するなどである。同じ変数組が繰り返し出て来るということは、その変数組がＨｏｒｎＣＮＦ（及び元のＳＡＴ）の充足可能性に重要な影響を与える変数組である可能性が高い。そのため、他の変数組よりも優先して処理する利点が多い。
【００６７】同様にＳＡＴ判定部１２１は、ＣＮＦや３ＣＮＦに変更するときに追加した変数を含む変数組の優先度を低くすることがある。ＣＮＦや３ＣＮＦ変換時に追加した変数は、他の変数への橋渡しなどの役割を果たしているため、直接ＳＡＴの充足可能性に重要な影響を与えることは少ないと考えられる。そこで、このような変数組は優先度を落とすことで、他の変数組を優先して処理することができる。
【００６８】また、ＳＡＴ判定部１２１は、変換部１１２から受け取ったデータを元に、実際に計算を始める前にＳＡＴの難易度を評価することができる。データに含まれる共通変数を持つ変数組同士の関係やリテラル組が規則的な場合はＳＡＴの難易度が低いことが予想されるし、逆に規則性が存在しない場合はＳＡＴの難易度が高いことが予想される。
また、リテラル組や変数組同士の関係が少ない場合はＳＡＴの難易度が低いことが予想されるし、リテラル組や変数組同士の関係が多い場合はＳＡＴの難易度が高いことが予想される。また、変数組を、共通変数を持つ変数組同士の関係の少ない、互いに独立性の高い集合に分割することができれば、その２つの集合を並行して処理（例えばＤＰＬＬアルゴリズムの分割規則を使用）することで処理速度を上げることができる。また同様に、通常ＨｏｒｎＣＮＦのＳＡＴで行われる手法を使用することができる。
【００６９】ＳＡＴ判定部１２１は、判定結果を判定結果出力部１２２に出力する。
【００７０】判定結果出力部１２２の詳細を説明する。判定結果出力部１２２は、ＳＡＴ判定部１２１から判定結果を受け取り、他のプログラムなど通常のコンピュータで使用される入出力部への出力を行う。他のプログラムには通常の表示プログラムや、他の演算プログラムなど、様々なプログラムが存在する。変換したデータには、変換結果だけではなく、変換で使用した変数やリテラルの対応関係、充足可能な真理値割当などの情報を含むことがある。また、そのために入力部１１１や変換部１１２、ＳＡＴ判定部１２１から計算過程・結果のデータを受け取ることがある。
【産業上の利用可能性】
【００７１】ＳＡＴに帰着可能な問題全般について、その構造の持つ対称性を効果的に活用して、効率的に充足可能性を判定することができるようになった。また、問題の持つ潜在的な構造を顕在化することによって、その解析を容易に行うことができるようになった。
また、解析によってＳＡＴの難易度の評価を、実際に計算を始める前に見積もることができるようになった。
【符号の説明】
【００７２】１１１  入力部
１１２  変換部
１１３  データ出力部
１２１  ＳＡＴ判定部
１２２  判定結果出力部
２１１  変数組
２１２  参照配列
２１３  リテラル組
２１４  リテラル組
２２１  変数組
２２２  参照配列
２２３  リテラル組
２３１  変数組
２３２  参照配列
２３３  リテラル組
２４１  変数組
【図１】
2012003733.tif 000003
【図２】
2012003733.tif 000004
【図３】
2012003733.tif 000005