このように,与えられた問題を論理式で表現しSATソルバーを用いて解くことから, SAT技術は現代の推論システムにおいて基盤的役割を果たしているといえる. 本特集では,こうしたSAT技術の最近の動向を踏まえ, SATソルバー技術とその応用技術,またSATを拡張・発展させた問題について, 第一線の研究者による解説を行うことを目指した.
このために本特集では,平成20--23年度科学研究費補助金基盤研究(A) 「制約最適化問題のSAT変換による解法とその並列分散処理に関する研究」 (No.20240003,代表: 田村直之)に参加している研究者に執筆を依頼した.
本特集は8篇の解説から構成されている. まず,井上・田村による「SATソルバーの基礎」では,SATの基礎理論および DPLLを始めとするSAT問題を解くための代表的なアルゴリズムについて解説し, この分野の研究動向について概観する. 続く,鍋島氏と宋氏による「高速SATソルバーの原理」では,最新のSATソルバーで 用いられている技術について解説する. とくに,高速SATソルバーとしてよく使われているMiniSatで用いられている 技術として,矛盾からの節学習,リテラル監視,リスタート,変数選択ヒューリ スティクスについて解説する.
田村および番原氏と丹生氏による「制約最適化問題とSAT符号化」では, グラフ彩色問題を例題として,制約充足問題に対する各種SAT符号化手法を解説し, 各種符号化の違いと特徴,性能評価結果について述べる.
また,岩沼氏と鍋島氏による「SMT: 個別理論を取り扱うSAT技術」では, 各種の応用・個別理論に最適化された背景理論付きSAT (Satisfiability Modulo Theories; SMT)について解説する. これは,等式,算術,配列,リスト,ビット列などの各種の個別理論に, SAT証明法/決定手続きを拡張して適用する技術であり,近年多くの研究がなされている.
SAT問題が充足可能である場合,問題の解はモデルとして与えられる. 長谷川氏,藤田氏および越村氏による「モデル列挙とモデル計数」では, モデル生成,極小モデル生成,モデル列挙およびモデル計数に関して解説を行う.
一般に命題式のモデルの個数を数え上げる問題は #SATと呼ばれ,確率的推論に 関する問題が #SAT問題に変換できることからも注目されている. さらに,SATソルバーの研究が近年大きく発展したことを受けて, SATの枠組みを多方面に拡張する試みも盛んになりつつある. 平山氏と横尾氏による「*-SAT: SATの拡張」では,(重み付き)MaxSAT, 限量ブール式におけるQSAT,分散SAT等, SATの重要な拡張およびソルバーについて述べる.
SATソルバーの性能が近年飛躍的に向上したことにより, SAT技術の多分野への応用も急速に拡大している. 鍋島氏による「SATによるプランニングとスケジューリング」では, SAT技術の適用が有効なAIへの応用として, プランニングおよびスケジューリングのSAT符号化に基づく手法について述べる.
また工学的な実問題への応用として,番原氏と田村による「SATによるシステム検証」 では,SAT変換を利用した新しい検査技術である有界モデル検査について述べ, さらにSATを用いたテストケース自動生成について実験を交えた解説を行う.
なお,SAT技術がこれほど注目されているにもかかわらず,人工知能学会誌に限らず 日本の学会誌においては,SATの基礎から応用までを含むまとまった解説が これまで皆無だったと思われる.このため,本特集で取り上げるトピックスについては, 基礎から応用まで含めるように配慮しつつも,理論や応用の詳細に立ち入り過ぎる ことは避け,多くの読者を対象としてできるだけ平易な解説を心掛けた. さらにいずれの解説も,掲載する内容については最新の文献を基に, 執筆者間で議論を重ねたうえで外せない最重要なものを精選した. 読者には,まず井上・田村論文で概要を把握した後に, 各論を読んでいただくことをお勧めする.SATというシンプルな問題が, 無限の広がりを持っていることが改めて理解していただけると思う. 本特集が,この分野の専門家のみならず他の分野の研究者・技術者・学生など 多くの方々の一助となり,ますます重要性を増してきているSAT技術のさらなる 発展につながれば幸いである.