講演情報
[2J5-OS-36a-03]SAT符号化を用いたCSPソルバーの一実装と評価
〇宋 剛秀1 (1. 名古屋大学大学院情報学研究科)
キーワード：
充足可能性判定問題、制約充足問題、制約プログラミング
SATソルバーとは，命題論理式の充足可能性判定（SAT）問題を解くプログラムである．1960年代から多くの研究が積み重ねられており，特に2000年以降は性能が飛躍的に向上してきた．しかし，SATソルバーの入力形式は素朴な連言標準形の論理式であるため，実世界の問題を直接記述することは容易ではない．このため，より記述性の高い制約充足問題（CSP）をSAT問題へと符号化し，SATソルバーの高い性能を活かしつつ，多様な制約を直接記述できるSAT型CSPソルバーが開発され，多くの分野で成功を収めている．本研究では，このようなSAT型CSPソルバーの一実装を紹介し，その評価を行う．