ATND アテンド β PRODUCED BY RECRUIT

ログイン or 無料登録

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

日時 :
2015/12/14 (月) 10:00 ~ 17:00
会場 :
国立情報学研究所 (会議室は 12階 #1208, #1210 or 19階 #1901, #1902, #1903 で調整中です) (〒101-8430 東京都千代田区一ツ橋2-1-2)
URL :
http://kix.istc.kobe-u.ac.jp/~soh/ai-tool/
主催者 :

セミナーの日程・場所

  • タイトル
    • 第9回AIツール入門講座 
    • 講座2「SATソルバーとそのアプリケーション開発について」
  • 詳細のページはこちら
  • 日程
    • 2015年12月14日(月) 10:00 - 17:00
  • 場所
    • 国立情報学研究所
    • (会議室は 12階 #1208, #1210 or 19階 #1901, #1902, #1903 で調整中です)
    • 〒101-8430 東京都千代田区一ツ橋2-1-2
  • セミナー講師
  • 参加費用
    • JSAI非会員 16,000円
    • JSAI会員 11,000
    • 学生の方は人工知能学会に入会 (入会金1,000円,年会費4,000円) して頂くことで,実質10,000円でご参加頂けます.
  • 申込み方法
    • 以下の人工知能学会のページからお申し込みください.
    • 申込みページ
  • 主催
    • (社)人工知能学会

セミナーの概要

命題論理式の充足可能性を判定する充足可能性判定問題(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ソルバーを用いた演習
       組合せ最適化問題など
       (参加者からのこんな問題は解けるか?といった提案も歓迎します!)

申込み方法

  • 以下の人工知能学会のページから「AIツール入門講座2:SATソルバーとそのアプリケーション開発について」をお申し込みください.
  • 申込みページ
  • このコメントは全員が閲覧、すべてのログインユーザが投稿することができます

コメントを投稿するには、ログインしてください。

掲載されるイベント情報は、利用者の皆様によりご提供いただくものであり、株式会社リクルートホールディングスは本情報の正確性や内容について、一切保証するものではございません。詳しくは利用規約をご参照ください。