九州大学 研究者情報
研究者情報 (研究者の方へ)入力に際してお困りですか?
基本情報 研究活動 教育活動 社会活動
越村 三幸(こしむら みゆき) データ更新日:2019.06.17

助教 /  システム情報科学研究院 情報学部門 知能科学


主な研究テーマ
自動演繹とその応用
キーワード:モデル生成法,非標準論理,推論の効率化,検証
1995.04.
並列オペレーティングシステム
キーワード:並列推論マシン 並列OS
1986.11~1990.03.
研究業績
主要原著論文
1. Xiaojuan Liao, Miyuki Koshimura, Kazuki Nomoto, Suguru Ueda, Yuko Sakurai, Makoto Yokoo, Improved WPM encoding for coalition structure generation under MC-nets, Constraints, https://doi.org/10.1007/s10601-018-9295-4, 24, 1, 25-55, 2019.01.
2. Aolong Zha, Kazuki Nomoto, Suguru Ueda, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo, Coalition Structure Generation for Partition Function Games Utilizing a Concise Graphical Representation, PRIMA 2017: Principles and Practice of Multi-Agent Systems , https://doi.org/10.1007/978-3-319-69131-2_9, 143-159, 2017.10, Coalition Structure Generation (CSG), a main research issue in the domain of coalition games, involves partitioning agents into exhaustive and disjoint coalitions to optimize the social welfare. The advent of compact representation schemes, such as Partition Decision Trees (PDTs), promotes the efficiency of solving CSG problems.

This paper studies the CSG problem for partition function games (PFGs) which are coalitional games with externalities. In PFGs, each value of a coalition depends on how the other agents are partitioned. We apply PDTs to represent PFGs and present two methods to solve CSG problems: a depth-first branch-and-bound algorithm and MaxSAT encoding.
3. Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Extending MaxSAT to Solve the Coalition Structure Generation Problem with Externalities Based on Agent Relations, IEICE TRANSACTIONS on Information and Systems, 10.1587/transinf.E97.D.1812, E97-D, 7, 1812-1821, 2014.07, Coalition Structure Generation (CSG) means partitioning agents into exhaustive and disjoint coalitions so that the sum of values of all the coalitions is maximized. Solving this problem could be facilitated by employing some compact representation schemes, such as marginal contribution network (MC-net). In MC-net, the CSG problem is represented by a set of rules where each rule is associated with a real-valued weights, and the goal is to maximize the sum of weights of rules under some constraints. This naturally leads to a combinatorial optimization problem that could be solved with weighted partial MaxSAT (WPM). In general, WPM deals with only positive weights while the weights involved in a CSG problem could be either positive or negative. With this in mind, in this paper, we propose an extension of WPM to handle negative weights and take advantage of the extended WPM to solve the MC-net-based CSG problem. Specifically, we encode the relations between each pair of agents and reform the MC-net as a set of Boolean formulas. Thus, the CSG problem is encoded as an optimization problem for WPM solvers. Furthermore, we apply this agent relation-based WPM with minor revision to solve the extended CSG problem where the value of a coalition is affected by the formation of other coalitions, a coalition known as externality. Experiments demonstrate that, compared to the previous encoding, our proposed method speeds up the process of solving the CSG problem significantly, as it generates fewer number of Boolean variables and clauses that need to be examined by WPM solver..
4. Xiaojuan Liao, Miyuki Koshimura, RYUZO HASEGAWA, Solving the Coalition Structure Generation Problem with MaxSAT, 24th International Conference on Tools with Artificial Intelligence, 910-915, 2012.12.
5. Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa, QMaxSAT: A Partial Max-SAT Solver, Journal on Satisfiability, Boolean Modeling and Computation, 8, 95-100, 2012.01, We present a partial Max-SAT solver \QMaxSAT which
uses CNF encoding of Boolean cardinality constraints.
The old version 0.1 was obtained by
adapting a CDCL based SAT solver MiniSat to manage cardinality constraints.
It was placed first in the industrial subcategory and second in the crafted
subcategory of partial Max-SAT category of the 2010 Max-SAT Evaluation.

