3M-2
連結性を有する組合せパズルの直接符号化法を用いたSATソルバでの解法と性能評価
○舟野勝彦，上嶋章宏（大阪電通大）
組合せパズルには，NP困難に属するような問題が多く存在する．
本研究では，そのような問題の解を高速に求めるために
SATソルバを用い，組合せパズルの解法を設計する．

制約条件として連結性を持つ組合せパズルでは，SATへ
符号化する際，連結性チェックを管理する論理式のサイズが
全体の大部分を占める．
そのような組合せパズルでは，SATへの符号化法の工夫が
計算時間にも影響を与えると考えられる．

本発表では，組合せパズルが持つ制約条件を表現するCNF論理式を
構成し，SATソルバを用いて解く手法と，論理式サイズの削減手法に
ついて述べる．また，連結性を持つ組合せパズルに対して，
符号化法の違いによる計算時間についての評価を示す．