式変形による命題論理式の充足可能性問題の難しさの変化
| Přispěvatelé: | 山田, 俊行 |
|---|---|
| Jazyk: | japonština |
| Rok vydání: | 2020 |
| Popis: | 命題論理式の充足可能性問題(satisfiability problem, SAT) は計算機科学の基本問題であり, 理論的に興味深い対象であると共に多くの応用を持つ. SAT はNP 完全問題であり, これを多項式時間で解くアルゴリズムは見つかっていない. 一方で, 近年のSAT ソルバは性能が著しく向上しており, 大規模な問題例でも現実的な時間で解けるようになってきている.SAT は計算困難問題に分類されるが, どんな問題例を解くのも非現実的というわけではない. 理論的には解くことが困難とされる問題例でも, ソルバでは現実的な時間で解ける場合がある. どんな場合にSAT を解くのに時間がかかるのかという疑問は理論的にも応用的にも重要である.本研究はこの疑問に理論面と実装面から異なるアプローチで取り組んだ. 特に, 入力の式を変形したとき, 計算時間がどのように変化するかという点に焦点を当てた.実装面では, 論理式の簡単化というSAT ソルバの機能に着目した. 簡単化はSAT ソルバの前処理などに用いられ, 入力された論理式から冗長な部分を除去してソルバの求解速度を向上させることを目的とする. 本研究は, 素朴な冗長性の定義に基づく変換前後の式が論理同値な簡単化手続きとその派生について, 除去される節の個数を比較した. また, ホーン節と単位伝播を利用した新しい簡単化の手法を提案し, その効果を実験的に調べた. 結果として, 限定的に有効性を示した.理論面では, SAT の解の個数と計算複雑性の関係を解析した. SAT の解の個数に関する結果としてValiant とVazirani の孤立化補題がある. 彼らはこの補題を使い, SAT から, 解を唯一つ持つか解を持たないかのいずれかである保証を入れたUnique-SAT へ, 多項式時間乱択帰着できることを示した. 本研究は孤立化補題を一般化した. 与えられる命題論理式が解を持つ場合には丁度t 個持つ保証入り問題としてt-solution SAT を定義し, SAT からの乱択帰着を解析した. また, 与えられる命題論理式の変数の個数に応じてtに制限を加えたとき,Valiant-Vazirani の帰着技術を一般化し, SAT をt-solution SAT へ多項式時間乱択帰着する手法を示した. 結果として, 制限された範囲で, t-solution SAT がSAT と同程度に計算困難であることを示唆する. 三重大学大学院 工学研究科 博士前期課程 情報工学専攻 コンピュータソフトウェア研究室 28p |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|