[AT-1-3] SATソルバーと利用技術
キーワード：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符号化について説明を行う．
講演論文集PDFを閲覧したい場合はパスワードを入力してください。
パスワードは、講演参加申込者、聴講参加申込者にメールで御連絡しております。