九州大学-研究者情報 [越村三幸 (助教) システム情報科学研究院情報学部門]

自動演繹とその応用
キーワード：モデル生成法，非標準論理，推論の効率化，検証
1995.04.

並列オペレーティングシステム
キーワード：並列推論マシン　並列OS
1986.11～1990.03.

主要原著論文

1.	岡本和也, 小出幸和, 越村三幸, 野田五十樹, 垂直搬送機のスケジューリング問題に対するMaxSAT の適用, 人工知能学会論文誌, https://doi.org/10.1527/tjsai.39-2_B-N64, 39, 2, 2024.03.
2.	Miyuki Koshimura, Emi Watanabe, Yuko Sakurai, Makoto Yokoo, Concise integer linear programming formulation for clique partitioning problems, CONSTRAINTS, 10.1007/s10601-022-09326-z, 2022.04.
3.	Miyuki Koshimura, Ken Satoh, A Simple yet Efficient MCSes Enumeration with SAT Oracles, 12th Asian Conference on Intelligent Information and Database Systems, 10.1007/978-3-030-41964-6_17, Part I, 191-201, 2020.03.
4.	Xiaojuan Liao, Miyuki Koshimura, Kazuki Nomoto, Suguru Ueda, Yuko Sakurai, Makoto Yokoo, Improved WPM encoding for coalition structure generation under MC-nets, Constraints, 10.1007/s10601-018-9295-4, 24, 1, 25-55, 2019.01, [URL], The Coalition Structure Generation (CSG) problem plays an important role in the domain of coalition games. Its goal is to create coalitions of agents so that the global welfare is maximized. To date, Weighted Partial MaxSAT (WPM) encoding has shown high efficiency in solving the CSG problem, which encodes a set of constraints into Boolean propositional logic and employs an off-the-shelf WPM solver to find out the optimal solution. However, in existing WPM encodings, a number of redundant encodings are asserted. This results in additional calculations and correspondingly incurs performance penalty. Against this background, this paper presents an Improved Rule Relation-based WPM (I-RWPM) encoding for the CSG problem, which is expressed by a set of weighted rules in a concise representation scheme called Marginal Contribution net (MC-net). In order to effectively reduce the constraints imposed on encodings, we first identify a subset of rules in an MC-net, referred as a set of freelance rules. We prove that solving the problem made up of all freelance rules can be achieved with a straightforward means without any extra encodings. Thus the set of rules requiring to be encoded is downsized. Next, we improve the encoding of transitive relations among rules. To be specific, compared with the existing rule relation-based encoding that generates transitive relations universally among all rules, I-RWPM only considers the transitivity among rules with particular relationship. In this way, the number of constraints to be encoded can be further decreased. Experiments suggest that I-RWPM significantly outperforms other WPM encodings for solving the same set of problem instances. 提携構造形成問題（CSG)は協力ゲーム理論の問題の一つで、エージェント集合を社会的効用が最大となるように分割する問題である．我々は以前、CSGをMaxSAT符号化して解く解法を示した．この解法は従来の混合整数計画法を利用する手法より桁違いに速い．本論文では、このMaxSAT符号化による制約数を削減する手法を提案した．そして理論的には、制約数を少なくとも1/4以下に削減できることを示した．計算機実験では、エージェント数が３００の時、制約数は１０の７乗超から１０の５乗程度に削減、計算時間は１００秒超から１０秒以内に短縮できた．.
5.	Aolong Zha, Miyuki Koshimura, Hiroshi Fujita, N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT, Constraints, 10.1007/s10601-018-9299-0, 24, 2, 133-161, 2019.04, [URL], Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver..
6.	Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa, Minimal model generation with respect to an atom set, 7th International Workshop on First-Order Theorem Proving, FTP 2009 CEUR Workshop Proceedings, 556, 49-59, 2009.12, This paper studies minimal model generation for SAT instances. In this study, we minimize models with respect to an atom set, and not to the whole atom set. In order to enumerate minimal models, we use an arbitrary SAT solver as a subroutine which returns models of satisfiable SAT instances. In this way, we benefit from the year-byyear progress of efficient SAT solvers for generating minimal models. As an application, we try to solve job-shop scheduling problems by encoding them into SAT instances whose minimal models represent optimum solutions..
7.	Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa, Solving open job-shop scheduling problems by SAT encoding, IEICE Transactions on Information and Systems, 10.1587/transinf.E93.D.2316, E93-D, 8, 2316-2318, 2010.01, [URL], This paper tries to solve open Job-Shop Scheduling Problems (JSSP) by translating them into Boolean Satisfiability Testing Problems (SAT). The encoding method is essentially the same as the one proposed by Crawford and Baker. The open problems are ABZ8, ABZ9, YN1, YN2, YN3, and YN4. We proved that the best known upper bounds 678 of ABZ9 and 884 of YN1 are indeed optimal. We also improved the upper bound of YN2 and lower bounds of ABZ8, YN2, YN3 and YN4..
8.	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..
9.	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.
10.	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.
11.	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..
12.	Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05.
13.	Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03.
14.	Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12.
15.	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.
16.	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.
17.	Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09.
18.	Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06.
19.	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.
20.	梅田眞由美，越村三幸，長谷川隆三, 抽象モデル生成による不要節の削除, 電子情報通信学会論文誌D, J89-D, 10, 2288-2295, 2006.10.
21.	Miyuki Koshimura, Megumi Iwaki, and Ryuzo Hasegawa, Minimal Model Generation with Factorization and Constrained Search, 情報処理学会論文誌, 44, 4, 1163-1172, 2003.04.
22.	越村三幸、長谷川隆三, 幅優先ノンホーンマジックセット法の完全性の証明とその応用, 情報処理学会論文誌, 42, 9, 2201-2212, 2001.09.
23.	長谷川隆三、藤田博、越村三幸, 分岐補題の抽出による極小モデル生成の効率化, 人工知能学会論文誌, 16, 2, 234-245, 2001.03.
24.	越村三幸、長谷川隆三, 証明の依存性解析によるモデル生成法の冗長探索の削除, 人工知能学会誌, 15, 6, 1064-1073, 2000.11.
25.	長谷川隆三，越村三幸，藤田博, ボトムアップ定理証明器の効率的アルゴリズムとその評価, 情報処理学会論文誌, 36, 3, 531-541, 1995.03.
26.	佐藤裕幸，越村三幸，近山隆，藤瀬哲朗，松尾正治，和田久美子, PIMOSの資源管理方式, 情報処理学会論文誌, 30, 12, 1646-1655, 1989.12.
27.	越村三幸，長谷川隆三, モデル生成型定理証明系のAND並列化方式, 電子情報通信学会論文誌 D-I, J78-D-I, 2, 531-541, 1995.02.
28.	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.
29.	越村三幸，長谷川隆三，田中智浩, ノンホーン・マジックセット変換節数削減手法とその評価, 九州大学大学院システム情報科学研究科報, Vol. 2, No. 2, pp. 247-252, 1997.09.
30.	越村三幸，長谷川隆三, 深さ優先ノンホーンマジックセット法の完全性証明, 九州大学大学院システム情報科学紀要, 第7巻，第2号，pp.111-118, 2002.09.

