教員紹介: 番原 睦則 (ばんばら むつのり)

高校生の君へ

コンピュータ科学は楽しく，魅力的で，社会に役立つ学問です．

私は「賢いソフトウェア」を開発するための理論と実装技術に興味をもっています．今日は，その中の一つである「SAT」について紹介します．名古屋大学で皆さんと一緒に研究できる日を楽しみに待っています．

SAT と SAT ソルバー

命題論理の充足可能性判定問題 (SAT; “さっと”と読む，Boolean SATisfiability の略) は，与えられた命題論理式の充足可能性を判定する問題です．SAT は最初に NP 完全性が証明された問題であり，人工知能および計算機工学における最も基本的な問題として知られています．SAT 問題を解くプログラムのことを SAT ソルバーといいます．

最近では，チューリング賞受賞者 Donald E. Knuth 先生の有名な教科書「The Art of Computer Programming」の分冊 (Volume 4, Fascicle 6, 2015年出版) でも，分冊丸ごと300ページ以上を使って SAT が紹介されています．

SAT 技術の進化

SAT ソルバーをはじめとする SAT 技術は，最新の高性能計算機アーキテクチャを背景に大規模な計算問題を解くアプローチとして21世紀以降劇的な進化を遂げています．SAT 技術はハードウェアやソフトウェアの検証など様々な分野に応用されており，身近なところでは，インテル社のi7プロセッサの設計，統合開発環境 Eclipse のコンポーネント間の依存解析，Linux のパッケージ管理システムなどに使われています．

もっと知りたい君へ

SAT の基礎から応用事例，関連技術までをわかりやすく解説した記事(全7篇)が情報処理学会の会誌「情報処理」に掲載されています．

パズル好きの君へ

数独とナンバーリンクを例に，パズルを SAT ソルバーで解く手法を紹介しています．パズルを SAT に翻訳する方法が丁寧に説明されていて，SAT 入門としても良いです．この記事を読んで，ギネス世界記録に認定された巨大数独に挑戦してみませんか？

投稿者の情報

情報システム学専攻SATソルバー, 教員紹介, 情報システム学専攻, コンピュータ科学科, 情報システム系

Posted by banbara@i.nagoya-u.ac.jp