(57)【要約】      （修正有）【課題】ＣＮＦの計算複雑性の明確化やＣＮＦＳＡＴの計算を効率よく行う手段を提供する。【解決手段】ＣＮＦＳＡＴの節同士の関係を明らかにすることでＣＮＦの構造を明らかにし、潜在的な制約を顕在化することにより計算複雑性を明らかにする。また、コンピュータにこの浸出節の導出を効率的に行わせる機能を実現させるためのプログラムにより実現する。【選択図】図１
2012198865.tif 000002
【特許請求の範囲】
【請求項１】
対象ＣＮＦと、対象ＣＮＦの調和ＣＮＦが記録されたコンピュータ読み取り可能な記録媒体。
【請求項２】
請求項１において、調和ＣＮＦが調和変数組をキーとする索引あるいは冪索引のレコードとして記録された、コンピュータ読み取り可能な記録媒体。
【請求項３】
請求項１〜２いずれかの項において、同じ相関ＣＮＦを構成する全ての調和ＣＮＦを参照するデータが記録された、コンピュータ読み取り可能な記録媒体。
【請求項４】
請求項１〜３いずれかの項において、対象ＣＮＦから導出した浸出ＣＮＦの一部または全てが記録された、コンピュータ読み取り可能な記録媒体。
【請求項５】
請求項４項において、浸出ＣＮＦの一部または全てが対応する調和ＣＮＦに記録され、浸出ＣＮＦを含む調和ＣＮＦの組合せから導出した浸出ＣＮＦも浸出ＣＮＦに含めて記録された、コンピュータ読み取り可能な記録媒体。
【請求項６】
請求項４〜５いずれかの項において、対象ＣＮＦと浸出ＣＮＦの節のうち簡約可能な節が削除されて記録された、コンピュータ読み取り可能な記録媒体。
【請求項７】
請求項４〜６いずれかの項において、浸出ＣＮＦに空節が含まれる場合、対象ＣＮＦが充足不可であるということを表すデータが記録された、コンピュータ読み取り可能な記録媒体。
【請求項８】
コンピュータに下記機能を実現させるためのプログラム。
ＣＮＦのデータを受け取り、未分類ＣＮＦに追加して記録する入力機能。
未分類ＣＮＦから節を選択して対象節として抽出して未分類ＣＮＦから削除して記録し、調和変数組をキーとし調和ＣＮＦをレコードとして記録された調和ＣＮＦ冪索引を用いて対象節から調和ＣＮＦを（調和ＣＮＦ冪索引にレコードが存在しない場合は追加しながら）冪検索して抽出し、抽出した調和ＣＮＦ全てに対象節を追加して記録する分類機能。
未分類ＣＮＦの全ての節が分類機能により分類された後に、記録されている調和ＣＮＦ冪索引を出力して機能の実行を終了する出力機能。
【請求項９】
コンピュータに下記機能を実現させるためのプログラム。
ＣＮＦのデータを受け取り、未分類ＣＮＦに追加して記録する入力機能。
未分類ＣＮＦから節を選択し対象節として抽出し未分類ＣＮＦから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。
調和変数組をキーとし調和ＣＮＦをレコードとして記録された調和ＣＮＦ冪索引を用いて、対象節から調和ＣＮＦを（レコードが存在しない場合は追加しながら）冪検索し、もしも冪検索した調和ＣＮＦの中に極小調和ＣＮＦが存在しない場合、
冪検索した調和ＣＮＦを全て抽出し、
抽出した調和ＣＮＦのうち節が存在しない調和ＣＮＦに対して下記の作成機能を適用し、抽出した調和ＣＮＦに対して下記の追加機能を適用し、
対象節を極小調和ＣＮＦとする調和ＣＮＦに対して下記の削除機能を適用する検索機能。
それぞれの調和ＣＮＦに対応する相関ＣＮＦ（同じ相関ＣＮＦからなる調和ＣＮＦの集合）に、その調和ＣＮＦを追加して記録する作成機能。
それぞれの調和ＣＮＦに対して対象節を追加して記録し、同じ対象節を持つ調和ＣＮＦの集合を所属ＣＮＦとして記録する追加機能。
対象節を極小調和ＣＮＦとする調和ＣＮＦが極小調和ＣＮＦでない場合は、その調和ＣＮＦに含まれる節のうち対象節を除いた節を削除ＣＮＦとして抽出し、削除ＣＮＦのそれぞれの節について、その節の所属ＣＮＦに含まれる全ての調和ＣＮＦからその節を削除して記録する削除機能。
未分類ＣＮＦの全ての節が分類機能により分類された後に、記録されている調和ＣＮＦ冪索引を出力して機能の実行を終了する出力機能。
【請求項１０】
コンピュータに下記機能を実現させるためのプログラム。
ＣＮＦのデータを受け取り、未分類ＣＮＦに追加して記録する入力機能。
未分類ＣＮＦから節を選択し対象節として抽出し未分類ＣＮＦから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。
調和変数組をキーとし調和ＣＮＦをレコードとして記録された調和ＣＮＦ冪索引を用いて、対象節から調和ＣＮＦを（レコードが存在しない場合は追加しながら）冪検索し、もしも冪検索した調和ＣＮＦの中に極小調和ＣＮＦが存在しない場合、
冪検索した調和ＣＮＦを全て抽出し、
抽出した調和ＣＮＦのうち節が存在しない調和ＣＮＦに対して下記の作成機能を適用し、抽出した調和ＣＮＦに対して下記の追加機能を適用し、
対象節を極小調和ＣＮＦとする調和ＣＮＦに対して下記の削除機能を適用する検索機能。
それぞれの調和ＣＮＦに対応する相関ＣＮＦ（同じ相関ＣＮＦからなる調和ＣＮＦの集合）に、その調和ＣＮＦを追加して記録する作成機能。
それぞれの調和ＣＮＦに対して対象節を追加して記録し、同じ対象節を持つ調和ＣＮＦの集合を所属ＣＮＦとして記録する追加機能。
対象節を極小調和ＣＮＦとする調和ＣＮＦが極小調和ＣＮＦでない場合は、その調和ＣＮＦに含まれる節のうち対象節を除いた節を削除ＣＮＦとして抽出し、削除ＣＮＦのそれぞれの節について、その節の所属ＣＮＦに含まれる全ての調和ＣＮＦからその節を削除して記録する削除機能。
調和ＣＮＦ冪索引から、導出済ＣＮＦでない節を含む調和ＣＮＦを選択して導出ＣＮＦとして抽出し、
導出ＣＮＦと同じ相関ＣＮＦに属する調和ＣＮＦを錯綜ＣＮＦとして抽出し、
導出ＣＮＦの導出済ＣＮＦでない節全てを未導出ＣＮＦとして抽出して導出ＣＮＦから削除して記録し、
全ての錯綜ＣＮＦの導出済ＣＮＦと未導出ＣＮＦを組み合わせてできる全ての完備相関ＣＮＦから浸出ＣＮＦを構成し、
浸出ＣＮＦを未分類ＣＮＦに追加して記録し、
未導出ＣＮＦを導出ＣＮＦの導出済ＣＮＦに追加して記録し、
浸出ＣＮＦに空節が含まれるかどうかを出力する導出機能。
もし導出機能が充足不可であることを記録した場合は充足不可であることを出力して機能の実行を終了し、あるいは未分類ＣＮＦの全ての節が分類機能により分類されて全ての調和ＣＮＦの全ての節が導出済ＣＮＦとして記録された場合は、充足可能であることを出力して機能の実行を終了する出力機能。
【請求項１１】
請求項１０において、下記の機能が追加されたプログラム。
追加機能にて、調和ＣＮＦに対象節を追加する際に、その調和ＣＮＦを未導出調和ＣＮＦ集合に追加する。
導出機能にて、未導出ＣＮＦを含む調和ＣＮＦを選択する際に、未導出調和ＣＮＦ集合から調和ＣＮＦを選択して導出ＣＮＦとして抽出して未導出調和ＣＮＦ集合から削除して記録する。
【請求項１２】
請求項１０〜１１いずれかの項において、出力機能が充足可能であることを出力する際に、調和ＣＮＦ冪索引のレコードから不備相関ＣＮＦを構成し、その不備相関ＣＮＦに含まれない極小調和ＣＮＦを全て偽とする真理値割当を集めて出力する機能が追加されたプログラム。
【請求項１３】
請求項１０〜１２いずれかの項において、出力機能が出力する際に、記録されている調和ＣＮＦ冪索引も出力する機能が追加されたプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】本発明は、ＣＮＦの節同士の関係を表すデータ構造、及びコンピュータにてＣＮＦの節同士の関係を表すデータを構成するプログラム、及びＣＮＦＳＡＴを計算するプログラムに関する
【背景技術】
【０００２】従来、コンピュータでは様々な問題が扱われており、また論理式や充足可能性問題、恒真式問題など論理に関する問題も様々なものが扱われている。【０００３】例えばＳＡＴ（充足可能性問題）は、ＮＰ完全問題というコンピュータの論理的概念よりも強い問題であり、その応用範囲も広い。特にＣＮＦ（乗法標準形）で構成されたＣＮＦＳＡＴと呼ばれるＳＡＴの一種は、ＳＡＴから多項式時間で変換可能（例えば非特許文献１参照）でありながらも、変換後の取り扱いが容易となる。そのため、様々な問題がＣＮＦＳＡＴに変換されてから計算されている。【０００４】しかし、ＣＮＦＳＡＴは本質的にコンピュータで計算するのが困難な問題であり、判定するのに実質不可能な指数時間が必要になることがある。その計算複雑性はＣＮＦの構造の複雑さにより決まる。よってＣＮＦＳＡＴをＣＮＦの構造の観点から整理することは、ＣＮＦＳＡＴを効率的に計算するために重要となる。【０００５】しかし、今まではＣＮＦＳＡＴの計算複雑性をＣＮＦの構造を用いて整理・抽出したデータ構造は存在しなかった。また上記データ構造をＣＮＦＳＡＴから構成する計算手法も、上記データ構造を用いてＣＮＦＳＡＴを計算する手法も存在しなかった。【０００６】また、複数の論理式から新たな論理式を構成する導出という演繹方法が存在する。導出とは２つの節から制約条件を変えずに追加可能な１つの節を導き出す操作である。片方の節にＡ∨Ｐという命題があり、もう片方に¬Ａ∨Ｑという命題がある時、両方の命題が同時に成立するときはＰ∨Ｑという命題も存在することを導き出す操作である。導出を用いることによって、ＣＮＦに含まれる命題を導き出して充足可否を求めることも可能である。また、この導出やその他の論理式を削除する手法をまとめたＤＬＰＰというアルゴリズムも存在する。【０００７】しかし、導出やＤＰＬＬアルゴリズムはある２つの命題の肯定と否定を組合せて別の命題を顕在化する操作であり、ＣＮＦのような様々なリテラルの肯定・否定が入れ混じる論理式で導出を行うのは計算の効率が悪かった。
【先行技術文献】
【０００８】
【非特許文献１】「オートマトン  言語理論  計算論  ＩＩ」Ｊ．ホップクロフト，Ｊ．ウルマン，Ｒ．モトワニ  サイエンス社  ２００８年  Ｐ１４７−１５５
【発明の概要】
【発明が解決しようとする課題】
【０００９】本発明の解決しようとする課題は、ＣＮＦＳＡＴの計算複雑性をＣＮＦの構造から整理・抽出したデータ構造を提供する点にある。また上記データ構造をＣＮＦＳＡＴから効率良く構成する機能をコンピュータで実現させるためのプログラムを提供する点にある。また、上記データ構造を用いてＣＮＦＳＡＴを効率良く計算する機能をコンピュータで実現させるためのプログラムを提供する点にある。
【課題を解決するための手段】
【００１０】まず、本発明で使用する用語を説明する。本発明では肯定リテラルを肯定変数、否定リテラルを否定変数、リテラルを肯否変数、リテラルを意識しない（肯否を無視する）場合は単に変数と呼ぶ。また、単数または複数の変数の組合せを変数組、変数組に含まれる変数の部分集合となる変数組を部分変数組と呼ぶ。【００１１】また、あるＣＮＦの節の部分集合からなるＣＮＦを部分ＣＮＦと呼ぶ。【００１２】また、ＣＮＦのある節と他の節の両方に含まれる変数の一部または全てを集めた変数組を相関変数組と呼ぶ。ある変数の組合せを含む節が複数存在しない場合でも、その変数の組合せを相関変数組と呼ぶことがある。また、相関変数組の部分変数組を部分相関変数組と呼ぶ。なお、簡単のため、相関変数組と部分相関変数組を合わせて単に相関変数組と呼ぶことがある。同じ相関変数組の節を全て集めたＣＮＦを相関ＣＮＦと呼ぶ。なお、相関ＣＮＦには対になる相関変数組が存在する。【００１３】また肯定変数・否定変数・肯否変数についても、それぞれの変数組や相関変数組を、肯定変数組・否定変数組・肯否変数組、肯定相関変数組・否定相関変数組・肯否相関変数組と呼ぶ。また、節に含まれる変数から相関変数組に含まれる変数を除いた変数組を分離変数組と呼ぶ。分離変数組についても同様に、それぞれの肯定変数・否定変数・肯否変数を肯定分離変数組・否定分離変数組・肯否分離変数組と呼ぶ。また、ある節の相関変数組の部分を相関部、分離変数組の部分を分離部と呼ぶ。また、同じ相関変数組を含む節同士の関係を相関関係と呼ぶ。【００１４】また相関関係のうち、肯否相関変数組の一致する関係を調和関係と呼び、肯否相関変数組の異なる関係を錯綜関係と呼ぶ。同様に相関〜〜と呼ぶものについて、肯否相関変数組の一致するものを調和〜〜、異なるものを錯綜〜〜と呼ぶ。【００１５】また、相関ＣＮＦのうち、お互いに調和関係にある節で構成されるＣＮＦを調和ＣＮＦと呼ぶ。また、ある調和ＣＮＦと錯綜関係にある単数あるいは複数の調和ＣＮＦで構成されるＣＮＦを調和ＣＮＦの錯綜ＣＮＦと呼ぶ。【００１６】また、ある節について、その節を含む調和ＣＮＦを所属ＣＮＦと呼ぶ。【００１７】また、調和ＣＮＦと対になる肯否相関変数組を、特に調和変数組と呼ぶ。【００１８】なお、調和ＣＮＦのうち、その調和ＣＮＦの調和変数組のみで構成されている節のみからなる調和ＣＮＦを極小調和ＣＮＦと呼ぶ。極小調和ＣＮＦは、そのＣＮＦに調和ＣＮＦの条件を満たすどのような節を追加したとしても、簡約律によりただ一つの節になる調和ＣＮＦである。例えば｛Ｘ，¬Ｙ，¬Ｚ｝が調和変数組となる極小調和ＣＮＦは（Ｘ∨¬Ｙ∨¬Ｚ）となる。｛Ｘ，¬Ｙ，¬Ｚ｝を調和変数組とする調和ＣＮＦは（Ｘ∨¬Ｙ∨¬Ｚ∨……）のように｛Ｘ，¬Ｙ，¬Ｚ｝を含む任意の節で構成することができる。しかし極小調和ＣＮＦは（Ｘ∨¬Ｙ∨¬Ｚ）を含むため、調和ＣＮＦの節を全てこの節に簡約することができる。なお、コンピュータでの取り扱いを容易にするため、極小調和ＣＮＦに調和ＣＮＦの節を追加した（簡約化前の）ＣＮＦは極小調和ＣＮＦとは呼ばないこととする（簡約化により極小調和ＣＮＦに変形することはできる）。【００１９】ある相関ＣＮＦを考える。その相関ＣＮＦの相関変数組の取り得る肯否相関変数組それぞれについて調和ＣＮＦが存在するとする。この時、それぞれの調和ＣＮＦから１つずつ節を取り出して構成したＣＮＦを相関ＣＮＦの完備相関ＣＮＦと呼ぶ。つまり、完備相関ＣＮＦはその相関関係について互いに錯綜関係となる節のみを集めた、全ての錯綜関係が存在するＣＮＦである。【００２０】また完備相関ＣＮＦの各節から、その相関変数組の分離肯否変数を集めた節を浸出節と呼ぶ。完備相関ＣＮＦは、どの真理値割当でもいずれかの節の相関部が必ず偽となる。よって、完備相関ＣＮＦを含むＣＮＦにおいて浸出部が充足不可の場合は、ＣＮＦ全体も充足不可となる。つまり、完備相関ＣＮＦには浸出節で表される潜在的な制約が存在し、浸出節を導くことにより顕在化することができる。本発明では完備相関ＣＮＦ〜浸出節を導く操作を相関導出、あるいは単に導出と呼ぶ。相関導出は導出の拡張であり、相関変数組が変数１つの場合は導出と同じ操作となる。【００２１】完備相関ＣＮＦから任意の節を取り除いたＣＮＦを不備相関ＣＮＦと呼ぶ。不備相関ＣＮＦからは完備相関ＣＮＦを構成することができない。また完備相関ＣＮＦに、相関変数組が同じだが完備相関ＣＮＦに含まれない節を追加したＣＮＦを過剰相関ＣＮＦと呼ぶ。過剰相関ＣＮＦからは複数の完備相関ＣＮＦを構成することができる。それぞれの調和ＣＮＦからいずれか１つの節を選択して組合せたＣＮＦは完備相関ＣＮＦとなる。【００２２】なお、ある相関ＣＮＦで複数種類の完備相関ＣＮＦが構成可能な場合、それぞれの完備相関ＣＮＦからそれぞれ異なる浸出節を導出することができる。つまり、過剰相関ＣＮＦには複数の完備相関ＣＮＦが畳み込まれていると言う事ができる。ここで、ある相関ＣＮＦの取り得る全ての完備相関ＣＮＦの浸出節を合わせたＣＮＦを（相関ＣＮＦの）浸出ＣＮＦと呼ぶ。なお簡単のため、単独の浸出節も浸出ＣＮＦと呼ぶ。複数の相関ＣＮＦについての浸出ＣＮＦを組み合わせたＣＮＦもまた浸出ＣＮＦと呼ぶことがある。【００２３】ここで具体例として３ＣＮＦを考える。肯否変数をＡ、Ｂ、Ｃ、Ｄとした時に、次の３ＣＮＦの相関ＣＮＦ｛Ｘ｝を考える。（Ａ∨Ｂ∨Ｘ）∧（Ｃ∨Ｄ∨¬Ｘ）【００２４】この３ＣＮＦは相関変数組｛Ｘ｝の完備相関ＣＮＦとなり、浸出節（Ａ∨Ｂ∨Ｃ∨Ｄ）を導出することができる。【００２５】次に、上記の３ＣＮＦに節を追加した下記の相関ＣＮＦ｛Ｘ｝を考える。
（Ａ∨Ｂ∨Ｘ）∧（Ａ∨Ｃ∨Ｘ）∧（Ｃ∨Ｄ∨¬Ｘ）∧（Ｂ∨Ｄ∨¬Ｘ）【００２６】この相関ＣＮＦ｛Ｘ｝は、同じ調和ＣＮＦから１つずつ選択した組合せそれぞれの完備相関ＣＮＦを考えることができる。つまり下記の４通りとなる。
（Ａ∨Ｂ∨Ｘ）∧（Ｃ∨Ｄ∨¬Ｘ）、（Ａ∨Ｂ∨Ｘ）∧（Ｂ∨Ｄ∨¬Ｘ）、（Ａ∨Ｃ∨Ｘ）∧（Ｃ∨Ｄ∨¬Ｘ）、（Ａ∨Ｃ∨Ｘ）∧（Ｂ∨Ｄ∨¬Ｘ）【００２７】また、上記の完備相関ＣＮＦそれぞれについて浸出節が存在するため、この相関ＣＮＦ｛Ｘ｝の浸出ＣＮＦは次のようになる。
（Ａ∨Ｂ∨Ｃ∨Ｄ）∧（Ａ∨Ｂ∨Ｄ）∧（Ａ∨Ｃ∨Ｄ）∧（Ａ∨Ｃ∨Ｂ∨Ｄ）【００２８】この関係は相関変数組の変数が２つの３ＣＮＦの場合も同様となる。例えば、肯否変数をＡ、Ｂ、Ｃ、Ｄとした時に、下記の相関ＣＮＦ｛Ｘ，Ｙ｝を考える。
（Ａ∨Ｘ∨Ｙ）∧（Ｂ∨¬Ｘ∨Ｙ）∧（Ｃ∨Ｘ∨¬Ｙ）∧（Ｄ∨¬Ｘ∨¬Ｙ）【００２９】この３ＣＮＦは相関変数組｛Ｘ，Ｙ｝の完備相関ＣＮＦとなり、浸出節（Ａ∨Ｂ∨Ｃ∨Ｄ）を導出することができる。【００３０】同じ肯否相関変数組が存在する場合も同様となる。Ｅを肯否変数とする次の相関ＣＮＦ｛Ｘ，Ｙ｝を考える。Ａを含む節とＥを含む節が同じ調和ＣＮＦとなる。
（Ａ∨Ｘ∨Ｙ）∧（Ｂ∨¬Ｘ∨Ｙ）∧（Ｃ∨Ｘ∨¬Ｙ）∧（Ｄ∨¬Ｘ∨¬Ｙ）∧（Ｅ∨Ｘ∨Ｙ）【００３１】この相関ＣＮＦ｛Ｘ，Ｙ｝でも、同じ調和ＣＮＦから１つずつ節を選択した組合せそれぞれの完備相関ＣＮＦを考えることができる。つまり下記の２通りとなる。
（Ａ∨Ｘ∨Ｙ）∧（Ｂ∨¬Ｘ∨Ｙ）∧（Ｃ∨Ｘ∨¬Ｙ）∧（Ｄ∨¬Ｘ∨¬Ｙ）、（Ｅ∨Ｘ∨Ｙ）∧（Ｂ∨¬Ｘ∨Ｙ）∧（Ｃ∨Ｘ∨¬Ｙ）∧（Ｄ∨¬Ｘ∨¬Ｙ）【００３２】そして、上記の完備相関ＣＮＦそれぞれについて浸出節が存在するため、相関ＣＮＦ｛Ｘ，Ｙ｝の浸出ＣＮＦは次のようになる。
（Ａ∨Ｂ∨Ｃ∨Ｄ）∧（Ｅ∨Ｂ∨Ｃ∨Ｄ）【００３３】また、上記の場合、相関変数組｛Ｘ，Ｙ｝だけではなく、その部分集合の相関変数組｛Ｘ｝｛Ｙ｝も同様に相関ＣＮＦを考えることができる。相関ＣＮＦ｛Ｘ｝｛Ｙ｝の浸出ＣＮＦの組み合わせでも上記結果を導くことが可能だが、単に相関ＣＮＦ｛Ｘ，Ｙ｝の浸出ＣＮＦの構成を優先する場合は、相関導出の方が効率良く計算できる。【００３４】この延長線として、節の変数全てが相関変数組となる相関ＣＮＦを考えることもできる。ただし、この場合は分離部が存在しないため、空節を導出することに注意する必要がある。例えば、下記の３ＣＮＦの相関ＣＮＦ｛Ｘ，Ｙ，Ｚ｝を考える。
（Ｘ∨Ｙ∨Ｚ）∧（¬Ｘ∨Ｙ∨Ｚ）∧（Ｘ∨¬Ｙ∨Ｚ）∧（Ｘ∨Ｙ∨¬Ｚ）∧（Ｘ∨¬Ｙ∨¬Ｚ）∧（¬Ｘ∨Ｙ∨¬Ｚ）∧（¬Ｘ∨¬Ｙ∨Ｚ）∧（¬Ｘ∨¬Ｙ∨¬Ｚ）【００３５】この相関ＣＮＦ｛Ｘ，Ｙ，Ｚ｝には、全ての肯否相関変数組に対応する節が存在し、完備相関ＣＮＦとなる。しかし分離部が存在しないため浸出節は空節となる。つまり、このＣＮＦは真になることができず充足不可となる。【００３６】なお、上記の関係は３ＣＮＦに限定されず、ＣＮＦ一般について成り立つ。【００３７】また、既に全ての浸出ＣＮＦを導出しているＣＮＦを導出済ＣＮＦと呼ぶ。これは相関ＣＮＦの部分ＣＮＦも同様とする。つまり、ある相関ＣＮＦの部分ＣＮＦのうち、その部分ＣＮＦの範囲では全ての浸出ＣＮＦを導出している部分ＣＮＦも相関ＣＮＦの導出済ＣＮＦと呼ぶ。なお、相関ＣＮＦの導出済ＣＮＦ以外の部分ＣＮＦを未導出ＣＮＦと呼ぶことがある。導出済ＣＮＦと未導出ＣＮＦの節を組み合せることにより、新たに浸出ＣＮＦを導出できる場合がある。【００３８】なお本発明では、ＣＮＦや節、変数を表すデータは従来のコンピュータで用いられるデータとする。バイナリ列や配列、テーブル、レコード、構造体などのデータとする場合や、変数の区切りを空白とし節の区切りを改行としたテキストデータとする場合もある。また変数番号の偶数奇数で変数の肯定否定を定める場合もある。あるいはＣＮＦや節、変数の省略形を表すデータ構造などの場合もある。またＣＮＦや節、変数を表すデータ構造が他に存在し、そのデータへの参照によってＣＮＦや節、変数を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。【００３９】また、節を表すデータとして、その節に含まれる肯否変数への参照などのデータを集めたデータを用いる場合もある。同様に、ＣＮＦを表すデータとして、ＣＮＦを構成する節への参照などのデータを集めたデータを用いる場合もある。【００４０】また、ＣＮＦを表すデータに、そのＣＮＦの特徴を表すデータを含める場合がある。例えば相関ＣＮＦが、その相関ＣＮＦに対応する相関変数組を含む場合がある。また相関ＣＮＦが、その相関ＣＮＦに含まれる調和ＣＮＦのデータを含む場合がある。調和ＣＮＦが、その調和ＣＮＦの錯綜ＣＮＦとなる調和ＣＮＦへの参照を含む場合がある。あるいは調和ＣＮＦが、その調和ＣＮＦを含む相関ＣＮＦへの参照を含む場合がある。また、節が所属する相関ＣＮＦや調和ＣＮＦへの参照を含む場合がある。【００４１】また、ＣＮＦを表すデータに、そのＣＮＦのある性質を持つＣＮＦが区別されて記録されている場合がある。例えば調和ＣＮＦのうち、その相関ＣＮＦにおける導出済ＣＮＦと未導出ＣＮＦがそれぞれわかるように記録されていることがある。【００４２】また後述のように調和ＣＮＦに分類される前の節と分類された後の節を、それぞれわかるように別々に記録することがある。【００４３】このようにＣＮＦや節、変数のデータ構造は様々なものがあるが、ＣＮＦや節、変数を特定し他と区別できるデータであれば良く、これらに限定されない。【００４４】また変数組を表すデータは従来のコンピュータで変数の組合せを表すのに用いられるものとする。バイナリ列や配列、テーブル、レコード、構造体などのデータとする場合や、変数の区切りを空白としたテキストデータとする場合もある。また変数組を表すデータが他に存在し、そのデータへの参照によって変数組を表すこともある。この場合のデータへの参照は通常のデータ構造で参照として用いられるデータとなる。例えばデータへのポインタやアドレスの場合がある。あるいはデータが配列やレコードの場合は、その配列やレコードの要素を特定する添字やタグの場合もある。また前述のＣＮＦや節、変数との組合せで用いるデータとする場合もある。例えばＣＮＦや節、変数を表すデータへの参照などである。参照はポインタやアドレスの場合もある。またＣＮＦが配列やレコードの時は、その配列やレコードの要素を特定する添字やタグの場合もある。このように変数組を表す様々なデータ構造があるが、変数の組合せを表すデータ構造であれば良く、上記の例に限定されない。【００４５】また、データの集合を表すデータも同様に、従来のコンピュータで複数のデータを表す方法として用いられるデータとする。配列やリスト、リンクリスト、循環リスト、テーブル、レコード、構造体、テキストデータなどがあるが、複数のデータをまとめて表すデータ（集合を表すデータ）であれば良く、これらに限定されない。【００４６】なお、本発明において索引のデータを使用する場合があるが、その索引のデータは従来のコンピュータでキーからレコードを検索する時に使用する索引のデータとする。例えばＢ木（Ｂ＋木、Ｂ＊木）や２分探索木、ハッシュ索引、トライ木、パトリシア木などである。このように索引のデータ構造は様々なものがあるが、キーとなるデータからレコードとなるデータを検索することのできる索引のデータとなっていれば良く、これらに限定されない。【００４７】また、同様に本発明において、あるキーとなるデータから、そのキーの全ての部分集合をキーとするレコードを全て検索する時に使用する索引を用意する場合がある。この索引を特に冪索引と呼ぶ。また、冪索引から対応するレコード全てを検索することを冪検索と呼ぶ。例えば、相関肯否変数組をキーとする冪索引があるとする。この冪索引で｛Ｘ，Ｙ，Ｚ｝という相関肯否変数組をキーとして冪検索した場合、その結果は｛Ｘ，Ｙ，Ｚ｝の部分相関肯否変数組をキーとする検索結果、すなわち｛Ｘ，Ｙ，Ｚ｝｛Ｙ，Ｚ｝｛Ｘ，Ｚ｝｛Ｘ，Ｙ｝｛Ｘ｝｛Ｙ｝｛Ｚ｝をキーとする検索結果のレコード全ての集合となる（なお、｛｝をキーとする検索結果を含む場合もある）。【００４８】この冪索引のデータを構成する方法はいくつか存在する。例えば、｛Ｘ，Ｙ，Ｚ｝に対応するレコードに｛Ｘ，Ｙ，Ｚ｝の部分集合のレコード全てを含むようにする場合である。なおこの場合、レコードの重複を避けるため、対応するレコードは全て参照としてデータそのものとは別に保存する場合がある。また、レコードを階層的に持つことで効率化することがある。例えば、あるキーのレコードは、そのキーの部分集合をキーとするレコードを参照として持つ場合である。【００４９】また、冪索引として通常の索引と同様のデータ構造を使用し、冪検索する時の検索方法を工夫することで対応する場合がある。例えば、データ構造として検索木を使用する場合、キーの部分集合を列挙しながら検索を行うことで冪検索を実現する場合がある。たとえはキーの部分集合を、その有無がグレイコードの順番になるように並べた順番で検索する場合や、キーを辞書順に並べた順番で検索するなどの検索方法である。こうすることで、同じ検索経路となるキーを集中して検索することができる。その結果、冪索引の冪検索で、検索木の同じ経路を辿ることなく効率的に対象を網羅することができる。【００５０】このように冪索引の冪検索を実現するデータ構造・機能は様々なものが存在するが、あるキーからそのキーの部分集合をキーとする全てのレコードの集合を検索できれば良く、これらに限定されない。【００５１】また、集合から要素を選択する機能を使用することがあるが、コンピュータに選択する機能を実現させるためのプログラムは従来のプログラムで用いられるものとする。例えば要素を辞書順に並べた順番に選択する、要素の大きさの大きい順、または要素の大きさの小さい順に選択する、先に追加された要素から選択する、後に追加された要素から選択する、集合からランダムに選択する、などである。なお、ＣＮＦからある節を選択する、節からある変数を選択する、冪索引の全てのレコードから１つのレコードを選択する、なども同様とする。【００５２】また、本発明で用いるそれぞれの構成要素は、メモリ等の記憶手段やコンピュータ読み取り可能な記録媒体に記録・記憶され、コンピュータのデータとして活用される。なお、表記の簡単化のため、メモリ等の記憶手段に記録されたデータを、ＣＮＦや節、変数、変数組、索引、冪索引、集合、要素、あるいはそれらへの参照、などのように、そのまま表記することがある。【００５３】これより本発明の説明を行う。【００５４】上記問題を解決するため、本発明では、対象となるＣＮＦと、その対象となるＣＮＦの調和ＣＮＦが記録されたコンピュータ読み取り可能な記録媒体とした。【００５５】なお、本発明では、この対象となるＣＮＦを対象ＣＮＦと呼ぶ。対象ＣＮＦは任意のＣＮＦであり、全てのＣＮＦが対象ＣＮＦになることができる。【００５６】つまり、上記は対象ＣＮＦの構造を調和関係で整理したデータとなる。ＣＮＦの節はお互いに調和関係にある節同士の関係で全体の構造を構成する。そのため、ＣＮＦの調和関係を整理することで、その構造の複雑性を明らかにすることができる。【００５７】なお、上記の調和ＣＮＦは、対象ＣＮＦの節への参照の集合となることがある。調和ＣＮＦに含まれる節は対象ＣＮＦに含まれるため、調和ＣＮＦの節を参照で表すことで節を繰り返し記録する必要が無くなり、記憶領域を節約することができる。【００５８】また上記の調和ＣＮＦが、その調和ＣＮＦの調和変数組のデータを含んで記録されている場合がある。こうすることで、その調和ＣＮＦの調和変数組が何かを容易に判定することができる。【００５９】また上記の調和ＣＮＦと調和変数組が、調和変数組をキーとして調和ＣＮＦをレコードとする索引、あるいは冪索引として記録されている場合がある。こうすることで、ある調和変数組に対応する調和ＣＮＦを容易に検索できるようになる。【００６０】また上記において、同じ相関ＣＮＦを構成する全ての調和ＣＮＦを参照するデータが記録されている場合がある。例えば、同じ相関ＣＮＦとなる調和ＣＮＦ同士が循環リストによって環状に参照しており、その参照を辿ることで、同じ相関ＣＮＦの他の調和ＣＮＦ（すなわち錯綜ＣＮＦ）全てを参照することができるようになっていることがある。あるいは、相関ＣＮＦとなるデータが存在し、その相関ＣＮＦと調和ＣＮＦの相互参照が含まれる場合がある。こうすることで、相関ＣＮＦから浸出ＣＮＦを構成するときに完備相関ＣＮＦを構成するのを効率的に行えるようになる。【００６１】また上記のコンピュータ読み取り可能な記録媒体に記録されたデータが、上記の相関ＣＮＦの一部または全ての浸出ＣＮＦを含んで記録されている場合がある。浸出ＣＮＦは相関ＣＮＦの潜在的な制約であり、対象ＣＮＦに導出した浸出ＣＮＦを追加したとしてもその充足可否は変わらない。よって潜在的な制約を浸出ＣＮＦとして顕在化することで、対象ＣＮＦの充足可否を変えずに、その対象ＣＮＦの計算複雑性を明らかにすることができる。なお、浸出ＣＮＦは対象ＣＮＦと同様のデータとして記録されている。【００６２】また上記のコンピュータ読み取り可能な記録媒体に記録されたデータにおいて、上記の浸出ＣＮＦの一部あるいは全ての節が対応する調和ＣＮＦに記録されている場合がある。なお、浸出ＣＮＦを含む調和ＣＮＦを組合せた相関ＣＮＦから新たに異なる浸出ＣＮＦが導出できる場合は、その新たに導出した浸出ＣＮＦも元の浸出ＣＮＦに含めて記録されている。こうすることで浸出ＣＮＦによる潜在的な制約をさらに顕在化することができ、対象ＣＮＦの構造をさらに詳細に明確化することができる。【００６３】なお上記の調和ＣＮＦにて、調和ＣＮＦに含まれるＣＮＦのうち、いずれかの節が他の節を簡約律により簡約可能な場合、そのＣＮＦでは複数の節がその簡約した節に置き換わって記録されている場合がある。このようにすることで調和ＣＮＦの構成をＣＮＦの充足可否を変えずに簡素化することができる。【００６４】また、調和ＣＮＦと調和ＣＮＦに含まれる節がお互いに参照可能となっていることがある。例えば調和ＣＮＦが対象ＣＮＦの節との双方向参照の集合となっており、対象ＣＮＦの節から全ての調和ＣＮＦを参照することができるようになっていることがある。このようにすることで、ある簡約可能な節が複数の調和ＣＮＦに含まれる場合でも効率的に簡約することができる。【００６５】また、上記の浸出ＣＮＦに空節が含まれる場合は、対象ＣＮＦが充足不可だということを表すデータが上記のコンピュータ読み取り可能な記録媒体に含まれて記録されている場合がある。こうすることで、全ての浸出ＣＮＦの節を確認することなく、対象ＣＮＦが充足不可であることを判定することができる。【００６６】また上記問題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
ＣＮＦのデータを受け取り、未分類ＣＮＦに追加して記録する入力機能。
未分類ＣＮＦから節を選択して対象節として抽出して未分類ＣＮＦから削除して記録し、調和変数組をキーとし調和ＣＮＦをレコードとして記録された調和ＣＮＦ冪索引を用いて対象節から調和ＣＮＦを（調和ＣＮＦ冪索引にレコードが存在しない場合は追加しながら）冪検索して抽出し、抽出した調和ＣＮＦ全てに対象節を追加して記録する分類機能。
未分類ＣＮＦの全ての節が分類機能により分類された後に、記録されている調和ＣＮＦ冪索引を出力して機能の実行を終了する出力機能。【００６７】プログラムをこのような構成とすることで、コンピュータにＣＮＦＳＡＴの計算複雑性を表す調和ＣＮＦを構成させることができるようになる。【００６８】また上記問題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
ＣＮＦのデータを受け取り、未分類ＣＮＦに追加して記録する入力機能。
未分類ＣＮＦから節を選択し対象節として抽出し未分類ＣＮＦから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。
調和変数組をキーとし調和ＣＮＦをレコードとして記録された調和ＣＮＦ冪索引を用いて、対象節から調和ＣＮＦを（レコードが存在しない場合は追加しながら）冪検索し、もしも冪検索した調和ＣＮＦの中に極小調和ＣＮＦが存在しない場合、
冪検索した調和ＣＮＦを全て抽出し、
抽出した調和ＣＮＦのうち節が存在しない調和ＣＮＦに対して下記の作成機能を適用し、抽出した調和ＣＮＦに対して下記の追加機能を適用し、
対象節を極小調和ＣＮＦとする調和ＣＮＦに対して下記の削除機能を適用する検索機能。
それぞれの調和ＣＮＦに対応する相関ＣＮＦ（同じ相関ＣＮＦからなる調和ＣＮＦの集合）に、その調和ＣＮＦを追加して記録する作成機能。
それぞれの調和ＣＮＦに対して対象節を追加して記録し、同じ対象節を持つ調和ＣＮＦの集合を所属ＣＮＦとして記録する追加機能。
対象節を極小調和ＣＮＦとする調和ＣＮＦが極小調和ＣＮＦでない場合は、その調和ＣＮＦに含まれる節のうち対象節を除いた節を削除ＣＮＦとして抽出し、削除ＣＮＦのそれぞれの節について、その節の所属ＣＮＦに含まれる全ての調和ＣＮＦからその節を削除して記録する削除機能。
未分類ＣＮＦの全ての節が分類機能により分類された後に、記録されている調和ＣＮＦ冪索引を出力して機能の実行を終了する出力機能。【００６９】プログラムをこのような構成とすることで、コンピュータに浸出ＣＮＦを構成する時に必要となる調和ＣＮＦを構成させることができるようになる。さらに、調和ＣＮＦを構成している時に、並行して簡約律による簡約化を行うため、より効率良く実行することができる。また同じ相関ＣＮＦとなる調和ＣＮＦ同士の集合を構成することにより、浸出ＣＮＦを構成するのが容易となる。【００７０】なお、作成機能により作成される相関ＣＮＦは、前述の様々な集合とすることができるが、特に索引と循環リストが重要となる。索引は、同じ相関ＣＮＦ毎に作成した、相関変数組をキーとして調和ＣＮＦの集合をレコードとするものである。循環リストは、同じ相関ＣＮＦとなる調和ＣＮＦ同士を循環リストで接続したものである。【００７１】索引の場合、調和ＣＮＦに参照などを追加することなく、調和ＣＮＦの集合を調和ＣＮＦ自体から切り離して用意することができる。そのため、調和ＣＮＦへの影響を最小限に抑えながらデータ構造を実現することができる。【００７２】循環リストの場合、調和ＣＮＦに循環リストのデータ構造を用意する必要があるが、同じ調和ＣＮＦを検索するための索引を調和ＣＮＦ冪索引と共用することができ（例えば肯定相関変数のみの調和ＣＮＦを相関ＣＮＦの代表とすることにより、共用を実現できる）、データの大きさを効率化することができる。【００７３】また追加機能により記録される所属ＣＮＦの集合も、前述の様々な集合とすることができる。特に索引と双方向参照が重要となる。索引は、同じ節毎に作成した、調和変数組をキーとして調和ＣＮＦの集合をレコードとするものである。双方向参照は、対象節と所属ＣＮＦの参照をそれぞれの節・ＣＮＦに記録したものである。【００７４】索引の場合、対象節に参照などを追加することなく、調和ＣＮＦの集合を対象節から切り離して用意することができる。そのため、対象節への影響を最小限に抑えながらデータ構造を実現することができる。【００７５】双方向参照の場合、その整合性の維持をどのように行うかを考える必要がある。例えば、同じ対象節は唯一のデータとなるように記録し、調和ＣＮＦはそのデータへの参照として記録するなどを行い、双方向参照の整合性を保ち易くする工夫が必要となる。【００７６】また上記問題を解決するため、本発明では、コンピュータに下記機能を実現させるためのプログラムとした。
ＣＮＦのデータを受け取り、未分類ＣＮＦに追加して記録する入力機能。
未分類ＣＮＦから節を選択し対象節として抽出し未分類ＣＮＦから削除して記録し、抽出した対象節に対して下記の検索機能を適用する分類機能。
調和変数組をキーとし調和ＣＮＦをレコードとして記録された調和ＣＮＦ冪索引を用いて、対象節から調和ＣＮＦを（レコードが存在しない場合は追加しながら）冪検索し、もしも冪検索した調和ＣＮＦの中に極小調和ＣＮＦが存在しない場合、
冪検索した調和ＣＮＦを全て抽出し、
抽出した調和ＣＮＦのうち節が存在しない調和ＣＮＦに対して下記の作成機能を適用し、抽出した調和ＣＮＦに対して下記の追加機能を適用し、
対象節を極小調和ＣＮＦとする調和ＣＮＦに対して下記の削除機能を適用する検索機能。
それぞれの調和ＣＮＦに対応する相関ＣＮＦ（同じ相関ＣＮＦからなる調和ＣＮＦの集合）に、その調和ＣＮＦを追加して記録する作成機能。
それぞれの調和ＣＮＦに対して対象節を追加して記録し、同じ対象節を持つ調和ＣＮＦの集合を所属ＣＮＦとして記録する追加機能。
対象節を極小調和ＣＮＦとする調和ＣＮＦが極小調和ＣＮＦでない場合は、その調和ＣＮＦに含まれる節のうち対象節を除いた節を削除ＣＮＦとして抽出し、削除ＣＮＦのそれぞれの節について、その節の所属ＣＮＦに含まれる全ての調和ＣＮＦからその節を削除して記録する削除機能。
調和ＣＮＦ冪索引から、導出済ＣＮＦでない節を含む調和ＣＮＦを選択して導出ＣＮＦとして抽出し、
導出ＣＮＦと同じ相関ＣＮＦに属する調和ＣＮＦを錯綜ＣＮＦとして抽出し、
導出ＣＮＦの導出済ＣＮＦでない節全てを未導出ＣＮＦとして抽出して導出ＣＮＦから削除して記録し、
全ての錯綜ＣＮＦの導出済ＣＮＦと未導出ＣＮＦを組み合わせてできる全ての完備相関ＣＮＦから浸出ＣＮＦを構成し、
浸出ＣＮＦを未分類ＣＮＦに追加して記録し、
未導出ＣＮＦを導出ＣＮＦの導出済ＣＮＦに追加して記録し、
浸出ＣＮＦに空節が含まれるかどうかを出力する導出機能。
もし導出機能が空節を含むと出力した場合は充足不可であることを出力して機能の実行を終了し、あるいは未分類ＣＮＦの全ての節が分類機能により分類されて全ての調和ＣＮＦの全ての節が導出済ＣＮＦとして記録された場合は、充足可能であることを出力して機能の実行を終了する出力機能。【００７７】プログラムをこのような構成とすることで、ＣＮＦの潜在的な制約を顕在化し、ＣＮＦの充足可否を判定することができる。【００７８】プログラムをこのような構成とすることで、コンピュータにＣＮＦの潜在的な制約を顕在化させて、ＣＮＦの充足可否を判定させることができるようになる。【００７９】なお、導出機能による浸出ＣＮＦの構成を効率化するために、導出済ＣＮＦでない節を含む調和ＣＮＦを識別可能なようにすることがある。具体的には下記の通り機能を追加する。なお、ここの未導出調和ＣＮＦ集合とは、導出済ＣＮＦでない節を含む調和ＣＮＦを集めた集合である。追加機能にて、調和ＣＮＦに対象節を追加する際に、その調和ＣＮＦを未導出調和ＣＮＦ集合として記録する機能を追加する。導出機能にて、未導出ＣＮＦを含む調和ＣＮＦを選択する際に、未導出調和ＣＮＦ集合から選択して導出ＣＮＦとして抽出して未導出調和ＣＮＦ集合から削除して記録する機能を追加する。このようにすることで、導出機能が全て導出済ＣＮＦとなっている調和ＣＮＦを選択することが無くなり、効率化することができる。【００８０】なお、本プログラムによる機能は容易に並列化することができる。まず分類機能と導出機能はお互いに影響を与えないで機能させることが可能である。未分類ＣＮＦと未導出ＣＮＦがそれぞれの機能のインターフェイスとなる。しかし、分類機能は未分類ＣＮＦから節を削除して未導出ＣＮＦに節を追加するのみ、導出機能は未導出ＣＮＦから節を削除して未分類ＣＮＦに節を追加するのみの動作となる。この節の動きは一方向であるため、ＣＮＦへの節の追加・削除の機能自体の整合性が保たれていれば、データの整合性は保たれる。よって未分類ＣＮＦや未導出ＣＮＦの整合性を保つことにより、分類機能と導出機能はそれぞれ独立して動作させることができる。【００８１】同様に、分類機能自身も複数並列して実行することが可能である。分類機能は必要な節を未分類ＣＮＦから抽出すると、すぐに未分類ＣＮＦから削除して記録することとなっている。そのため、その抽出〜削除の間だけ排他処理を行えば、他の分類機能が未分類ＣＮＦを参照しても整合性は保たれる。【００８２】同様に、導出機能自身も複数並列して実行することが可能である。導出機能は相関ＣＮＦ（の全ての錯綜ＣＮＦの導出済ＣＮＦと導出ＣＮＦの未導出ＣＮＦ）から完備相関ＣＮＦを構成し、浸出ＣＮＦを構成する。そのため、導出中の相関ＣＮＦについて導出の間だけ排他処理を行えば、他の導出機能が導出を行っていない相関ＣＮＦを参照しても整合性は保たれる。【００８３】また、上記の出力機能において、充足可能であることを出力する際に、調和ＣＮＦ冪索引のレコードから不備相関ＣＮＦを構成し、その不備相関ＣＮＦに含まれない極小調和ＣＮＦを偽とする真理値割当を集めて出力する場合がある。不備相関ＣＮＦに含まれない極小調和ＣＮＦを偽とする真理値割当は、つまりは対象ＣＮＦを真とする真理値割当の一部であり、その真理値割当を集めることにより、対象ＣＮＦ全体を真にする真理値割当を求めることができる。
【発明の効果】
【００８４】本発明により、ＣＮＦＳＡＴの潜在的な制約を顕在化することが可能となり、ＣＮＦＳＡＴの計算複雑性に関連するＣＮＦの構造を整理・抽出したデータ構造を実現できた。またそのようなデータを構成する機能をコンピュータで実現することが可能となった。また、そのようなデータ構造を活用してＣＮＦＳＡＴを計算する機能をコンピュータで実現することが可能となった。
【図面の簡単な説明】
【００８５】
【図１】本発明の実施形態の一例を示す構成図である。
【図２】本発明の実施形態の一例を示すフローチャートである。
【図３】本発明の分類機能の一例を示すフローチャートである。
【発明を実施するための形態】
【実施例１】
【００８６】以下に本発明の実施形態の一つについて説明する。図１は本例によるデータ構成図である。本例では（Ａ∨Ｘ）∧（Ｃ∨¬Ｘ）の実施形態を挙げるが、他のＣＮＦについても同様のデータ構成となる。【００８７】本データ構造には、対象となるＣＮＦのデータとなる対象ＣＮＦが記録されている。本例では対象ＣＮＦ１０１が記録されており、対象ＣＮＦ１０１にはその節となる、（Ａ∨Ｘ）に対応する節１１１、（Ｃ∨¬Ｘ）に対応する節１１２が記録されている。【００８８】また、対象ＣＮＦの調和関係を表す調和ＣＮＦも記録されている。本例では、調和変数組が｛Ｘ｝となる調和ＣＮＦ１２１、｛¬Ｘ｝となる調和ＣＮＦ１２２、｛Ａ，Ｘ｝となる調和ＣＮＦ１２３、｛Ｃ，¬Ｘ｝となる調和ＣＮＦ１２４、｛Ｃ｝となる調和ＣＮＦ１２５、｛Ａ｝となる調和ＣＮＦ１２６によって表される。対象ＣＮＦの節に含まれる調和変数組は以上となる。他の調和変数組による調和ＣＮＦも考えることができるが、対象ＣＮＦの構造を表すのには重要でないため、本例では省略する。【００８９】調和ＣＮＦはそれぞれ同じようなデータ構造をしているが、図にはそのうち調和ＣＮＦ１２１を代表して詳細を記載する。【００９０】調和ＣＮＦ１２１、及び（調和ＣＮＦ１２１と調和変数組の一致する）節１１１には、お互いへの双方向参照が記録されている。そのため、調和ＣＮＦ１２１から節１１１を参照することも可能であり、逆に節１１１から調和ＣＮＦ１２１を参照することも可能である。同様に、調和ＣＮＦ１２２と節１１２、調和ＣＮＦ１２３と節１１１、調和ＣＮＦ１２４と節１１２、調和ＣＮＦ１２５と節１１２、調和ＣＮＦ１２６と節１１１には、それぞれへの双方向参照が記録されている。【００９１】また、相関変数組の一致する調和ＣＮＦ１２１と調和ＣＮＦ１２２には、同じ相関ＣＮＦとなる調和ＣＮＦへの循環リストが記録されている。この循環リストを辿ることにより、ある調和ＣＮＦの錯綜ＣＮＦを抽出することが可能である。また、調和ＣＮＦ１２３のように他の調和ＣＮＦが存在しない場合は、循環リストの取り扱いを容易にするために、自分自身への参照が記録されている。【００９２】また、本データ構造には調和ＣＮＦの中に導出済ＣＮＦが記録されているとする。例えば調和ＣＮＦ１２１の中には導出済ＣＮＦ１３１が記録されている。同様に、調和ＣＮＦ１２２の中には導出済ＣＮＦ１３２が、調和ＣＮＦ１２３の中には導出済ＣＮＦ１３３が、調和ＣＮＦ１２４の中には導出済ＣＮＦ１３４が、調和ＣＮＦ１２５の中には導出済ＣＮＦ１３５が、調和ＣＮＦ１２６の中には導出済ＣＮＦ１３６が記録されている。なお、未導出ＣＮＦの節は導出済ＣＮＦに含まれない調和ＣＮＦの節となる。【００９３】また、本データ構造では調和ＣＮＦ冪索引１４１が記録されており、調和ＣＮＦ冪索引１４１により、調和変数組から調和ＣＮＦを冪検索できるようになっている。本例の調和ＣＮＦ冪索引１４１は、調和変数組をキーとして調和ＣＮＦをレコードとする二分木となっている。【００９４】また、本データ構造には、浸出ＣＮＦ１７１が記録されている。もしも調和ＣＮＦ１２１と調和ＣＮＦ１２２から導出を行った場合、その浸出節（Ａ∨Ｃ）は浸出ＣＮＦ１���１に記録される。この浸出ＣＮＦ１７１に記録されるデータは、対象ＣＮＦ１０１と同様に節のデータが記録され、調和ＣＮＦなどから参照される。【００９５】また、本データ構造には、まだ調和ＣＮＦに分類していない節を集めた未分類ＣＮＦ１５１が記録されている。もしも調和ＣＮＦ１２１と調和ＣＮＦ１２２から導出を行った場合、その浸出節（Ａ∨Ｃ）は浸出ＣＮＦ１７１に記録されたあと、その参照が未分類ＣＮＦに記録される。なお、未分類ＣＮＦをさらに対象ＣＮＦとして扱い、浸出節を調和ＣＮＦに分類することもある。【００９６】また、本データ構造には未導出調和ＣＮＦ集合１６１も記録されている。本例では調和ＣＮＦ１２１の節１１１が未導出ＣＮＦとなっており、他の調和ＣＮＦの節は全て導出済ＣＮＦに記録されている。そのため、未導出調和ＣＮＦ集合１６１には調和ＣＮＦ１２１が記録されている。
【実施例２】
【００９７】以下に本発明の実施形態の一つについて説明する。本例は前述のデータ構造を使用して対象ＣＮＦの構造を顕在化するプログラムである。図２は本例のフローチャートである。フローチャートでは、機能の分岐条件や機能を切り分けて記載している。具体的には分岐２０３〜処理２０４は分類機能、分岐２０５〜分岐２１０は導出機能、処理２１１、２１２は出力機能となる。【００９８】本例では、まず開始２０１より処理を開始すると、入力機能となる処理２０２により入力として受け取ったＣＮＦのデータを未分類ＣＮＦに追加して記録する。【００９９】次に、分岐２０３で未分類ＣＮＦに節が存在するかの判定を行う。節が存在する場合は分類機能となる処理２０４を適用し、さもなければ分岐２０５に移行する。【０１００】処理２０４は、未分類ＣＮＦの節の調和ＣＮＦへの分類を行う。処理２０４の詳細なフローチャートを図３に示す。【０１０１】まず始めに処理３０２により未分類ＣＮＦから対象節を選択する。選択する方法は前述の通常のプログラムで使用される方法とするが、本例では未分類ＣＮＦに最後に追加された節を選択するとする。次に検索機能となる処理３０３により、調和ＣＮＦ冪索引から、対象節の調和変数組（及び調和部分変数組）に対応する調和ＣＮＦを冪検索する。検索した調和ＣＮＦに極小調和ＣＮＦが存在する場合、対象節は簡約律により簡約化できるため、これ以上の処理は行わず分岐３０４で終了３０９に分岐する。【０１０２】極小調和ＣＮＦが存在しない場合は、分岐３０４で分類処理に分岐する。まず処理３０５で冪検索した調和ＣＮＦを全て抽出し、作成機能となる処理３０６により、もしも相関ＣＮＦに含まれない調和ＣＮＦが存在する場合は相関ＣＮＦへの追加を行う。【０１０３】処理３０６は、調和ＣＮＦに節が存在するかどうかで相関ＣＮＦへの追加を行うかどうかの判定を行う。一度処理された調和ＣＮＦには必ず節が存在するため、節の含まれない調和ＣＮＦは初めて現れた調和ＣＮＦと考えることができる。そこで、処理３０６では節の含まれない調和ＣＮＦを抽出し、その調和ＣＮＦに対応する相関変数組を構成し、相関変数組に対応する相関ＣＮＦを検索する。なお、処理３０６は簡単化のため、相関変数組を全て肯定変数からなる調和変数組で代用し、また相関ＣＮＦも全て肯定変数からなる調和ＣＮＦで代用する。つまり全て肯定変数からなる調和ＣＮＦは、たとえＣＮＦに節が含まれないとしても相関ＣＮＦの代用として相関ＣＮＦに含まれることになる。そのため、全て肯定変数からなる調和ＣＮＦは特別扱いする必要があり、もしも対象節が全て肯定変数で構成される場合は処理３０６による処理を行わない。【０１０４】次に追加機能となる処理３０７により、調和ＣＮＦに対象節を追加する。この際に、もしも調和ＣＮＦの未導出ＣＮＦに節が含まれない場合は、その調和ＣＮＦを未導出調和ＣＮＦ集合に追加する。【０１０５】次に削除機能となる処理３０８により、対象節により簡約化される節の削除を行う。まず対象節を極小調和ＣＮＦとする調和ＣＮＦを抽出する。この調和ＣＮＦに含まれる節は全て対象節によって簡約化される節となる。なお、この調和ＣＮＦには処理３０７によって追加された対象節も存在するため、まずはこの調和ＣＮＦから対象節を除いた節を削除ＣＮＦとして抽出する。そして、削除ＣＮＦのそれぞれの節から、その節の属する調和ＣＮＦを抽出し、その節を削除する。節にはその節の所属する調和ＣＮＦへの参照が（双方向参照として）含まれるため、その参照を辿ることにより節を削除する必要のある調和ＣＮＦを抽出することができる。この削除を全ての調和ＣＮＦについて行った後に、その節自体の削除を行う。この削除を、削除ＣＮＦに含まれる節全てについて行う。この結果、簡約化される節は全て削除され、対象節が調和ＣＮＦに残ることになる。処理３０８を実行した後は終了３０９に移行し、処理２０４を終了する。処理２０４は、終了後に再び分岐２０３に移行する。【０１０６】分岐２０３で未分類ＣＮＦに節が存在しない場合は、導出機能に移行する。導出機能は、まず分岐２０５で導出済ＣＮＦでない節のある調和ＣＮＦが存在するかどうかを判定する。存在する場合はその節を導出ＣＮＦとして抽出して処理２０６に移行し、存在しない場合は出力機能となる処理２１２に移行する。【０１０７】処理２０６では、まず導出ＣＮＦと同じ相関ＣＮＦに属する調和ＣＮＦを錯綜ＣＮＦとして抽出する。同じ相関ＣＮＦに属する調和ＣＮＦは、循環リストによりお互いに参照可能なため、この循環リストを辿ることで全ての錯綜ＣＮＦを抽出する。【０１０８】次に分岐２０７にて、錯綜ＣＮＦが浸出ＣＮＦを導出する条件を満たすかどうかを判定する。条件を満たす場合は処理２０９に移行し、満たさない場合は処理２０８に移行する。【０１０９】判定する条件の１つは、錯綜ＣＮＦの導出済ＣＮＦに節を含まないＣＮＦが存在しないかである。錯綜ＣＮＦの導出済ＣＮＦに節が存在しない場合は浸出ＣＮＦの導出を行うことができない。よって、錯綜ＣＮＦに節を含まないＣＮＦが存在する場合は浸出ＣＮＦが存在しないということで処理２０８に移行する。【０１１０】判定する条件の１つは、錯綜ＣＮＦの数が相関変数組の変数の数を指数とする２の冪乗となるかである。相関ＣＮＦが完備相関ＣＮＦを構成するためには、その調和ＣＮＦの種類の数が最大数存在しなくてはならない。種類の数の最大数は変数の数をＮとすると２＾Ｎ（ただし＾は冪乗を表す）となるため、錯綜ＣＮＦは２＾Ｎ−１になる必要がある。もしも錯綜ＣＮＦの数が２＾Ｎ−１未満の場合は、相関ＣＮＦは不備相関ＣＮＦとなるため、浸出ＣＮＦを導出できない。よって、錯綜ＣＮＦが２＾Ｎ−１未満の場合は処理２０８に移行する。【０１１１】処理２０８では導出ＣＮＦの全ての節を導出済ＣＮＦに変更して記録し、分岐２０３に移行する。【０１１２】次に、処理２０９に移行する。処理２０９では、まず導出ＣＮＦから導出済ＣＮＦでない節全てを未導出ＣＮＦとして抽出し、導出ＣＮＦから削除して記録する。そして、未導出ＣＮＦと錯綜ＣＮＦの導出済ＣＮＦそれぞれから１つの節を取り出す組合せ全てについて完備相関ＣＮＦを構成して浸出節を構成し、この浸出節を全ての組合せについて構成することで複数の浸出節を構成し、構成した浸出節を浸出ＣＮＦに追加して記録し、その参照を未分類ＣＮＦに追加して記録する。そして分岐２１０に移行する。【０１１３】また、もしも浸出ＣＮＦに空節が含まれる場合は、対象ＣＮＦは充足不可となることが確定する。そのため分岐２１０で浸出ＣＮＦに空節が含まれるかどうかの判定を行い、もしも含まれる場合は出力機能となる処理２１１に移行する。もしも空節が含まれない場合は、分岐２０３に移行して未分類ＣＮＦの処理を継続する。【０１１４】処理２１１は結果の出力となる。まず計算結果として調和ＣＮＦ冪索引を出力し、かつ対象ＣＮＦが充足不可なことを出力する。そして終了２１３に移行する。【０１１５】処理２１２は結果の出力となる。まず計算結果として調和ＣＮＦ冪索引を出力し、かつ対象ＣＮＦが充足可能なことを出力する。さらに調和ＣＮＦ冪索引のレコードから不備相関ＣＮＦを構成し、その不備相関ＣＮＦに含まれない極小調和ＣＮＦを全て偽とする真理値割当を集めて出力する。そして終了２１３に移行する。【０１１６】このように本例のプログラムを構成することで、対象ＣＮＦの複雑性を表す相関ＣＮＦと、対象ＣＮＦの充足可否を計算する機能をコンピュータに実現させることができるようになる。
【実施例３】
【０１１７】以下に本発明の実施形態の一つについて説明する。本例は前述のプログラムにおいて、導出機能を未導出ＣＮＦ単位ではなく相関ＣＮＦ単位で行うものである。具体的には上記プログラムにおいて導出機能となる処理２０９が下記の処理４０９となったプログラムである。処理４０９は、処理２０９と異なり、相関ＣＮＦから全ての未導出の浸出ＣＮＦを構成する。【０１１８】つまり、処理４０９は処理２０９を一度適用すると、導出ＣＮＦの循環リストを辿り、錯綜ＣＮＦを導出ＣＮＦとして導出を繰り返す。これを全ての相関ＣＮＦについて繰り返す。【０１１９】このように、相関ＣＮＦについて一括して導出を行うことで、導出ＣＮＦの選択などのオーバーヘッドを抑えることができる。
【産業上の利用可能性】
【０１２０】前述の通り、ＣＮＦＳＡＴの潜在的な制約を顕在化することにより、そのＣＮＦＳＡＴの計算複雑性を顕在化することができるようになった。また、ＣＯＮＰとなる充足不可となるＣＮＦＳＡＴの判定を理論上可能な範囲で効率良く行うことができるようになった。またそのようなデータを構成する機能をコンピュータで実現することが可能となった。また、そのようなデータ構造を活用してＣＮＦＳＡＴを計算する機能をコンピュータで実現することが可能となった。以上をコンピュータの並列処理を活用しながら効率的に行うことができるようになった。
【符号の説明】
【０１２１】１０１  対象ＣＮＦ
１１１〜１１２  節
１２１〜１２６  調和ＣＮＦ
１３１  導出済ＣＮＦ
１４１  調和ＣＮＦ冪索引
１５１  未分類ＣＮＦ
１６１  未導出調和ＣＮＦ集合
２０１  開始
２０２、２０４、２０６、２０８、２０９、２１１、２１２  処理
２０３、２０５、２０７、２１０  分岐
２１３  終了
３０１  開始
３０２、３０３、３０５、３０６、３０７、３０８  処理
３０４  分岐
３０９  終了
【図１】
2012198865.tif 000003
【図２】
2012198865.tif 000004
【図３】
2012198865.tif 000005