| 研究概要 |
本年度は,CNF論理式の最大充足化問題,すなわちMAX SAT問題に対する例題生成手法の基本的な解析を行った.具体的には各節にちようど2つのリテラルがあるCNF論理式を対象とするMAX 2SAT問題をとりあげた.
この問題に対し,最適解を保障するための構造を理論的に考察し,必ず最適解を保障する例題生成アルゴリズムを考案した.具体的には次のような手法である.2CNF論理式では充足不可能であるための必要十分な構造が知られている.この構造を用いて,極小な,すなわちどれかひとつでも節を取り除くと充足可能となる充足不可能2CNF論理式をランダムに生成することができる.このとき,任意に固定された真理値割当で1個だけ充足不可能な節があるように生成することも可能である.このようにして得られた,ある任意に固定された真理値割当で充足できない節が1個である極小な充足不可能2CNF論理式を,複数個組み合わせることによって,最適解を保障したMAX 2SAT問題のテスト例題が生成できる.
さらに,この例題生成アルゴリズムが生成する例題の集合がNP完全,すなわち厳密に最適解を求めることが困難だと考えられるクラスに属することを理論的に証明した.この結果からすぐに「生成される問題はすべて難しい」ということは言うことはできないが,少なくとも「生成される問題はすべて易しい」ということではないことが予想される.すなわち,テスト例題として「全くふさわしくない」ということではないと予想される.
|
