1996 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number	07458061
Research Institution	KYUSHU UNIVERSITY
Principal Investigator	岩間一雄九州大学, 大学院・システム情報科学研究科, 教授 (50131272)
Co-Investigator(Kenkyū-buntansha)	宮野英次九州大学, 大学院・システム情報科学研究科, 助手 (10284548) 岩本宙造九州芸術工科大学, 講師 (60274495) 澤田直九州大学, 大学院・システム情報科学研究科, 助手 (70235464) 櫻井幸一九州大学, 大学院・システム情報科学研究科, 助教授 (60264066)
Keywords	充足可能性問題 / 充足解数の制御 / 局所探索法 / 重みつけ法 / 単読導出原理 / 計算複雑さ / 定理自動証明 / 例題生成系の安全性
Research Abstract	1.充足解の個数などのSAT例題の属性を制御可能な例題生成系の利点を利用して,局所探索法を基本戦略としたSATアルゴリズムに項の重みつけ法と呼ばれる発見的手法を適用することが大きな性能の向上をもたらすことをIJCAI'95会議で発表した.また,項の重みつけ法の得手不得手を詳細に調べることにより,SAT例題に含まれない新しい項の追加がより有効であることをAAAI-96会議で発表した.項を追加することにより問題のサイズは大きくなり問題が難しくなってしまうと思われるが,実際には効率良く問題を解くことができるということ示しており,大きな反響を呼んだ. 2.SATの例題生成のプロセスが,導出原理による定理証明のプロセスの逆に類似していることを利用して,導出原理の中でも最も易しいと考えられる単読導出原理がNP完全であることを証明した.我々の生成系は少なくともこの証明系の逆よりはかなり複雑なので,その安全性がかなり主張できたと考えられる.こちらはIEEE Structure in Complexity会議で発表された.例題生成への応用もさることながら,この結果はそれ自身非常に興味深い.導出原理は実用的にはかなり効率が良いと広く信じられていたが,その計算複雑さは未解決のままだった.最も制限された単読導出原理でさえ手に負えないことは,驚くべき結果として注目された. 3.属性制御可能な例題生成技術の研究で得られた成果は「Cliques,Coloring,and Satisfiability(DIMACS Series26)」で公表された.また,その中では,本システムにより生成された例題を入力として様々なSATアルゴリズムに対する計算機実験の結果が他の研究者達により報告されており,SATに対する有効な解法の選定に大きく貢献をした.

Research Products

(6 results)

All Other

All Publications (6 results)

[Publications] Cha,Byungki: "Performance test of local search 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] 櫻井,幸一: "On separating proofs of knowledge from proofs of membership of lauguages and its application to secure identification scheme" Proc.lst Annual Int.Computing and Combinatorics Conf.11-20 (1995)
[Publications] Cha,Byungki: "Adding new clauses for faster local search" Proc.13th National Conference on Artificial Intelligence. 304-310 (1996)
[Publications] 朝廣,雄一: "Random generation of test instances with controlled attributes" Cliques,Coloring,and Satisfiability. 26. 377-393 (1996)

1996 Fiscal Year Annual Research Report

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

Principal Investigator

岩間 一雄 九州大学, 大学院・システム情報科学研究科, 教授 (50131272)

Research Products

[Publications] Cha,Byungki: "Performance test of local search 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] 櫻井,幸一: "On separating proofs of knowledge from proofs of membership of lauguages and its application to secure identification scheme" Proc.lst Annual Int.Computing and Combinatorics Conf.11-20 (1995)

[Publications] Cha,Byungki: "Adding new clauses for faster local search" Proc.13th National Conference on Artificial Intelligence. 304-310 (1996)

[Publications] 朝廣,雄一: "Random generation of test instances with controlled attributes" Cliques,Coloring,and Satisfiability. 26. 377-393 (1996)

岩間一雄九州大学, 大学院・システム情報科学研究科, 教授 (50131272)