1. |
Aolong Zha, Hiroshi Fujita, Miyuki Koshimura, N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT, *Constraints*, https://doi.org/10.1007/s1060, 24, 2, 133-161, 2019.04. |

2. |
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, 提携構造形成問題（CSG)は協力ゲーム理論の問題の一つで、エージェント集合を社会的効用が最大となるように分割する問題である． 我々は以前、CSGをMaxSAT符号化して解く解法を示した． この解法は従来の混合整数計画法を利用する手法より桁違いに速い． 本論文では、このMaxSAT符号化による制約数を削減する手法を提案した． そして理論的には、制約数を少なくとも1/4以下に削減できることを示した． 計算機実験では、エージェント数が３００の時、制約数は１０の７乗超から１０の５乗程度に削減、計算時間は１００秒超から１０秒以内に短縮できた．. |

3. |
Aolong Zha, Miyuki Koshimura, Hiroshi Fujita, A Hybrid Encoding of Pseudo-Boolean Constraints into CNF, *Conference on Technologies and Applications of Artificial Intelligence, TAAI 2017*, 10.1109/TAAI.2017.15, 9-12, 2017.12. |

4. |
Aolong Zha, Naoki Uemura, Miyuki Koshimura, HIROSHI FUJITA, Mixed Radix Weight Totalizer Encoding for Pseudo-Boolean Constraints, *29th International Conference on Tools with Artificial Intelligence*, 10.1109/ICTAI.2017.00135, 868-875, 2017.11. |

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

6. |
Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Reconstructing AES Key Schedule Images with SAT and MaxSAT, *IEICE TRANSACTIONS on Information and Systems*, 10.1587/transinf.2015EDP7223, E99D, 1, 141-150, 2016.01, Cold boot attack is a side channel attack that recovers data from memory, which persists for a short period after power is lost. In the course of this attack, the memory gradually degrades over time and only a corrupted version of the data may be available to the attacker. Recently, great efforts have been made to reconstruct the original data from a corrupted version of AES key schedules, based on the assumption that all bits in the charged states tend to decay to the ground states while no bit in the ground state ever inverts. However, in practice, there is a small number of bits flipping in the opposite direction, called reverse flipping errors. In this paper, motivated by the latest work that formulates the relations of AES key bits as a Boolean Satisfiability problem, we move one step further by taking the reverse flipping errors into consideration and employing off-the-shelf SAT and MaxSAT solvers to accomplish the recovery of AES-128 key schedules from decayed memory images. Experimental results show that, in the presence of reverse flipping errors, the MaxSAT approach enables reliable recovery of key schedules with significantly less time, compared with the SAT approach that relies on brute force search to find out the target errors. Moreover, in order to further enhance the efficiency of key recovery, we simplify the original problem by removing variables and formulas that have relatively weak relations to the whole key schedule. Experimental results demonstrate that the improved MaxSAT approach reduces the scale of the problem and recover AES key schedules more efficiently when the decay factor is relatively large.. |

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

8. |
Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, MaxSAT Encoding for MC-Net-Based Coalition Structure Generation Problem with Externalities, *IEICE TRANSACTIONS on Information and Systems*, 10.1587/transinf.E97.D.1781, E97-D, 7, 1781-1789, 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, Hui Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Using MaxSAT to Correct Errors in AES Key Schedule Images, *25th International Conference on Tools with Artificial Intelligence*, 10.1109/ICTAI.2013.51, 284-291, 2013.11. |

10. |
Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers, *25th International Conference on Tools with Artificial Intelligence*, 10.1109/ICTAI.2013.13, 9-17, 2013.11. |

11. |
HIROSHI FUJITA, Miyuki Koshimura, RYUZO HASEGAWA, SCSat: A Soft Constraint Guided SAT Solver, *16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013)*, 415-421, 2013.07. |

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

13. |
Xue-Feng Zhang, Miyuki Koshimura, HIROSHI FUJITA, RYUZO HASEGAWA, Hybrid Particle Swarm Optimization and Convergence Analysis for Scheduling Problems, *Evolutionary Computation and Multi-Agent Systems and Simulation (ECoMASS) Workshop*, 307-314, 2012.07. |

14. |
Noriacki Chikara, Miyuki Koshimura, HIROSHI FUJITA, RYUZO HASEGAWA, Rule Extraction from Micro-Blog using Inductive Logic Programming, *2012 Spring World Congress on Engineering and Technology (SCET2012)*, 2, 257-260, 2012.05. |

15. |
Yuichi Takiguchi, Koji Kurakado, Tetsuya Oishi, Miyuki Koshimura, Hiroshi Fujita, and Ryuzo Hasegawa, Evaluating Reranking Methods based on Link Co-occurence and Category in Wikipedia, *4th International Conference on Agents and Artificial Intelligence*, 1, 277-282, 2012.02. |

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