主要総説, 論評, 解説, 書評, 報告書等

全てを見る→

1.	越村三幸, 藤田博, MaxSAT : SATの最適化問題への拡張ーMaxSATソルバーの活用法ー, 情報処理， Vol.57 No.8, 2016.08.

主要学会発表等

全てを見る→

1.	越村三幸, 頂点の次数に着目したラムゼーグラフ結合の評価, 情報処理学会第86回全国大会, 2024.03.
2.	越村三幸、野田五十樹, 垂直搬送機のMaxSATによる最適スケジューリング, スケジューリング・シンポジウム2022, 2022.09.
3.	越村三幸、廖暁鵑、渡部恵海、櫻井祐子、横尾真, 推移関係を表す SAT 節の削減, 2020年度人工知能学会全国大会（第34回）, 2020.06.
4.	越村三幸、佐藤健, SATソルバーGlucoseを用いたMCS列挙, 2019年度人工知能学会全国大会（第33回）, 2019.06.
5.	越村三幸, モデルとUnsat Coreを利用したMaxSATソルバーの試作, 2016年度人工知能学会全国大会（第30回）, 2016.06.
6.	越村三幸, 有村寿高, 基数制約のSAT符号化を用いたMaxSATソルバーの試作, 2014年度人工知能学会全国大会（第28回）, 2014.05.
7.	越村三幸, 廖暁鵑, 藤田博, 長谷川隆三, MaxSATの一拡張について, 第11回情報科学技術フォーラム(FIT 2012), 2012.09.
8.	越村三幸，安宣烨，藤田博，長谷川隆三, QMaxSAT: Q-dai MaxSAT ソルバー, 2011年度人工知能学会全国大会（第25回）, 2011.06.
9.	越村三幸，鍋島英知，藤田博，長谷川隆三, SAT変換による未解決ジョブショップスケジューリング問題への挑戦, スケジューリング・シンポジウム2009　講演論文集， pp.209-213, 2009.09.
10.	越村三幸，鍋島英知，藤田博，長谷川隆三, 極小モデル生成とジョブショップスケジューリング問題の解法, 日本ソフトウェア科学会第25回大会, 2008.12.
11.	越村三幸，長谷川隆三, 抽象モデルを利用したSAT問題の前処理, 電子情報通信学会〔人工知能と知識処理〕, 2006.05.
12.	越村三幸，川村正，大神茂之，清水亮，藤田博，長谷川隆三, 鉄道信号システムの連動図と連動装置のモデル検査, 産業技術総合研究所システム検証研究センター, 2005.10.
13.	Miyuki Koshimura, Megumi Kita, Ryuzo Hasegawa, Minimal Model Generation with Factorization and Constrained Search, Tableaux 2000, 2000.07.
14.	Miyuki Koshimura, Ryuzo Hasegawa, A Proof of Completeness for Non-Horn Magic Sets and Its Application to Proof Condensation, Tableaux 1999, 1999.06.
15.	越村三幸，長谷川隆三, モデル生成型証明器上の様相命題タブロ, The Logic Programming Conference' 91, 1991.07.

