近似手法と数式処理の融合による実数多項式制約の効率化

Material type: 文書・図像類

Author: 小川, 瑞史

Publisher: -

Publication date: 2015-06-10

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 本研究では、多項式制約解消アルゴリズムである区間制約伝播の拡張としてraSAT ループを提案し、SMTソルバ raSATとして実装を行った。制約解消の解は SAT（充足可能）かUNSAT（充足不能）だが、SAT検出はエラー検出、UNSAT検出はループ不変式生成に用いられる。数百変数程度の大規模な問題...

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

JAIST Repository
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
JAIST Repository

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 近似手法と数式処理の融合による実数多項式制約の効率化
Author/Editor: 小川, 瑞史
Author Heading: 小川, 瑞史
Publication Date: 2015-06-10
Publication Date (W3CDTF): 2015-06-10
Alternative Title: Optimization of polynomial constraint solving based on fusion of approximation and algebraix methods
Periodical title: 科学研究費助成事業研究成果報告書
Pages: 1-4
Text Language Code: jpn
Subject Heading: ソフトウェア
仕様記述
仕様検証
制約解消
数式処理
Target Audience: 一般
Note (General): 本研究では、多項式制約解消アルゴリズムである区間制約伝播の拡張として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
研究分野：理論計算機科学、形式手法
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/12815
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/12815/1/23300005seika.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/12815/1/23300005seika.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