命題論理の推論技術を用いた高性能かつ柔軟な制約プログラミングシステムの実現

2013 Fiscal Year Annual Research Report

• Project/Area Number: 24300007
• Research Institution: Kobe University
• Principal Investigator: 田村 直之 神戸大学, 情報基盤センター, 教授 (60207248)
• Co-Investigator(Kenkyū-buntansha): 井上 克巳 国立情報学研究所, 大学共同利用機関等の部局等, 教授 (10252321) ; 鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848)
• Project Period (FY): 2012-04-01 – 2015-03-31
• Keywords: 制約プログラミング / 充足可能性判定問題 / 命題論理

Research Abstract

当初の研究計画に従い A. フレキシブル制約に関する研究開発，B. 動的な制約変更に関する研究開発，C. ドメイン拡張に関する研究開発，D. 応用研究開発 の4つの研究テーマについて研究を進めた．
「A. フレキシブル制約に関する研究開発」については，フレキシブル制約のSAT符号化で重要になる擬似ブール制約の符号化方法の研究，PBSugarシステムの開発，および論文発表を行った．「B. 動的な制約変更に関する研究開発」については，動的な制約変更が可能なScarabシステムの開発および論文発表を行った．「C. ドメイン拡張に関する研究開発」については，記号推論が可能な解集合プログラミングシステム上で整数上の制約記述を可能にするプロトタイプシステムを開発し，性能評価を行った．「D. 応用研究開発」については，各種問題の評価を進めた．特に，時間割問題について優れた結果を得，論文発表を行った．
また，「論理と推論の理論，実装，応用に関する合同セミナー」のERATO湊プロジェクトとの合同開催，人工知能学会全国大会オーガナイズドセッションの開催，多くの国際会議および国内学会での研究発表などを通じ，本研究課題の成果を発表した．開発したソフトウェアについてもWeb上で公開し，国内外で広く利用されている．
国際研究交流についても，ドイツ・ポツダム大学，フランス・アルトワ大学，フランス・ボルドー大学の研究者と共同研究を進めている．

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

研究実績の概要に述べたように，4つの研究テーマのいずれにおいても順調に進展しており，全般的にも計画通り順調に進展している．

Strategy for Future Research Activity

当初の研究計画に従い A. フレキシブル制約に関する研究開発，B. 動的な制約変更に関する研究開発，C. ドメイン拡張に関する研究開発，D. 応用研究開発 の4つの研究テーマについて研究を進める．

Expenditure Plans for the Next FY Research Funding

海外協力研究者の招聘を次年度に繰り越したため．
次年度に海外協力研究者の招聘を行う．

Research Products

• [Journal Article] パッキング配列問題の制約モデリングとSAT符号化 (2014)
  • Author(s): 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • Journal Title: コンピュータソフトウェア Volume: 31(1) Pages: 116-130
  • DOI: 10.11309/jssst.31.1_116
  • Peer Reviewed
• [Journal Article] Learning from Interpretation Transition (2014)
  • Author(s): Katsumi Inoue, Tony Ribeiro, and Chiaki Sakama
  • Journal Title: Machine Learning Volume: 94(1) Pages: 51-79
  • DOI: 10.1007/s10994-013-5353-8
  • Peer Reviewed
• [Journal Article] Lp-Norm Based Algorithm for Multi-Objective Distributed Constraint Optimization (2014)
  • Author(s): Tenda Okimoto, Nicolas Schwind, Maxime Clement, and Katsumi Inoue
  • Journal Title: The 13th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2014) Volume: なし Pages: 未定
  • Peer Reviewed
• [Journal Article] Modeling and Algorithm for Dynamic Multi-Objective Weighted Constraint Satisfaction Problem (2014)
  • Author(s): Tenda Okimoto, Tony Ribeiro, Maxime Clement, and Katsumi Inoue
  • Journal Title: The 6th International Conference on Agents and Artificial Intelligence (ICAART 2014) Volume: なし Pages: 未定
  • Peer Reviewed
