| 研究概要 |
1.充足解の個数を制御できる利点を利用して,充足解の個数が少ない時に性能が悪いとされていた代表的なSATアルゴリズムである局所探索法を詳細に評価することができた.その結果,重みつけ法と呼ばれるヒューリスティックが他のヒューリスティックスに比べて格段にすぐれていることを示せた.この成果はIJCAI'95で発表され大きな反響を呼んだ.従来,局所探索法の性能評価は非常に限定された純粋なランダム例題に限られていたので,多くの人が実際の性能に疑問を抱いていた.我々の結果はこの疑問をかなり解消することに成功した.
2.SATの例題生成のプロセスが,導出原理による定理証明のプロセスの逆に類似していることを利用して,ある種の導出原理が困難であることを証明して我々の生成系の安全性を保証することを試みた.導出原理の中でも最も易しいと考えられる単読導出原理がNP安全であることを証明した.我々の生成系は少なくともこの証明系の逆よりはかなり複雑なので,その安全性がかなり主張できたと考えられる.こちらはIEEE Structure in Complexity会議で発表された.例題生成への応用もさることながら,この結果はそれ自身非常に興味深い.導出原理は実用的にはかなり効率が良いと広く信じられていたが,その計算複雑さは未解決のままだった.最も制限された単読導出原理でさえ手に負えないことは驚くべき結果として注目された.
現有の例題生成系を公開することも重要な目標であったが,これに関しては今だ実現されておらず,8年度の課題としたい.
|