17. |
Xue-Feng Zhang, Xuanye An, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Hybrid Particle Swarm Optimization with Parameter Selection Approaches to Solve Flow Shop Scheduling Problem, *10th IEEE Internationa Conference on Cybernetic Intelligent Systems*, 13-19, 2011.09. |

18. |
Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Combining PSO and Local Search to Solve Scheduling Problems, *10th Annual Conference Companion on Genetic and Evolutionary Computation (GECCO'11)*, 347-357, 2011.07. |

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

20. |
Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita and Ryuzo Hasegawa, An Efficient Hybrid Particle Swarm Optimization for the Job Shop Scheduling Problem, *IEEE*, Proc. of 2011 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE 2011), pp.622-626, 2011.06. |

21. |
Koji Kurakado, Tetsuya Oishi, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, EVALUATING RERANKING METHODS USING WIKIPEDIA FEATURES, *Proc. of ICAART 2011*, 1, 376-381, International Conference on Agents and Artificial Intelligence, 2011.01. |

22. |
Wataru Shirakihara, Tetsuya Oishi, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, TRENDSPOTTER DETECTION SYSTEM FOR TWITTER, *Proc. of ICAART 2011*, 1, 625-628, International Conference on Agents and Artificial Intelligence, 2011.01. |

23. |
Xue-Feng Zhang, Bin Tong, Miyuki Koshimura, Hiroshi Fujita, and Ryuzo Hasegawa, A Multi-Layer Hybrid Particle Swarm Optimization Model for Flow Shop Scheduling Problem, *Australian Journal of Intelligent Information Processing Systems*, 12, 4, 1-6, 7th International Conference on Neural Information Processing (ICONIP 2010), 2010.12. |

24. |
Xue-Feng Zhang, Bin Tong, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, A Hybrid Particle Swarm Optimization Algorithm HPTS for the Flow-Shop Scheduling Problem, *九州大学大学院システム情報科学紀要*, 15, 2, 65-69, 2010.09. |

25. |
Noriaki Chikara, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Rule Extraction from Blog Using Inductive Logic Programming, *Proc. of WEBPRESS 2010*, 269-272, 2010.08. |

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

27. |
Kentaro Hori, Tetsuya Oishi, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Related Word Extraction from Wikipedia for Web Retrieval Assistance, *Proc. of ICAART 2010*, 2, 192-199, 2010.01. |

28. |
Tetsuya Oishi, Ttsnenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Related Word Extraction Algorithm for Query Expansion - an Evaluation -, *Proc. of ACCDS 2009*, 41-56, 2009.12. |

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

30. |
Tetsuya Oishi, Shunsuke Kuramoto, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, A Method for Query Expansion Using the Related Word Extraction Algorithm, *Proc. of WIRSS*, 41-44, 2008.12. |

31. |
Tetsuya Oishi, Yoshiaki Kambara, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura, Personalized Search using ODP-based User Profiles Created from User Bookmark, *Pacific Rim Int'l Conf. on Artificial Intelligence (PRICAI 2008)*, 839-848, 2008.12. |

32. |
Tetsuya Oishi, Shunsuke Kuramoto, Hiroto Nagata, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, and Miyuki Koshimura, User-Schedule-based Web Page Recommendation, *The 2007 IEEE/WIC/ACM International Conference on Web Intelligence*, pp.776-779, 2007.11. |

33. |
Satoshi Amamiya, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Ryo Hirana, and Makoto Amamiya, A Language Design for Non-Interruptable Multithreading Environment Fuce, *International Supercomputing Conference (ISC'07)*, CD, 2007.06. |

34. |
Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, *Proc. of LPAR2004*, 3452, 67-78, LNAI 3452, 2005.03. |

35. |
Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, *Proc. of LPAR2001*, 299-308, LNAI2250, 2001.12. |

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

37. |
Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Efficient Minimal Model Generation Using Branching Lemmas, *Proc. of CADE-17*, 1831, 184-199, LNAI1831, 2000.06. |

38. |
Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, MGTP: A Parallel Theorem-Proving System Based on Model Generation, *Proc. of INAP98*, 34-41, 1998.09. |

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

40. |
Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura, Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving, *Proc. of CADE-14*, 1249, 176-190, pp.176-190, 1997.07. |

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

42. |
Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, *Proc. of PASCO'94*, 194-203, 1994.09. |

43. |
Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, *Proc. of TABLEAUX-'94*, 145-151, 1994.05. |

44. |
Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, Lazy Model Generation for Improving the Efficiency of Forward Reasoning Theorem Provers, *Proc. of the Intl. Workshop on Automated Reasoning*, 192-202, 1992.07. |

45. |
Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa, Embedding Negation as Failure into a Model Generation Theorem Prover, *Proc. of CADE-11*, 400-415, 1992.06. |

46. |
Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, *Proc. of CADE-11*, 776-780, 1992.06. |

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