セミナーの日程・場所

• タイトル
  • 第9回AIツール入門講座　講座2「SATソルバーとそのアプリケーション開発について」
• 日程
  • 2015年12月14日(月) 10:00 - 17:00
• 場所
  • 国立情報学研究所
  • (会議室は 12階 #1208, #1210 もしくは 19階 #1901, #1902, #1903 で調整中です)
  • 〒101-8430 東京都千代田区一ツ橋2-1-2
  • http://www.nii.ac.jp/about/access/
• セミナー講師
  • 鍋島 英知 (山梨大学)
  • 宋 剛秀 (神戸大学)

• 参加費用

  一般会員	11,000円
  学生会員	5,000円
  非会員	16,000円

  • 学生で非会員の方は人工知能学会に入会 (入会金1,000円，年会費4,000円) して頂くことで，実質10,000円でご参加頂けます．
  • 申込み方法
  • 以下の人工知能学会のページからお申し込みください．
  • http://www.ai-gakkai.or.jp/no09_jsai_tool_introductory_course/
  • 主催
  • (社)人工知能学会

セミナーの概要

命題論理式の充足可能性を判定する充足可能性判定問題（SAT）は，約半世紀 に渡って膨大な量の研究が蓄積されてきました．特に近年SAT問題を解くプログラ ムであるSATソルバーの性能が飛躍的に向上し，様々な応用領域における推論 の基盤技術としてSAT技術は注目を集めています．

• 例えば，スケジューリング問題の未解決問題の求解，インテル社のi7プロセッ サの検証，Eclipseのコンポーネント間の依存解析にSAT技術が使われるなど， 産学両方において応用が進んでいる．
• またスタンフォード大学 Knuth 教授著 "The Art of Computer Programming" の4B巻 (2015年12月出版予定) ではSATについて318ページが割 かれ，序文には「SAT問題は，非常に多くの問題を解くためのキーであることから，明らかに “killer app” である」と述べられています．

本セミナーでは，各種組合せ問題，システム検証，プランニング，スケジュー リング，定理証明，組合せパズル等に興味がある方を対象として，ここ10数年 で性能が飛躍的に向上しているSATソルバーの仕組みとそれを用いた問題の基 本的解法，SATソルバーを用いたアプリケーション開発の基礎について説明と 演習を行います．

セミナーの対象者

• SATやSATソルバーに興味があり，各種問題の求解エンジンとして利用してみたい方．
• SATソルバー，SAT型CSPソルバーの手軽な体験を希望される方．

セミナーの内容

• 前半ではSATについての概要，SATソルバーの仕組みについて解説し，実際にSATソルバーGlueMiniSat, Sat4jを用いた問題解法を参加者に演習・体験して頂く予定です．
• 後半では離散最適化問題などの組合せ問題をSATに符号化する方法の概要を解説し，SAT型CSPソルバーScarabを用いたアプリケーション開発を参加者に演習・体験して頂く予定です．

受講に必要な PC 環境

二つの方法を考えています．

• 自分で環境を構築する場合

  • 以下を事前にインストールください
    • gcc
    • g++
    • java
    • scala (バージョン 2.11.* 以降が必要です)
  • 以下のソルバーソフトウェアも事前にインストールして，動作を確認し てください．
    • (GlueMiniSat) http://glueminisat.nabelab.org/
    • (Sat4j) http://www.sat4j.org/
    • (Scarab) http://kix.istc.kobe-u.ac.jp/~soh/scarab/

• 仮想マシンを利用する場合

  • 必要な環境を構築した仮想マシンVirtualBoxのイメージを近日中に公開する予定です．
  • 当日使用する PC に VirtualBox のインストールを受講前までにお願いします．
    • (本家) https://www.virtualbox.org
  • HDDの空き容量は 10GB 以上あることが必要です．

プログラム (予定，適宜休憩を挟む予定です)

• 10:00 - 14:00 : SATソルバー (講師: 鍋島)

  時間	内容
  10:00-11:00 (基礎)	SATソルバーの基礎
  	基本的アルゴリズム
  	最近の高速化技法
  	高度なSAT技術 (最適化，列挙，非充足コア)
  11:00-12:00 (ツールの利用方法)	SATソルバー GlueMiniSat, Sat4j の概要と使い方
  	コマンドラインから直接利用する方法
  	ライブラリとしての利用方法
  	SAT,UNSAT判定
  	モデル列挙の方法
  	非充足コアの利用
  12:00 - 13:00 昼食
  13:00-14:00 (演習)	SATソルバーを用いた演習
  	列挙，最適解など
  	(参加者からのこんな問題は解けるか?といった提案も歓迎します!)

• 14:00 - 17:00 : SAT型CSPソルバー (講師: 宋)

  時間	内容
  14:00-15:00 (基礎)	CSPとSAT型CSPソルバーの基礎
  	制約充足問題 (CSP)
  	SAT符号化
  	SATソルバーを用いたCSPの解法
  15:00-16:00 (ツールの利用方法)	SAT型CSPソルバー Scarab の概要と使い方
  	制約の書き方, 列挙, 最適化など
  16:00-17:00 (演習)	SAT型CSPソルバーを用いた演習
  	組合せ最適化問題など
  	(参加者からのこんな問題は解けるか?といった提案も歓迎します!)

申込み方法

• 以下の人工知能学会のページから「AIツール入門講座2：SATソルバーとそのアプリケーション開発について」をお申し込みください．
• http://www.ai-gakkai.or.jp/no09_jsai_tool_introductory_course/