作品・ソフトウェア・データベース等

1.	越村三幸, QMaxSAT: Q-dai MaxSAT ソルバー, 2010.03, [URL].

特許出願・取得

特許出願件数 1件

特許登録件数 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, 人工知能学会 , 人工知能基本問題研究会幹事.

学会大会・会議・シンポジウム等における役割

2024.08.03～2024.08.09, IJCAI 2024 (the 33rd International Joint Conference on Artificial Intelligence), Program Committee.

2024.02.20～2024.02.27, AAAI-24 (the 38th Annual AAAI Conference on Artificial Intelligence), Program Committee.

2023.08.19～2023.08.25, IJCAI 2023 (the 32nd International Joint Conference on Artificial Intelligence), Program Committee.

2022.07.02～2022.07.07, IIAI AAI 2022: 11th International Congress on Advanced Applied Informatics, Program Committee.

2022.07.23～2022.07.29, IJCAI-ECAI 2022 (the 31st International Joint Conference on Artificial Intelligence and the 25th European Conference on Artificial Intelligence), Program Committee.

2021.08.21～2021.08.26, IJCAI2021 (30th International Joint Conference on Artificial Intelligence), Program Committee.

2021.07.11～2021.07.16, IIAI AAI 2021: 10th International Congress on Advanced Applied Informatics, Program Committee.

2021.01.07～2021.01.15, IJCAI-PRICAI 2020 (29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence), Program Committee.

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技術の理論，実装，応用）.

学術論文等の審査

年度	外国語雑誌査読論文数	日本語雑誌査読論文数	国際会議録査読論文数	合計
2023年度	4	1	5	10
2022年度	6	0	9	15
2021年度	2	1	10	13
2020年度	1	1	5	7
2019年度	0	1	3	4
2018年度	2	0	0	2
2017年度	1	1	1	3
2016年度	2	0	0	2
2015年度	0	1	0	1
2014年度	1	1	2	4
2013年度	0	0	1	1
2012年度	0	0	1	1
2011年度	3	1	1	5
2010年度	0	0	1	1
2008年度	0	0	1	1
2007年度	0	1	0	1
2006年度	1	0	0	1
2003年度	0	1	0	1

海外渡航状況, 海外での教育研究歴

The 22nd International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2019), Italy, 2019.10～2019.11.

The 16th Pacific Rim International Conference on Artificial Intelligence (PRICAI 2019) , Fiji, 2019.08～2019.09.

The 29th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2017), UnitedStatesofAmerica, 2017.11～2017.11.

The 20th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2017), France, 2017.10～2017.11.

The 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.

科学研究費補助金の採択状況(文部科学省、日本学術振興会)

2019年度～2022年度, 基盤研究(B), 代表, SATオラクルを用いた問題解法とその応用.

2017年度～2019年度, 基盤研究(C), 分担, Ramsey数に関する計算科学的研究.

2016年度～2018年度, 基盤研究(C), 代表, 推論・学習機能を備えた実験候補推薦システムの研究開発.

2013年度～2015年度, 基盤研究(C), 代表, 基数制約を用いたSATソルバーの拡張とその応用に関する研究.

2013年度～2015年度, 基盤研究(C), 分担, 大規模組合せ最適化問題のEPR解法に関する研究.

2010年度～2012年度, 萌芽研究, 分担, 超高性能自動推論システムのための高抽象度機能素子に関する研究.

2009年度～2011年度, 基盤研究(B), 分担, 細粒度マルチスレッド原理による言語処理系および分散並列ＯＳ構成法の研究.

2009年度～2012年度, 基盤研究(B), 分担, 大規模SAT問題解決のためのEPRプルーバーに関する研究.

2009年度～2011年度, 基盤研究(C), 代表, 個別化Web検索支援システムの開発に関する研究.

2008年度～2011年度, 基盤研究(A), 分担, 制約最適化問題のSAT変換による解法とその並列分散処理に関する研究.

2002年度～2004年度, 基盤研究(C), 分担, プラスティック・セル・アーキテクチャの言語処理系に関する研究.

2002年度～2004年度, 萌芽研究, 分担, 作動時に再構成可能な演算チップのためのソフトウェア開発技術に関する研究.

1997年度～1998年度, 国際学術研究, 分担, 超並列計算機のアーキテクチャと宣言型言語に関する研究.

1996年度～1998年度, 一般研究(B), 分担, モデル生成型定理証明に基づく分散知識情報処理システムの構築.

共同研究、受託研究(競争的資金を除く)の受入状況

2023.08～2024.03, 代表, 物流システムの最適化に関する研究.

2019.07～2020.03, 代表, 体外診断用医療機器により取得されたデジタル画像の新規解析法の検討.

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処理系.


	※ 研究者情報全体を検索する場合は右端の「すべて」を選択して下さい。

九大関連コンテンツ