抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
近年,背景理論付きSAT(Satisfiability Modulo Theories,SMT)技術の発展にともなって,ハードウェア・ソフトウェアの検証など様々な問題をSMTの制約式として表現して利用する試みがさかんである。それにともない,SMTソルバの高速化に対する需要が高まり,数多くの研究が高速化を目指している。多くの制約式を効率的に解けるようになったものの,与える制約式によっては現実的な時間で解を求めることができず,そのような場合にはユーザが得られる情報はほとんどないことが問題となっている。さらに,個々のSMTソルバの実装は大変複雑になっており,制約式を変更した際の影響が予想しにくいため,情報を得るためにユーザが制約式を変更するのも難しい。そこで本論文は,与えられた制約式に対して制約を緩和した制約式を生成し,反復的にSMTソルバを利用することで,反例を蓄積するSMTソルバの実行戦略を示す。本論文で蓄積する反例は,充足不能であると判定された部分割当て,もしくは,時間内に判定できなかった部分割当てである。そのため,打ち切り時間を設けてSMTソルバをブラックボックスとして利用するアルゴリズムを提案し,SMT-LIB形式の制約式を対象とするプログラムを実装した。個々のソルバの最適化方法には立ち入らないことで,SMTソルバ内部の探索方法によらない変数選択,制約の緩和方法など実行戦略を検討する。本論文では,いくつかの制約の緩和方法について,実行時間を比較したので,その結果を示す。(著者抄録)
