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

セミナーの日程・場所

(2015.12.16更新) おかげさまで45名もの方にご参加いただき盛況のなかでセミナーを終了することができました.ありがとうございました!

  • タイトル
    • 第9回AIツール入門講座 講座2「SATソルバーとそのアプリケーション開発について」
  • 日程
    • 2015年12月14日(月) 10:00 - 17:00
  • 場所
  • セミナー講師
    • 鍋島 英知 (山梨大学)
      • SATソルバー GlueMiniSat の開発者
      • 2011年,2013年の国際SATソルバー競技会で複数部門入賞,優勝
      • GlueMiniSat に関する研究で日本ソフトウェア科学会第28回大会高橋奨励賞 (2012年) 受賞
    • 宋 剛秀 (神戸大学)
      • SAT型制約ソルバー Scarab の開発者
      • SAT2016 (SATの理論と応用に関する国際会議) プログラム委員
      • Scarab に関する研究で日本ソフトウェア科学会第31回大会高橋奨励賞 (2014年) 受賞
  • 参加費用
    一般会員 11,000円
    学生会員 5,000円
    非会員 16,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 環境

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

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

申込み方法

参考資料

関連リンク

Author: Takehide Soh

Created: 2015-12-16 水 10:08

Emacs 24.3.1 (Org mode 8.2.10)

Validate