The new version 0.2 is obtained by modifying version 0.1 to
decrease the number of clauses for the cardinality encoding.
We compare the two versions by solving Max-SAT instances taken
from the 2010 Max-SAT Evaluation..
6. Xuanye An, Miyuki Koshimura, Hiroshi Fujita and Ryuzo Hasegawa, QMaxSAT version 0.3 & 0.4, International Workshop on First-Order Theorem Proving (FTP), FTP 2011, TABLEAUX 2011 Workshops, Tutorials, and Short Papers, pp.7-15, 2011.07.
7. Miyuki Koshimura, Hidetomo Nabeshima, HIROSHI FUJITA, RYUZO HASEGAWA, Solving Open Job-Shop Scheduling Problems by SAT Encoding, IEICE TRANSACTIONS on Information and Systems, E93-D, 8 , 2316-2318, 2010.08.
8. Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, and Ryuzo Hasegawa, Minimal Model Generation with respect to an Atom Set, International Workshops on First-Order Theorem Proving (FTP), 49-59, 2009.07.
9. 梅田 眞由美,越村 三幸,長谷川 隆三, 抽象モデル生成による不要節の削除, 電子情報通信学会論文誌D, J89-D, 10, 2288-2295, 2006.10.
10. Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03.
11. Miyuki Koshimura, Megumi Iwaki, and Ryuzo Hasegawa, Minimal Model Generation with Factorization and Constrained Search, 情報処理学会論文誌, 44, 4, 1163-1172, 2003.04.
12. 越村 三幸,長谷川 隆三, 深さ優先ノンホーンマジックセット法の完全性証明, 九州大学大学院システム情報科学紀要, 第7巻,第2号,pp.111-118, 2002.09.
13. Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12.
14. 越村 三幸、長谷川 隆三, 幅優先ノンホーンマジックセット法の完全性の証明とその応用, 情報処理学会論文誌, 42, 9, 2201-2212, 2001.09.
15. 長谷川 隆三、藤田 博、越村 三幸, 分岐補題の抽出による極小モデル生成の効率化, 人工知能学会論文誌, 16, 2, 234-245, 2001.03.
16. Miyuki Koshimura, Ryuzo Hasegawa, Proof Simplification for Model Generation and Its Applications, Proc. of LPAR2000, 10.1007/3-540-44404-1_8, 1955, 96-113, LNAI1955, 2000.11.
17. 越村 三幸、長谷川 隆三, 証明の依存性解析によるモデル生成法の冗長探索の削除, 人工知能学会誌, 15, 6, 1064-1073, 2000.11.
18. 越村 三幸,長谷川 隆三,田中 智浩, ノンホーン・マジックセット変換節数削減手法とその評価, 九州大学大学院システム情報科学研究科報, Vol. 2, No. 2, pp. 247-252, 1997.09.
19. Miyuki Koshimura, Takashi Matsumoto, Hiroshi Fujita and Ryuzo Hasegawa, A Method to Eliminate Redundant Case-Splittings in MGTP, IJCAI-97 Workshop on Model Based Automated Reasonging, pp. 73-84, 1997.08.
20. Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, MGTP: A Model Generation Theorem Prover - Its Advanced Features and Applications -, Proc. of TABLEAUX'97, 1227, 1-15, 1997.05.
21. 長谷川 隆三,越村 三幸,藤田 博, ボトムアップ定理証明器の効率的アルゴリズムとその評価, 情報処理学会論文誌, 36, 3, 531-541, 1995.03.
22. 越村 三幸,長谷川 隆三, モデル生成型定理証明系のAND並列化方式, 電子情報通信学会論文誌 D-I, J78-D-I, 2, 531-541, 1995.02.
23. Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09.
24. Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05.
25. Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06.
26. Masayuki Fujita, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, Model Generation Theorem Provers on a Parallel Inference Machine, Proc. of FGCS'92, 357-375, 1992.06.
27. 佐藤 裕幸,越村 三幸,近山 隆,藤瀬 哲朗,松尾 正治,和田 久美子, PIMOSの資源管理方式, 情報処理学会論文誌, 30, 12, 1646-1655, 1989.12.
主要総説, 論評, 解説, 書評, 報告書等
1. 越村 三幸, 藤田 博, MaxSAT : SATの最適化問題への拡張 ーMaxSATソルバーの活用法ー, 情報処理, Vol.57 No.8, 2016.08.
主要学会発表等
1. 越村 三幸、佐藤 健, SATソルバーGlucoseを用いたMCS列挙, 2019年度 人工知能学会全国大会(第33回), 2019.06.
2. 越村 三幸, モデルとUnsat Coreを利用したMaxSATソルバーの試作, 2016年度 人工知能学会全国大会(第30回), 2016.06.
3. 越村 三幸, 有村 寿高, 基数制約のSAT符号化を用いたMaxSATソルバーの試作, 2014年度 人工知能学会全国大会(第28回), 2014.05.
4. 越村 三幸, 廖 暁鵑, 藤田 博, 長谷川 隆三, MaxSATの一拡張について, 第11回情報科学技術フォーラム(FIT 2012), 2012.09.
5. 越村 三幸,安 宣烨,藤田 博,長谷川 隆三, QMaxSAT: Q-dai MaxSAT ソルバー, 2011年度 人工知能学会全国大会(第25回), 2011.06.
6. 越村三幸,鍋島英知,藤田博,長谷川隆三, SAT変換による未解決ジョブショップスケジューリング問題への挑戦, スケジューリング・シンポジウム2009 講演論文集, pp.209-213, 2009.09.
7. 越村三幸,鍋島英知,藤田博,長谷川隆三, 極小モデル生成とジョブショップスケジューリング問題の解法, 日本ソフトウェア科学会 第25回大会, 2008.12.
8. 越村三幸,長谷川隆三, 抽象モデルを利用したSAT問題の前処理, 電子情報通信学会〔人工知能と知識処理〕, 2006.05.
9. 越村三幸,川村正,大神茂之,清水亮,藤田博,長谷川隆三, 鉄道信号システムの連動図と連動装置のモデル検査, 産業技術総合研究所システム検証研究センター, 2005.10.
10. Miyuki Koshimura, Megumi Kita, Ryuzo Hasegawa, Minimal Model Generation with Factorization and Constrained Search, Tableaux 2000, 2000.07.
11. Miyuki Koshimura, Ryuzo Hasegawa, A Proof of Completeness for Non-Horn Magic Sets and Its Application to Proof Condensation, Tableaux 1999, 1999.06.
12. 越村 三幸,長谷川 隆三, モデル生成型証明器上の様相命題タブロ, The Logic Programming Conference' 91, 1991.07.
作品・ソフトウェア・データベース等
1. 越村三幸, QMaxSAT: Q-dai MaxSAT ソルバー, 2010.03, [URL].
特許出願・取得
特許出願件数  0件
特許登録件数  1件
その他の優れた研究業績
2013.07, Max-SAT 2013に出場したQMaxSAT が,Partial Max-SAT部門(Industrial)で準優勝した..
2012.06, Max-SAT 2012に出場したQMaxSAT が,Partial Max-SAT部門(Industrial)と(Crafted)で優勝した..
2011.06, Max-SAT 2011(Max-SATソルバーの国際コンペ)に出場したQMaxSAT(Q-dai MaxSAT ソルバー)が,Partial Max-SAT部門(Industrial)で優勝,同部門(Crafted)で準優勝した..
2010.07, Max-SAT 2010(Max-SATソルバーの国際コンペ)に出場したQMaxSAT(Q-dai MaxSAT ソルバー)が,Partial Max-SAT部門(Industrial)で優勝,同部門(Crafted)で準優勝した..
学会活動
所属学会名
電子情報通信学会
人工知能学会
情報処理学会
ソフトウェア科学会
学協会役員等への就任
2014.04~2016.03, 人工知能学会 , 人工知能基本問題研究会 幹事.
学会大会・会議・シンポジウム等における役割
2018.03.16~2018.03.17, 人工知能学会 第106回人工知能基本問題研究会, 座長(Chairmanship).
2016.06.06~2016.06.09, 2016年度人工知能学会全国大会(第30回), 座長(Chairmanship).
2015.03.22~2015.03.23, 人工知能学会 第97回人工知能基本問題研究会, 座長(Chairmanship).
2014.11.23~2014.11.23, Workshop on Graph-based Algorithms for Big Data and its Applications (GABA2014), 座長(Chairmanship).
2014.03.04~2014.03.05, 火の国情報シンポジウム2014, 座長(Chairmanship).
2013.06.04~2013.06.07, 2013年度人工知能学会全国大会(第27回), 座長(Chairmanship).
2012.06.12~2012.06.15, 2012年度人工知能学会全国大会(第26回), 座長(Chairmanship).
2011.06.01~2011.06.03, 2011年度人工知能学会全国大会(第25回), 座長(Chairmanship).
2015.05.30~2015.06.02, 2015年度 人工知能学会全国大会(第29回), オーガナイザ(SAT技術の理論,実装,応用).
2014.11.23~2014.11.23, Workshop on Graph-based Algorithms for Big Data and its Applications (GABA2014), Program Committee.
2014.05.12~2014.05.15, 2014年度 人工知能学会全国大会(第28回), オーガナイザ(SAT技術の理論,実装,応用).
2013.06.04~2013.06.07, 2013年度 人工知能学会全国大会(第27回), オーガナイザ(SAT技術の理論,実装,応用).
2012.06.12~2012.06.15, 2012年度 人工知能学会全国大会(第26回), オーガナイザ(SAT技術の理論,実装,応用).
学術論文等の審査
年度 外国語雑誌査読論文数 日本語雑誌査読論文数 国際会議録査読論文数 国内会議録査読論文数 合計
2019年度
2018年度
2017年度
2016年度
2015年度
2014年度
2013年度
2012年度
2011年度
2010年度
2008年度
2007年度
2006年度
2003年度
その他の研究活動
海外渡航状況, 海外での教育研究歴
29th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2017), UnitedStatesofAmerica, 2017.11~2017.11.
PRIMA 2017: Principles and Practice of Multi-Agent Systems, France, 2017.10~2017.11.
24th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2012), Greece, 2012.11~2012.11.
FTP 2011: International Workshop on First-Order Theorem Proving, Switzerland, 2011.07~2011.07.
2010 IEEE / WIC / ACM International Conferences on Web Intelligence and Intelligent Agent Technology, Canada, 2010.07~2010.08.
FTP 2009: International Workshop on First-Order Theorem Proving, Norway, 2009.07~2009.07.
LPAR 2004: 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, ウルグアイ, 2005.03~2005.03.
LPAR 2001: 8th International Conference on Logic for Programming, Artifical Intelligence and Reasoning,, Cuba, 2001.12~2001.12.
LPAR 2000: 7th International Conference on Logic for Programming and Automated Reasoning, France, 2000.11~2000.11.
PRICAI2000, Australia, 2000.08~2000.09.
TABLEAUX 2000, UnitedKingdom, 2000.07~2000.07.
TABLEAUX'99, UnitedStatesofAmerica, 1999.06~1999.06.
University of Karlsruhe, Germany, 1997.11~1997.11.
外国人研究者等の受入れ状況
2010.02~2010.02, 2週間未満, Chalmers University of Technology, Sweden, Sweden, 学内資金.
2010.02~2010.02, 2週間未満, Chalmers University of Technology, Sweden, Germany, 学内資金.
受賞
ISC(International Supercomputing Conference) Award, ISC Award Committee, 2007.06.
研究資金
科学研究費補助金の採択状況(文部科学省、日本学術振興会)
2017年度~2019年度, 基盤研究(C), 分担, Ramsey数に関する計算科学的研究.
2016年度~2018年度, 基盤研究(C), 代表, 推論・学習機能を備えた実験候補推薦システムの研究開発.
2013年度~2015年度, 基盤研究(C), 代表, 基数制約を用いたSATソルバーの拡張とその応用に関する研究.
2013年度~2015年度, 基盤研究(C), 分担, 大規模組合せ最適化問題のEPR解法に関する研究.
2010年度~2012年度, 萌芽研究, 分担, 超高性能自動推論システムのための高抽象度機能素子に関する研究.
2009年度~2011年度, 基盤研究(B), 分担, 細粒度マルチスレッド原理による言語処理系および分散並列OS構成法の研究.
2009年度~2012年度, 基盤研究(B), 分担, 大規模SAT問題解決のためのEPRプルーバーに関する研究.
2009年度~2011年度, 基盤研究(C), 代表, 個別化Web検索支援システムの開発に関する研究.
2008年度~2011年度, 基盤研究(A), 分担, 制約最適化問題のSAT変換による解法とその並列分散処理に関する研究.
2002年度~2004年度, 基盤研究(C), 分担, プラスティック・セル・アーキテクチャの言語処理系に関する研究.
2002年度~2004年度, 萌芽研究, 分担, 作動時に再構成可能な演算チップのためのソフトウェア開発技術に関する研究.
1997年度~1998年度, 国際学術研究, 分担, 超並列計算機のアーキテクチャと宣言型言語に関する研究.
1996年度~1998年度, 一般研究(B), 分担, モデル生成型定理証明に基づく分散知識情報処理システムの構築.
共同研究、受託研究(競争的資金を除く)の受入状況
2018.04~2019.03, 代表, 体外診断用医療機器により取得されたデジタル画像の新規解析法の検討.
2017.08~2018.03, 分担, 工場設備保全における軸受の異常判定システムへの人工知能の適用.
2017.07~2018.03, 代表, 体外診断用医療機器により取得されたデジタル画像の新規解析法の検討.
2015.04~2016.03, 代表, SATソルバーの性能向上および応用に関する研究.
2014.10~2015.03, 代表, SATソルバーの性能向上および応用に関する研究.
2010.05~2011.03, 分担, SATソルバおよびJavaの化学分野への適用可能性に関する検討.
2010.04~2011.03, 分担, 新しいSAT符号化法、新しいSATソルバー、及び求解困難な問題への応用に関する研究.
2009.12~2011.03, 代表, 高性能SATソルバーによる制約最適化問題の解法とその並列処理に関する研究.
2009.04~2010.03, 分担, SAT変換技術の拡張による求解困難な制約最適化問題の解法に関する研究.
2008.04~2009.03, 分担, SAT変換による制約最適化問題の限界突破.
2007.04~2008.03, 分担, 補題再利用による効率的な分散・協調SATシステムの構築に関する研究.
1995.07~1996.03, 分担, KLIC上のMGTP処理系.

九大関連コンテンツ

pure2017年10月2日から、「九州大学研究者情報」を補完するデータベースとして、Elsevier社の「Pure」による研究業績の公開を開始しました。
 
 
九州大学知的財産本部「九州大学Seeds集」