Kyushu University Academic Staff Educational and Research Activities Database
Researcher information (To researchers) Need Help? How to update
Miyuki Koshimura Last modified date:2019.07.12

Graduate School
Undergraduate School

Academic Degree
Doctor of Engineer
Field of Specialization
Automated Reasoning Systems and Their Applications
Research Interests
  • Automated Reasoning and its Applications
    keyword : model generation, non-monotonic logic, efficiency of inference, verification
    1995.04Automated Resoning: (1)Developing a mechnicial theorem proving system based on model generation (2)Enhancing efficiency of model generation by using proof condensation and folding-up operations (3)Implementing modal reasoning on top of model generation (4)Verifying a railway interlocking system with a mathematical method (5)SAT solver and its applications.
  • Parallel Operating System
    keyword : parallel inference machine, parallel OS
Academic Activities
1. Xiaojuan Liao, Miyuki Koshimura, Kazuki Nomoto, Suguru Ueda, Yuko Sakurai, Makoto Yokoo, Improved WPM encoding for coalition structure generation under MC-nets, Constraints,, 24, 1, 25-55, 2019.01, 提携構造形成問題(CSG)は協力ゲーム理論の問題の一つで、エージェント集合を社会的効用が最大となるように分割する問題である. 我々は以前、CSGをMaxSAT符号化して解く解法を示した. この解法は従来の混合整数計画法を利用する手法より桁違いに速い. 本論文では、このMaxSAT符号化による制約数を削減する手法を提案した. そして理論的には、制約数を少なくとも1/4以下に削減できることを示した. 計算機実験では、エージェント数が300の時、制約数は10の7乗超から10の5乗程度に削減、計算時間は100秒超から10秒以内に短縮できた..
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 ,, 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. Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03.
10. Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12.
11. 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.
12. 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.
13. 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.
14. Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09.
15. Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05.
16. Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06.
17. 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.
Works, Software and Database
1. QMaxSAT: Q-dai MaxSAT solver
Membership in Academic Society
  • The Institute of Electronics, Information and Communication Engineers
  • Japan Society for Artificial Intelligence
  • Information Processing Society of Japan
  • Japan Society for Software and Technology