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

摘要

This report discusses the efficiency of iteratively solving various instances with solution reuse in test generation based on Boolean satisfiability (SAT). The efficiency is mainly affected by (1) instance ordering, (2) variable ordering and (3) logic value assignments. This work presents an effective method to determine two factors of (1) and (2). The proposed method aims at reducing the overall processing time by decreasing the number of similarity calculation, which is needed to determine an effective instance order, by means of a threshold value of similarity. The method also attempts to enhance the efficiency of searching solutions by determining an variable order with history of solution reuse in terms of literals. In this work, preliminary experiments are conducted to find out appropriate parameters used in the proposed method. Experimental results under the parameters show that the proposed method can outperform conventional methods.%本稿では充足可能性問題(SAT)に基づくテスト生成問題を取り上げ，解を再利用しながら複数のインスタンスを解く状況下での求解の効率について議論する.その効率に主に影響を与える3つの要素(1)インスタンス順序，(2)変数割当て順序，(3)論理値割当てのうち前者2つに着目し，それらの効果的な決定法を提案する.提案手法では，インスタンス順序を決定するために必要な類似度計算の回数を閾値によって減らし，手法全体の処理時間の削減を行う.また，解の再利用の履歴をリテラル単位で管理することによって変数割当て順序を決定し，解の探索効率を高める.本研究では，予備実験結果により提案手法で必要なパラメータ設定の指針を導くとともに，そのパラメータ設定の下で従来手法との比較実験を行い提案手法の有効性を示す.