TOP

クリップ
2015/12/14(月) 10:00 開催
東京都 竹橋

SATソルバーとそのアプリケーション開発について

基本情報

日 時: 2015/12/14(月) 10:00 〜 17:00
会 場: 国立情報学研究所
住 所: 〒101-8430 東京都千代田区一ツ橋2-1-2

イベント内容

セミナーの日程・場所

  • タイトル
    • 第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 環境

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

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

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

    • 必要な環境を構築した仮想マシンVirtualBoxのイメージを近日中に公開する予定です.
    • 当日使用する PC に VirtualBox のインストールを受講前までにお願いします.
    • 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ソルバーを用いた演習
       組合せ最適化問題など
       (参加者からのこんな問題は解けるか?といった提案も歓迎します!)

申込み方法

  • Twitterでシェア
  • 0
    Facebookでシェア
  • 0
    Google+でシェア
  • 0
    はてなブックマークに追加

タグに関連するイベント

2016/12/16(金) 10:30 〜 18:30
大阪府 梅田
2016/12/10(土) 13:00 〜 18:00
東京都 西新宿五丁目

Facebookページ

dots.で申込可能なイベント