解の再利用を用いたSATに基づくテスト生成におけるインスタンス順序と変数割当順序の決定法

摘要

本稿では充足可能性問題（SAT）に基づくテスト生成問題を取り上げ，解を再利用しながら複数のインスタンスを解く状況下での求解の効率について議論する．その効率に主に影響を与える3つの要素（1）インスタンス順序，（2）変数割当て順序，（3）論理値割当てのうち前者2つに着目し，それらの効果的な決定法を提案する．提案手法では，インスタンス順序を決定するために必要な類似度計算の回数を閾値によって減らし，手法全体の処理時間の削減を行う．また，解の再利用の履歴をリテラル単位で管理することによって変数割当て順序を決定し，解の探索効率を高める．本研究では，予備実験結果により提案手法で必要なパラメータ設定の指針を導くとともに，そのパラメータ設定の下で従来手法との比較実験を行い提案手法の有効性を示す．