|
JAIST Repository >
b. 情報科学研究科・情報科学系 >
b50. 科学研究費助成事業研究成果報告書 >
2014年度 >
このアイテムの引用には次の識別子を使用してください:
http://hdl.handle.net/10119/12815
|
| タイトル: | 近似手法と数式処理の融合による実数多項式制約の効率化 |
| その他のタイトル: | Optimization of polynomial constraint solving based on fusion of approximation and algebraix methods |
| 著者: | 小川, 瑞史 |
| 著者（別表記）: | Mizuhito, Ogawa |
| キーワード: | ソフトウェア
仕様記述
仕様検証
制約解消
数式処理 |
| 発行日: | 10-Jun-2015 |
| 抄録: | 本研究では、多項式制約解消アルゴリズムである区間制約伝播の拡張としてraSAT ループを提案し、SMTソルバ raSATとして実装を行った。制約解消の解は SAT（充足可能）かUNSAT（充足不能）だが、SAT検出はエラー検出、UNSAT検出はループ不変式生成に用いられる。数百変数程度の大規模な問題に対し、実質的に後者が解けるのはUNSATコア（小さな部分制約で充足不能となるもの）を発見した場合に限られ、前者はすべての制約の充足性の確認が必要なため、実用上より困難である。本研究ではSAT検出に焦点をあて、SMTlibベンチマーク上の実験で答えが未知であった複数の問題のSATを検出した。 : ）：This research extends the interval constraint propagation to the raSAT loop, which is implemented as an SMT solver raSAT. A polynomial constraint solving concludes either SAT (satisfiable) or UNSAT (unsatisfiable). raSAT is designed to intend the former, which is often used for error detection, where the latter is used for loop invariant generation. In practice, when tackling a larger problem with several hundred variables, UNSAT is detected only with the discovery of a small UNSAT core, whereas SAT is detected by finding an instance that satisfies all constraints, and often becomes a harder problem. In experiments, we newly found that several unsolved problems in SMTlib benchmark are SAT. |
| 記述: | 研究種目：基盤研究(B)
研究期間：2011～2014
課題番号：23300005
研究者番号：40362024
研究分野：理論計算機科学、形式手法 |
| 言語: | jpn |
| URI: | http://hdl.handle.net/10119/12815 |
| 出現コレクション: | 2014年度 (FY 2014)
|
このアイテムのファイル:
| ファイル |
記述 |
サイズ | 形式 |
|---|
| 23300005seika.pdf | | 100Kb | Adobe PDF | 見る/開く |
|
当システムに保管されているアイテムはすべて著作権により保護されています。
|
