1995 Fiscal Year Annual Research Report

各種属性を制御可能なランダムテスト例題生成技術の研究

Research Project

Project/Area Number	07458061
Research Category	Grant-in-Aid for General Scientific Research (B)
Research Institution	Kyushu University
Principal Investigator	岩間一雄九州大学, 工学部, 教授 (50131272)
Co-Investigator(Kenkyū-buntansha)	岩本宙造九州芸術工科大学, 芸術工学部, 講師 (60274495) 澤田直九州大学, 工学部, 助手 (70235464) 櫻井幸一九州大学, 工学部, 助教授 (60264066)
Keywords	充足可能性問題 / 充足解数の制御 / 局所探索法 / 重みつけ法 / 定理自動証明 / 単読導出原理 / 計算複雑さ / 例題生成系の安全性
Research Abstract	1.充足解の個数を制御できる利点を利用して,充足解の個数が少ない時に性能が悪いとされていた代表的なSATアルゴリズムである局所探索法を詳細に評価することができた.その結果,重みつけ法と呼ばれるヒューリスティックが他のヒューリスティックスに比べて格段にすぐれていることを示せた.この成果はIJCAI'95で発表され大きな反響を呼んだ.従来,局所探索法の性能評価は非常に限定された純粋なランダム例題に限られていたので,多くの人が実際の性能に疑問を抱いていた.我々の結果はこの疑問をかなり解消することに成功した. 2.SATの例題生成のプロセスが,導出原理による定理証明のプロセスの逆に類似していることを利用して,ある種の導出原理が困難であることを証明して我々の生成系の安全性を保証することを試みた.導出原理の中でも最も易しいと考えられる単読導出原理がNP安全であることを証明した.我々の生成系は少なくともこの証明系の逆よりはかなり複雑なので,その安全性がかなり主張できたと考えられる.こちらはIEEE Structure in Complexity会議で発表された.例題生成への応用もさることながら,この結果はそれ自身非常に興味深い.導出原理は実用的にはかなり効率が良いと広く信じられていたが,その計算複雑さは未解決のままだった.最も制限された単読導出原理でさえ手に負えないことは驚くべき結果として注目された. 現有の例題生成系を公開することも重要な目標であったが,これに関しては今だ実現されておらず,8年度の課題としたい.

Research Products

(7 results)

All Other

All Publications (7 results)

[Publications] 岩間,一雄: "α-Connectivity: A gradually non-parallel graph problem" Journal of Algorithms. (発表予定). (1996)
[Publications] 岩間,一雄: "Routing problems on the mesh of buses" Journal of Algorithms. (発表予定). (1996)
[Publications] 岩間,一雄: "Time lower bounds do not exist for CRCW PRAMs" Theoretical Computer Science. (発表予定). (1996)
[Publications] 車,炳〓: "Performance test of local scarch algorithms using new types of random CNF formulas" Proc. International Joint Conference on Artificial Intelligence. 304-310 (1995)
[Publications] 岩間,一雄: "Intractability of read-once resolution" Proc. 10th IEEE Structure in Complexity Theory Conference. 29-36 (1995)
[Publications] 岩間,一雄: "Exponential lower bounds for he tree-like Hajos calculus" Information Processing Letters. 54. 289-294 (1995)
[Publications] 岩間,一雄: "「逐次アルゴリズムの理論」(新版情報処理ハンドブック,1偏3章3節)" オーム社, (1995)

1995 Fiscal Year Annual Research Report

各種属性を制御可能なランダムテスト例題生成技術の研究

Principal Investigator

岩間 一雄 九州大学, 工学部, 教授 (50131272)

Research Products

[Publications] 岩間,一雄: "α-Connectivity: A gradually non-parallel graph problem" Journal of Algorithms. (発表予定). (1996)

[Publications] 岩間,一雄: "Routing problems on the mesh of buses" Journal of Algorithms. (発表予定). (1996)

[Publications] 岩間,一雄: "Time lower bounds do not exist for CRCW PRAMs" Theoretical Computer Science. (発表予定). (1996)

[Publications] 車,炳〓: "Performance test of local scarch algorithms using new types of random CNF formulas" Proc. International Joint Conference on Artificial Intelligence. 304-310 (1995)

[Publications] 岩間,一雄: "Intractability of read-once resolution" Proc. 10th IEEE Structure in Complexity Theory Conference. 29-36 (1995)

[Publications] 岩間,一雄: "Exponential lower bounds for he tree-like Hajos calculus" Information Processing Letters. 54. 289-294 (1995)

[Publications] 岩間,一雄: "「逐次アルゴリズムの理論」(新版情報処理ハンドブック,1偏3章3節)" オーム社, (1995)

岩間一雄九州大学, 工学部, 教授 (50131272)