| 研究実績の概要 |
H26年度は、実数上の多項式制約の充足性判定器（ＳＭＴソルバ）raSATの実装を主に学生雇用により進め、SMTcomp 2014（ウィーン数理論理連合国際会議 H26年7月に共催）に参加し、またSMTワークショップ（同共催）において口頭発表を行った。raSATの実装における主たる進捗は、(1) 効率化のための有効な戦略の発見と多岐にわたる実験による実証、(2) H25年度までは主に不等式制約のみが対象であったが、（複数）等式制約への拡張を中間値の定理を用いた拡張による実装、の二点である。(1)については、H25年度まで、有効と考えていた探索戦略が実際にはランダムな選択と有意な差がないことが実験によりわかり、探索先着の再設計を余儀なくされたが、幸いにして新たな探索戦略およびその有効性の検証を実験を通して行うことができた。(2) については、まだ十分な効率化は進めていないが、ベンチマークにより、良好な実験結果が示された。また、ロレーヌ大学LORIA のPascal Fontain博士の開発するSMTフレームワーク VeriT 上での再実装による融合を今後進める予定である。（これは11月に2週間 LORIA に滞在して討論し、合意に達した。）
H26年度は、DSMT-comp への初挑戦は参加システム4件中4位と成績は振るわなかったが、H27年度以降も挑戦する予定である。現状では Microsoft research による defacto standard なSMTソルバZ3 に及ばないが、かなりせまる性能を示しており（一部のベンチマークでは上回る）、上位の入賞をめざす。また、難関国際会議である、第21回システム構成・解析のためのツールとアルゴリズム国際会議 (TACAS 2015) には不採択となったが、現在,第10回システム構成のフロンティア国際会議 (FroCos 2015)への再投稿を準備中である。
|
