[3L4-GS-1] 基礎・理論：

[3L4-GS-1-02] 順序符号化アルゴリズムの実装に関する一考察

〇船木 泰平¹、堀岡 真未、宋 剛秀¹ (1. 神戸大学)

キーワード：SAT、CSP、SAT符号化

本論文では，制約充足問題（CSP）に適用可能な順序符号化のアルゴリズムと実装について考察する．命題論理の充足可能性判定 (SAT) 問題を解くプログラムであるSATソルバーの性能向上を背景に，CSPをSAT問題に変換して解くSAT型CSPソルバーが活発に研究されている．順序符号化は代表的なSAT型CSPソルバーであるSugarやFun-sCOPで採用されている符号化であり，これらのソルバーでは順序符号化アルゴリズムによりSAT問題を構成する節集合を生成する．本論文では，まず既存の順序符号化アルゴリズムを用いた場合に冗長な節が生成される場合があることを示す．次に冗長な節を生成しない改良した順序符号化アルゴリズムを示す．この改良は，メモを用いて既に生成した節に包摂される冗長な節を検査する方法により実現する．提案方法の有効性を評価するために，国際CSPソルバー競技会のベンチマークに対して，提案アルゴリズムがどのくらい節数を削減できるか調査を行った．結果として，19%の問題で節数の削減効果を確認し，SAT型CSPソルバーの求解時間が短くなる問題があることも確認した．