| 研究課題/領域番号 |
23300005
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| 研究分担者 |
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| 研究協力者 |
ヴ シュアン ツング
ト ヴァン カン
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2015-03-31
|
| キーワード | ソフトウェア / 仕様記述 / 仕様検証 / 制約解消 / 数式処理 |
|---|
| 研究成果の概要 |
本研究では、多項式制約解消アルゴリズムである区間制約伝播の拡張としてraSAT ループを提案し、SMTソルバ raSATとして実装を行った。制約解消の解は SAT（充足可能）かUNSAT（充足不能）だが、SAT検出はエラー検出、UNSAT検出はループ不変式生成に用いられる。数百変数程度の大規模な問題に対し、実質的に後者が解けるのはUNSATコア（小さな部分制約で充足不能となるもの）を発見した場合に限られ、前者はすべての制約の充足性の確認が必要なため、実用上より困難である。本研究ではSAT検出に焦点をあて、SMTlibベンチマーク上の実験で答えが未知であった複数の問題のSATを検出した。
|
| 自由記述の分野 |
理論計算機科学、形式手法
|
