4M-01
SAT型制約ソルバーを用いた配置配線パズル解法の検討
○立野良長,若葉陽一(木更津高専)
配置配線問題とは、数字が記入されたブロックを盤面に配置し、同じ数字同士を線で結び合わせたとき、ブロックと配線を囲う矩形領域が最小となる解を求める問題である。本研究では与えられた配置配線問題を制約充足問題(CSP)に定式化し、CSPを充足可能性判定問題(SAT)に符号化し、SATソルバーに解かせることで厳密解を得ることを目的とする。
本手法では既存研究で提案されたナンバーリンクの制約を配線制約として適用し、全てのブロックが特定の領域内に配置されるための基本制約を提案する。
また、効率的な解法を得るための配置制約と配線制約に対してCSPの表現方法の検討を行った。