• [Journal Article] Discriminative MO-COP Operators (2014)
  • Author(s): Nicolas Schwind, Tenda Okimoto, Tony Ribeiro, Sebastien Konieczny, Katsumi Inoue
  • Journal Title: International Joint Workshop On Optimisation In Multi-Agent Systems And Distributed Constraint Reasoning (OPTMAS-DCR) Volume: なし Pages: 未定
  • Peer Reviewed
• [Journal Article] Model and Algorithm for Dynamic Multi-Objective Distributed Optimization (2014)
  • Author(s): Maxime Clement, Tenda Okimoto, Tony Ribeiro, Katsumi Inoue
  • Journal Title: International Joint Workshop On Optimisation In Multi-Agent Systems And Distributed Constraint Reasoning (OPTMAS-DCR) Volume: なし Pages: 未定
  • Peer Reviewed
• [Journal Article] Answer Set Programming as a Modeling Language for Course Timetabling (2013)
  • Author(s): Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue and Torsten Schaub
  • Journal Title: Theory and Practice of Logic Programming Volume: 13(4-5) Pages: 783-798
  • DOI: 10.1017/S1471068413000495
  • Peer Reviewed
• [Journal Article] 直観主義線形論理型言語 LLP とそのコンパイラ処理系 (2013)
  • Author(s): 田村直之, 番原睦則
  • Journal Title: コンピュータソフトウェア Volume: 30(2) Pages: 83-89
  • DOI: 10.11309/jssst.30.2_83
  • Peer Reviewed
• [Journal Article] Abduction, Unpredictability and Garden of Eden (2013)
  • Author(s): Chiaki Sakama and Katsumi Inoue
  • Journal Title: Logic Journal of the IGPL Volume: 21(6) Pages: 980-998
  • DOI: 10.1093/jigpal/jzt015
  • Peer Reviewed
• [Journal Article] 多目的分散制約最適化問題における厳密／非厳密解法の提案 (2013)
  • Author(s): 沖本天太，櫻井祐子，横尾真，井上克巳
  • Journal Title: 電子情報通信学会論文誌 D Volume: J96-D(12) Pages: 2929-2938
  • DOI: http://search.ieice.org/bin/summary.php?id=j96-d_12_2929
  • Peer Reviewed
• [Journal Article] 分散制約最適化問題：擬似木に基づくハイブリッド型の解法の提案 (2013)
  • Author(s): 沖本天太，山本将，櫻井祐子，横尾真，井上克巳
  • Journal Title: 電子情報通信学会論文誌 D Volume: J96-D(12) Pages: 2920-2928
  • DOI: http://search.ieice.org/bin/summary.php?id=j96-d_12_2920
  • Peer Reviewed
• [Journal Article] Encoding Petri Nets in Answer Set Programming for Simulation Based Reasoning (2013)
  • Author(s): Saadat Anwar, Chitta Baral, and Katsumi Inoue
  • Journal Title: Theory and Practice of Logic Programming Volume: 13(4-5) Pages: On-line
  • DOI: http://journals.cambridge.org/downloadsup.php?file=/tlp2013023.pdf
  • Peer Reviewed
• [Journal Article] Combining Answer Set Programs for Adaptive and Reactive Reasoning (2013)
  • Author(s): Tony Ribeiro, Katsumi Inoue and Gauvain Bourgne
  • Journal Title: Theory and Practice of Logic Programming Volume: 13(4-5) Pages: On-line
  • DOI: http://journals.cambridge.org/downloadsup.php?file=/tlp2013012.pdf
  • Peer Reviewed
• [Journal Article] Aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming (2013)
  • Author(s): Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Torsten Schaub, Takehide Soh, Naoyuki Tamura and Matthias Weise
  • Journal Title: Proceedings of the Sixth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2013) Volume: なし Pages: 33-48
  • Peer Reviewed
• [Journal Article] Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems (2013)
  • Author(s): Takehide Soh, Naoyuki Tamura, and Mutsunori Banbara
  • Journal Title: Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) Volume: なし Pages: 429-436
  • DOI: 10.1007/978-3-642-39071-5_34
  • Peer Reviewed
• [Journal Article] PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding (2013)
  • Author(s): Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh
  • Journal Title: Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013) Volume: なし Pages: 1020-1027
  • DOI: 10.1109/ICTAI.2013.153
  • Peer Reviewed
