| 研究課題/領域番号 |
11780236
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 国立情報学研究所 (2000)
広島市立大学 (1999) |
|---|
研究代表者 |
新井 紀子 国立情報学研究所, 情報学基礎研究系, 助教授 (40264931)
|
|---|
| 研究期間 (年度) |
1999 – 2000
|
| 研究課題ステータス |
完了 (2000年度)
|
| 配分額 *注記 |
2,200千円 (直接経費: 2,200千円)
2000年度: 1,100千円 (直接経費: 1,100千円)
1999年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 自動証明 / 証明の複雑さ / 証明論 / 計算の複雑さ / 計算量 / ロジック |
|---|
| 研究概要 |
平成11年度に提案した、simple combinatorial reasoningが類似の体系であるsymmetryつきのresolutionよりも体系として優れていることを証明した。すなわち、symmetryつきのresolutionはbackward searchができないという自動証明機向けの体系としての大きな欠点があるばかりでなく、simple combinatorial reasoningでは線形時間で解決可能であるような問題にたいして、指数時間かかることがあることを示した。このことで、simple combinatorial reasoningの優位性を証明したといえる。
一方、simple combinatorial reasoningをC言語を使って自動証明機Godzillaとして実装した。そして、この自動証明機が初等的組み合わせ問題に対してどれだけ短時間で大規模な問題を自動的に解くことができるのかを(1)鳩ノ巣問題(2)部分集合問題(3)k分割問題(4)クリーク色分け問題などを例にとって、実験を行う。その結果、今回開発されたGodzillaが最先端の各種の自動証明機よりも高速で問題解決することが確認された。
上に挙げられた問題に関してはGodzillaの計算時間は入力の二乗程度のオーダであった。ただし、この結果は入力となる命題論理式を元の述語論理式からシステマティックに変換して得た場合であり、入力をシャッフルすると、計算時間は指数時間かかってしまう。このことを改善するため、さまざまなヒューリスティックスを検討して、好結果が得られるものをさらに選りすぐり、改良型Godzillaに発展させた。
|
