人工知能学会 第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日(月) 研究会終了後，引き続き第８回CSPSAT講演会が翌24日まで開催さ
れます．なお，本講演会はクローズドな講演会です．
■ 照会先：越村三幸
E-mail: sig-fpai@sanken.osaka-u.ac.jp
■ プログラム
22日（日）（10:45-17:40）
----------
セッション１（10:45-12:00)
----------
データストリーム上のオンライン型頻出飽和集合マイニング
○福田 翔士，岩沼 宏治，山本 泰生（山梨大学）
負相関ルールマイニングの高速化と関連性尺度の導入
○黒岩 健歩，岩沼 宏治，山本 泰生（山梨大学）
密度優先探索に基づくコミュニティ抽出と入札データ分析への応用
○狩山 和亮*，Marco Cuturi*，山本 章博*，久保山 哲二†，福元 健太郎†（*京都大学，†学習院大学）
----------
セッション２（13:30-14:20)
----------
ホーン規則による反マトロイドの表現と教育システム設計への応用
○吉川 和*，平井 広志*，牧野 和久†（*東京大学，†京都大学）
各種の疑似クリーク列挙アルゴリズムの実験的性能比較
○ジェイ 泓杰，大久保 好章，原口 誠（北海道大学）
----------
セッション３（14:30-15:45)
----------
移動付き編集距離のオンラインパターンマッチング
○高畠 嘉将，田部井 靖生，坂本 比呂志（九州工業大学）
移動付き編集距離に基づく曖昧検索が可能な圧縮索引
○中島 健太，前田 幸司，高畠 嘉将，坂本 比呂志（九州工業大学）
距離ベースの特徴選択指標
○申 吉浩*，Adrian Angulo†，久保山 哲二‡（*兵庫県立大学，†Universidad de Holguin Oscar Lucero Moya，‡学習院大学）
----------
セッション４（16:00-17:40)
----------
ALLSATのためのBDD構築および効率的なキャッシング技法
○戸田 貴久*，津田 宏治†（*電気通信大学，†東京大学）
Parallel Portfolio SATzilla2012
○査 澳龍，長谷川 隆三（九州大学）
DPLL型モデル計数ソルバの投射モデル計数への拡張
○鈴木 涼介，橋本 健二，酒井 正彦（名古屋大学）
制約充足問題のハイブリッド符号化に向けて
○宋 剛秀，佐古田 淳史，番原 睦則，田村 直之（神戸大学）
23日（月）（9:30-14:30）
----------
セッション５（9:30-10:45)
----------
節集合の簡単化によるMaxSATソルバーの高速化
○上村 直輝，越村 三幸，長谷川 隆三（九州大学）
重み付き部分MaxSAT問題における基数制約符号化手法の改良
長谷川 隆三，○早田 翔（九州大学）
MaxSATソルバを用いた帰納論理プログラミング
○力 規晃*，越村 三幸†，藤田 博†，長谷川 隆三†（*徳山工業高等専門学校，†九州大学）
----------
セッション６（11:00-12:15)
----------
CDCLソルバーのための軽量動的簡単化手法
○杉本 拓也，鍋島 英知（山梨大学）
CDCLソルバーにおける学習節の深さに基づく節管理戦略
○横前 菜々子，鍋島 英知（山梨大学）
SAT変換手法における充足不能コアの抽出
○渡辺 大樹，鍋島 英知（山梨大学）
----------
招待講演（13:30-14:30)
----------
モデル生成型定理証明系とSATソルバー
○長谷川 隆三（九州大学）