[AT-1] 組合せ論と情報理論 −最新動向と展望−

[AT-1-3] SATソルバーと利用技術

宋剛秀 (神戸大)

Keywords:SATソルバー、SAT符号化

SATソルバーとは，命題論理式の充足可能性判定（SAT）問題を解くプログラムである．1960年代から多くの研究が蓄積されており，特に2000年以降その性能が飛躍的に向上している．そのためSATソルバーは様々な応用分野における推論の基盤技術として注目を集めている． しかし，一方で，その入力は連言標準形の命題論理式であるため，SATソルバーを使って問題を解きたい場合は，多くの場合SAT符号化と呼ばれる方法で変換を行う必要がある．チューリング賞受賞者である Donald E. Knuth は著書で ``Thus the art of problem encoding turns out to be just as important as the art of devising algorithms for satisfiability.'' と述べており，SAT符号化がSATソルバーと同様に重要技術であることを強調している．本講演では，これらSATソルバーとその利用技術であるSAT符号化について説明を行う．