人工知能学会 第97回人工知能基本問題研究会(SIG-FPAI)

主査 坂本比呂志
幹事 大久保好章,鍜治伸裕,河原吉伸,越村三幸,田部井靖生
担当幹事 越村三幸

■ 開催日:2015年3月22日(日)、23日 (月)

■ 会場:別府国際コンベンションセンター B-CON PLAZA 小会議室32
〒874-0828 大分県別府市山の手町12番1号
http://www.b-conplaza.jp/access/index.htm

■ 発表申込期限:2015年2月13日(金) 17:00(締め切りました)

■ 原稿提出期限:2015年3月4日(水) 15:00

■ テーマ: 特集「命題論理の充足可能性問題SATと応用技術」および一般

■ 開催趣旨
組合せ問題の多くは,命題論理の充足可能性判定問題SATとして表現できること
が知られている.そして,SAT技術を用いた組合せ問題への取り組みが多くなさ
れている.例えば,形式的検証,人工知能,オペレーションズリサーチ,生物学,
暗号学,データマイニング,機械学習などの分野の問題への取り組みが知られて
いる.これは,ここ20年のSAT研究の理論的及び実用的な進展により,様々な分
野でSAT技術が不可欠なツールとなってきていることを示している.今回は,最
新のSAT技術はもちろん,MaxSAT,Pseudo Boolean,モデル列挙,SMT,並列分
散SAT等の次世代SAT技術,および,SATに関連の深い制約充足問題(CSP)や
BDD, ZDD, 解集合プログラミング(ASP)等に関する幅広い研究発表を募集する.
また,これに限らず,人工知能の基本問題に関する理論・技術の研究発表も歓迎
します.

■ 招待講演:
[講演] 長谷川隆三 氏 (九州大学大学院システム情報科学研究院)
□ 講演タイトル:モデル生成型定理証明系とSATソルバー
□ 概要:
本講演では、先ず、FGCSプロジェクトで産声をあげた1階述語論理の定理証明系
MGTPの研究開発の足跡を辿る。MGTPは証明手続きとして、並列論理型言語KL1
との相性の良さや単一化が不要で照合で済むという利点を考慮し、SATCHMOの
モデル生成法を採用している。次いで、SATソルバーに話題を転じ、MM-MGTP
を命題に特化したMiniMGを紹介する。MiniMGでは、極小モデル生成を特長とす
るMGTPと、学習節やリスタート等の最新のSAT技術を備えたDPLLベースのSAT
ソルバーMiniSatの融合を図っている。最後に、現在開発を進めているMaxSATソ
ルバーQMaxSatについてふれる。基数制約のCNF符号化方式として、Bailleuxらに
よるTotalizer (TO)の改良を図った、Modulo Totalizer (MTO)を開発し、さらに、重
み付きMaxSATの符号化方式として、Weighted Totalizer (WTO)、WMTOの開発を
進めている。

■ 参加費:
当研究会の聴講は無料です.
研究会資料は発表の有無に関わらず1500円(学生会員無料)です.

■ 懇親会:
3月22日(日) 研究会後 (調整中です。詳細は後日連絡いたします。)

■ その他:
3月23日(月) 研究会終了後,引き続き第8回CSPSAT講演会が翌24日まで開催さ
れます.なお,本講演会はクローズドな講演会です.

■ 照会先:越村三幸
E-mail: sig-fpai@sanken.osaka-u.ac.jp


■ プログラム

22日(日)(10:45-17:40)

----------
セッション1(10:45-12:00)
----------
データストリーム上のオンライン型頻出飽和集合マイニング
○福田 翔士,岩沼 宏治,山本 泰生(山梨大学)

負相関ルールマイニングの高速化と関連性尺度の導入
○黒岩 健歩,岩沼 宏治,山本 泰生(山梨大学)

密度優先探索に基づくコミュニティ抽出と入札データ分析への応用
○狩山 和亮*,Marco Cuturi*,山本 章博*,久保山 哲二†,福元 健太郎†(*京都大学,†学習院大学)

----------
セッション2(13:30-14:20)
----------
ホーン規則による反マトロイドの表現と教育システム設計への応用
○吉川 和*,平井 広志*,牧野 和久†(*東京大学,†京都大学)

各種の疑似クリーク列挙アルゴリズムの実験的性能比較
○ジェイ 泓杰,大久保 好章,原口 誠(北海道大学)

----------
セッション3(14:30-15:45)
----------
移動付き編集距離のオンラインパターンマッチング
○高畠 嘉将,田部井 靖生,坂本 比呂志(九州工業大学)

移動付き編集距離に基づく曖昧検索が可能な圧縮索引
○中島 健太,前田 幸司,高畠 嘉将,坂本 比呂志(九州工業大学)

距離ベースの特徴選択指標
○申 吉浩*,Adrian Angulo†,久保山 哲二‡(*兵庫県立大学,†Universidad de Holguin Oscar Lucero Moya,‡学習院大学)

----------
セッション4(16:00-17:40)
----------
ALLSATのためのBDD構築および効率的なキャッシング技法
○戸田 貴久*,津田 宏治†(*電気通信大学,†東京大学)

Parallel Portfolio SATzilla2012
○査 澳龍,長谷川 隆三(九州大学)

DPLL型モデル計数ソルバの投射モデル計数への拡張
○鈴木 涼介,橋本 健二,酒井 正彦(名古屋大学)

制約充足問題のハイブリッド符号化に向けて
○宋 剛秀,佐古田 淳史,番原 睦則,田村 直之(神戸大学)


23日(月)(9:30-14:30)

----------
セッション5(9:30-10:45)
----------
節集合の簡単化によるMaxSATソルバーの高速化
○上村 直輝,越村 三幸,長谷川 隆三(九州大学)

重み付き部分MaxSAT問題における基数制約符号化手法の改良
長谷川 隆三,○早田 翔(九州大学)

MaxSATソルバを用いた帰納論理プログラミング
○力 規晃*,越村 三幸†,藤田 博†,長谷川 隆三†(*徳山工業高等専門学校,†九州大学)

----------
セッション6(11:00-12:15)
----------
CDCLソルバーのための軽量動的簡単化手法
○杉本 拓也,鍋島 英知(山梨大学)

CDCLソルバーにおける学習節の深さに基づく節管理戦略
○横前 菜々子,鍋島 英知(山梨大学)

SAT変換手法における充足不能コアの抽出
○渡辺 大樹,鍋島 英知(山梨大学)

----------
招待講演(13:30-14:30)
----------
モデル生成型定理証明系とSATソルバー
○長谷川 隆三(九州大学)