2020 Fiscal Year Research-status Report
Development of Practical Techniques for All Soltuion Enumeration of Large-scale Constraint Satisfaction Problems
| Project/Area Number |
17K17725
|
|---|
| Research Institution | The University of Electro-Communications |
|---|
Principal Investigator |
戸田 貴久 電気通信大学, 大学院情報理工学研究科, 准教授 (50451159)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Keywords | モデル検査 / アルゴリズム / SAT / 制約 |
|---|
| Outline of Annual Research Achievements |
有界モデル検査はハードウェアやソフトウェアなどのシステムに含まれるバグを発見するための実践的な手法の１つとして広く知られている。ここで、バグとはシステムの開発者が当然成り立つと期待する仕様に対する反例を意味し、望ましくない状態に至るシステムの実行トレースとして表現される。有界モデル検査では、そのような反例をSATソルバーで探索するアプローチが取られてきた。誤りの根本原因が１つであったとしても、ただ１つの実行トレースが反例として存在することはなく、一般には数多くの反例が存在する。有界モデル検査は１つの反例だけをバグの証拠として提示するが、その反例を構成する変数の値自体には特段の意味はなく、異なる値をとってもバグのままであることがある。本研究ではこの点に着目して、反例を構成する特定の変数をピックアップして、その変数の値だけを変動させるとき依然反例のままであるような、取りうる値の最長の区間を計算によって求める手法を与えた。
さらに、単純配線決定問題に対するCSP解法も研究した。大規模集積回路では、配置されたモジュール同士を交差しないように配線で結ぶ必要がある。この際、コストの最小化などさまざまな要因を考慮する必要があるが、それに応じて増大する複雑さのため計算の困難さの本質がわかりにくくなる。そこで配線が交差しないことだけに焦点を絞った単純配線問題がこれまで考えられてきた。さまざまな異なる計算手法が考えられてきたが、その中で本研究ではCSPソルバーを使った従来手法を改善した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
有界モデル検査の研究は本研究計画における大きな目標であった。提案手法を実現するために代表的な有界モデル検査器のNuSMV2のプログラム内部に大幅に手を加えて機能拡張をする必要があり、そのために途中で非常に多くの時間を費やした。最終的には予定していたプログラム開発を遂行して、計算機実験を行うことができた。その結果はすでに論文にまとめており、査読付き学術雑誌に投稿している。
単純配線問題の研究は当初の計画では予定していなかったが、本研究計画を進める過程で新たな結果として得られた。
この結果をまとめた論文は査読付き学術雑誌ですでに出版されている。
|
| Strategy for Future Research Activity |
有界モデル検査の研究は現在、学術雑誌に投稿中であり、査読者のコメントに応じた改訂などを今後進める。最終年度となるため、有界モデル検査を含め、これまでに実施した研究のデータやプログラムを整理して、各種の資料を公開する。また、これまでの結果を踏まえて、残されている課題を整理して事前実験や研究調査を実施しながら、今後の研究に向けた準備を進める。
|
| Causes of Carryover |
コロナ感染拡大のため研究会や国際会議などに参加しなかったため。また、投稿中の論文の出版費用なども必要なため。
|
Research Products
(3 results)
