変数値域を限定した試行に基づく高次制約問題の充足可能性推定方法の検討

• 中山, 寛己

• 高野, 保真

• 千代, 英一郎

書誌事項

タイトル別名

• Estimation of Satisfiability for High Order Constraint Problem Based on Trials with Range Restriction of Variabels

抄録

近年，SMTソルバの研究がさかんに行われてきており，様々な制約問題を解けるよう飛躍的に進歩している．しかしながら，SMTソルバは線形制約式の解を短時間で求められることが多いのに対し，高次の制約式の解を求めるのに時間がかかってしまうことがある．たとえば，代表的なプログラム検査であるループ停止性検査等で必要となる複雑な制約式の場合，検査に数日を要することもあり，実用上の課題となっている．この問題に対して，本発表では，変数のとりうる値域を限定した検査を，値域を変えて繰り返すことで，制約式の充足可能性を推定する方法について報告する．それぞれの試行を短い時間で打ち切ることにより，結果が得られないことを避けることができる．

In recent years, studies of SMT solvers are conducted flourishingly and progress drastically to be able to solve various constraint satisfaction problems. However, while the SMT solver tends to find solution of linear constraints efficiently, it may take a few days to find solutions of the higher degree constraints needed for checking loop termination. For this problem, we examine methods to estimate the satisfiability of constraints by iterative checking (trial) with range restriction of variables. In this presentation, we report some experimental results about trial.

収録刊行物

• 情報処理学会論文誌プログラミング（PRO）

  情報処理学会論文誌プログラミング（PRO） 10 (1), 34-34, 2017-01-06

キーワード

• [発表概要]

詳細情報

• CRID: 1050845762838415360
• NII論文ID: 170000148341
• NII書誌ID: AA11464814
• ISSN: 18827802
• Web Site: http://id.nii.ac.jp/1001/00176523/
• 本文言語コード: ja
• 資料種別: article
• データソース種別:
  • IRDB
  • CiNii Articles