• [Journal Article] On-The-Fly Lazy Clause Simplification based on Binary Resolvents (2013)
  • Author(s): Hidetomo Nabeshima, Koji Iwanuma and Katsumi Inoue
  • Journal Title: Proceedings of the 25th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2013) Volume: なし Pages: 987-995
  • DOI: 10.1109/ICTAI.2013.149
  • Peer Reviewed
• [Journal Article] AOF-Based Algorithm for Dynamic Multi-Objective Distributed Constraint Optimization (2013)
  • Author(s): Tenda Okimoto, Maxime Clement, and Katsumi Inoue
  • Journal Title: Multi-Disciplinary Trends in Artificial Intelligence: Proceedings of the 7th International Workshop (MIWAI 2013) Volume: なし Pages: 175-186
  • DOI: 10.1007/978-3-642-44949-9_17
  • Peer Reviewed
• [Journal Article] Modeling and Algorithm for Dynamic Multi-Objective Distributed Optimization (2013)
  • Author(s): Maxime Clement, Tenda Okimoto, Tony Ribeiro, and Katsumi Inoue
  • Journal Title: Principles and Practice of Multi-Agent Systems: Proceedings of the 16th International Conference (PRIMA 2013) Volume: なし Pages: 413-420
  • DOI: 10.1007/978-3-642-44927-7_29
  • Peer Reviewed
• [Journal Article] A Two-Phase Complete Algorithm for Multiobjective Distributed Constraint Optimization (2013)
  • Author(s): Alexandre Medi, Tenda Okimoto, and Katsumi Inoue
  • Journal Title: Joint Agent Workshop and Symposium 2013 (JAWS 2013) Volume: なし Pages: On-line
  • Peer Reviewed
• [Journal Article] Representation Theorems for Revision of Logic Programs (2013)
  • Author(s): Nicolas Schwind and Katsumi Inoue
  • Journal Title: Logic Programming and Nonmonotonic Reasoning: Proceedings of the 12th International Conference (LPNMR 2013) Volume: なし Pages: 485-498
  • DOI: 10.1007/978-3-642-40564-8_48
  • Peer Reviewed
• [Journal Article] Encoding Higher Level Extensions of Petri Nets in Answer Set Programming (2013)
  • Author(s): Saadat Anwar, Chitta Baral, and Katsumi Inoue
  • Journal Title: Logic Programming and Nonmonotonic Reasoning: Proceedings of the 12th International Conference (LPNMR 2013) Volume: なし Pages: 116-121
  • DOI: 10.1007/978-3-642-40564-8_12
  • Peer Reviewed
• [Journal Article] Inference and Learning of Boolean Networks using Answer Set Programming (2013)
  • Author(s): Alexandre Rocca, Tony Ribeiro, and Katsumi Inoue
  • Journal Title: The 1st International Workshop on Learning and Nonmonotonic Reasoning (LNMR 2013) Volume: なし Pages: 17-30
  • DOI: http://arxiv.org/abs/1311.4639
  • Peer Reviewed
• [Journal Article] Translating the SBGN-AF Language into Logics to Analyze Signalling Networks (2013)
  • Author(s): Adrien Rougny, Christine Froidevaux, Yoshitaka Yamamoto, and Katsumi Inoue
  • Journal Title: The 1st International Workshop on Learning and Nonmonotonic Reasoning (LNMR 2013) Volume: なし Pages: 43-54
  • DOI: http://arxiv.org/abs/1311.4639
  • Peer Reviewed
• [Journal Article] Pseudo-Tree Based Hybrid Algorithm for Distributed Constraint Optimization (2013)
  • Author(s): Tenda Okimoto, Makoto Yokoo, Yuko Sakurai, and Katsumi Inoue
  • Journal Title: The IJCAI 2013 Workshop on Distributed Constraint Reasoning (DCR 2013) Volume: なし Pages: 1-15
  • DOI: http://www.cs.nmsu.edu/~wyeoh/DCR2013/docs/paper1.pdf
  • Peer Reviewed
