| 研究概要 |
1.充足解の個数などのSAT例題の属性を制御可能な例題生成系の利点を利用して,局所探索法を基本戦略としたSATアルゴリズムに項の重みつけ法と呼ばれる発見的手法を適用することが大きな性能の向上をもたらすことをIJCAI'95会議で発表した.また,項の重みつけ法の得手不得手を詳細に調べることにより,SAT例題に含まれない新しい項の追加がより有効であることをAAAI-96会議で発表した.項を追加することにより問題のサイズは大きくなり問題が難しくなってしまうと思われるが,実際には効率良く問題を解くことができるということ示しており.大きな反響を呼んだ.
2.SATの例題生成のプロセスが,導出原理による定理証明のプロセスの逆に類似していることを利用して,導出原理の中でも最も易しいと考えられる単読導出原理がNP完全であることを証明した.我々の生成系は少なくともこの証明系の逆よりはかなり複雑なので,その安全性がかなり主張できたと考えられる.こちらはIEEE Structure in Complexity会議で発表された.例題生成への応用もさることながら,この結果はそれ自身非常に興味深い.導出原理は実用的にはかなり効率が良いと広く信じられていたが,その計算複雑さは未解決のままだった.最も制限された単読導出原理でさえ手に負えないことは,驚くべき結果として注目された.
3.属性制御可能な例題生成技術の研究で得られた成果は「Cliqoes,Coloring,and Satisfiability (DIMACS Series 26)」で公表された.また,その中では,本システムにより生成された例題を入力として様々なSATアルゴリズムに対する計算機実験の結果が他の研究者達により報告されており,SATに対する有効な解法の選定に大きく貢献をした.
|
