| Research Abstract |
本研究の目的は,系統的SATソルバーと確率的SATソルバーの両方を含む,複数のSATソルバーを競争的・協調的に並行動作させることにより,単一のソルバーをチューニングする以上の効果を得ることである.
本年度は,並列SATソルバーの適用が期待される問題として,組合せテスト生成問題を取り上げ,以下の研究成果を得た.組合せテストはソフトウェアのテスト手法の一つであり,近年ソフトウェア工学の分野において,活発に研究が行われている.
1. 組合せテスト生成問題をSAT問題へ変換・コンパイルする新しいSAT符号化を考案した.このSAT符号化は,順序符号化法と呼ばれる制約充足問題からSAT問題へのSAT符号化法に基づいている.
2. SAT符号化された組合せテスト生成問題に対して,系統的SATソルバーと確率的SATソルバーの両方を用いた実行実験を行った.その結果,これまで最適値が未知であった3問(CA、(3,12,2), CA(3,13,2), CA(3,14,2))について,その最適値を決定することに成功した.
2において最適値を決定した問題のうち,CA(3,12,2)は,2009年に出版された"Handbook of Satisfiability(IOS Press)"でも未解決問題として挙げられている求解困難な問題であった.一方,組合せテスト生成問題の問題規模が大きくなると,生成されるSAT問題のサイズが巨大になるという問題があり,サイズの縮小化が今後の大きな課題である.
|