• [Journal Article] Learning Revised Models for Planning in Adaptive Systems (2013)
  • Author(s): Daniel Sykes, Domenico Corapi, Jeff Magee, Jeff Kramer, Alessandra Russo, and Katsumi Inoue
  • Journal Title: The 35th International Conference on Software Engineering (ICSE 2013) Volume: なし Pages: 63-71
  • DOI: http://dl.acm.org/citation.cfm?id=2486797
  • Peer Reviewed
• [Journal Article] Systems Resilience: A Challenge Problem for Dynamic Constraint-Based Agent Systems (2013)
  • Author(s): Nicolas Schwind, Tenda Okimoto, Katsumi Inoue, Hei Chan, Tony Ribeiro, Kazuhiro Minami, and Hiroshi Maruyama
  • Journal Title: The 12th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2013) Volume: なし Pages: 785-788
  • DOI: http://www.ifaamas.org/Proceedings/aamas2013/docs/p785.pdf
  • Peer Reviewed
• [Presentation] パッキング配列問題の制約モデリングとSAT符号化
  • Author(s): 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳
  • Organizer: 日本ソフトウェア科学会第30回大会
  • Place of Presentation: 東京大学
• [Presentation] Scala 上で実現されたSAT型制約プログラミングシステムのための開発ツール Scarab について
  • Author(s): 宋剛秀, 番原睦則, 田村直之, Daniel Le Berre, Stéphanie Roussel
  • Organizer: 日本ソフトウェア科学会第30回大会
  • Place of Presentation: 東京大学
• [Presentation] 正方形詰込み問題の制約モデルとSAT符号化を用いた解法
  • Author(s): 佐古田淳史, 宋剛秀, 番原睦則, 田村直之
  • Organizer: 2013年度人工知能学会全国大会
  • Place of Presentation: 富山国際会議場
• [Presentation] Answer Set Programming as a Modeling Language for Course Timetabling
  • Author(s): Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, Torsten Schaub
  • Organizer: 第16回プログラミングおよびプログラミング言語ワークショップ (PPL 2014)
  • Place of Presentation: 阿蘇の司ビラパークホテル
• [Presentation] PBSugar: Compiling Pseudo-Boolean Constraints to SAT with Order Encoding
  • Author(s): Naoyuki Tamura, Mutsunori Banbara, and Takehide Soh
  • Organizer: The 4th International Workshop on Pragmatics of SAT (PoS 2013)
  • Place of Presentation: University of Helsinki, Finland
• [Presentation] System Architecture and Implementation of a Prototyping Tool for SAT-based Constraint Programming Systems
  • Author(s): Takehide Soh, Naoyuki Tamura, Mutsunori Banbara, Daniel Le Berre, and Stéphanie Roussel
  • Organizer: The 4th International Workshop on Pragmatics of SAT (PoS 2013)
  • Place of Presentation: University of Helsinki, Finland
• [Presentation] CSPSAT Projects and their SAT Related Tools
  • Author(s): Naoyuki Tamura, Takehide Soh, Mutsunori Banbara, and Katsumi Inoue
  • Organizer: The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013)
  • Place of Presentation: University of Helsinki, Finland
• [Presentation] 最新SATソルバーへの充足不能コア抽出手法の実装
  • Author(s): 渡辺 大樹，鍋島 英知
  • Organizer: 第27回人工知能学会全国大会
  • Place of Presentation: 富山国際会議場
• [Presentation] 拡張融合法に基づく次世代SATソルバーの試作
  • Author(s): 森 淳，鍋島 英知
  • Organizer: 第27回人工知能学会全国大会
  • Place of Presentation: 富山国際会議場
• [Presentation] 動的な多目的分散制約最適化問題に関する一検討
  • Author(s): 沖本 天太，井上 克巳
  • Organizer: 人工知能学会第27回全国大会 (JSAI 2013)
  • Place of Presentation: 富山国際会議場
• [Presentation] GlueMiniSat 2.2.7: On-The-Fly Lazy Clause Simplification
  • Author(s): Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue
  • Organizer: The 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013)
  • Place of Presentation: University of Helsinki, Finland
• [Remarks] CSPSAT2プロジェクト
  • URL: http://www.edu.kobe-u.ac.jp/istc-tamlab/cspsat/