| 越村 三幸（こしむら みゆき） | データ更新日：2024.04.11 |
助教 ／
システム情報科学研究院
情報学部門
知能科学
| 1. | 岡本 和也, 小出 幸和, 越村 三幸, 野田 五十樹, 垂直搬送機のスケジューリング問題に対するMaxSAT の適用, 人工知能学会論文誌, https://doi.org/10.1527/tjsai.39-2_B-N64, 39, 2, 2024.03. |
| 2. | Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Fagen Li, Solving Restricted Preemptive Scheduling on Parallel Machines with SAT and PMS, Journal of Universal Computer Science, https://doi.org/10.3897/jucs.97743, 2023.08. |
| 3. | Aolong Zha, Kazuki Nomoto, Suguru Ueda, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo, Coalition Structure Generation for Partition Function Games Utilizing a Concise Graphical Representation, 20th International Conference on Principles and Practice of Multi-Agent Systems, PRIMA 2017 PRIMA 2017 Principles and Practice of Multi-Agent Systems - 20th International Conference, Proceedings, 10.1007/978-3-319-69131-2_9, 143-159, 2017.10, [URL], 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.. |
| 4. | Tomoya Sugahara, Kaito Yamashita, Nathanaël Barrot, Miyuki Koshimura, Makoto Yokoo, Robust Weighted Partial Maximum Satisfiability Problem: Challenge to Sigma2P-Complete Problem, PRICAI 2022: Trends in Artificial Intelligence - 19th Pacific Rim International Conference on Artificial Intelligence, 10.1007/978-3-031-20862-1_2, 17-31, 2022.11. |
| 5. | Sung-Ho Cho, Miyuki Koshimura, Pink Mandal, Kentaro Yahiro, Makoto Yokoo, Impossibility of weakly stable and strategy-proof mechanism, Economics Letters, https://doi.org/10.1016/j.econlet.2022.110675, 217, 2022.06. |
| 6. | Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu, Fagen Li, Modeling and Solving Scheduling in Overloaded Situations with Weighted Partial MaxSAT, Mathematical Problems in Engineering, https://doi.org/10.1155/2021/9615463, 2021, 17, 2021.07. |
| 7. | 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. |
| 8. | 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. |
| 9. | Aolong Zha, Rongxuan Gao, Qiong Chang, Miyuki Koshimura, Itsuki Noda, CNF Encodings for the Min-Max Multiple Traveling Salesmen Problem, 32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020, 10.1109/ICTAI50040.2020.00053, 285-292, 2021.01. |
| 10. | Xiaojuan Liao, Miyuki Koshimura, A comparative analysis and improvement of MaxSAT encodings for coalition structure generation under MC-nets, Journal of Logic and Computation, 10.1093/logcom/exz017, 29, 913-931, 2019.10, Coalition structure generation (CSG) is one of the main research issues in the use of coalitional games in multiagent systems and weighted partial MaxSAT (WPM) encodings, i.e. rule relation-based WPM (RWPM) and agent relation-based WPM (AWPM), which are efficient for solving the CSG problem. Existing studies show that AWPM surpasses RWPM since it achieves more compact encoding; it generates fewer variables and clauses than RWPM. However, in this paper, we focus on a special case in which the two encodings generate identical numbers of variables and clauses. Experiments show that RWPM surprisingly has a dominant advantage over AWPM, which aroused our interest. We exploit the deep-rooted reason and find that it is the redundancy when encoding transitive laws in RWPM that leads to this situation. Finally, we remove redundant clauses for transitive laws in RWPM and develop an improved RWPM with refined transitive laws to solve the CSG problem. Experiments demonstrate that refined encoding is more compact and efficient than previous WPM encodings.. |
| 11. | 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以下に削減できることを示した． 計算機実験では、エージェント数が３００の時、制約数は１０の７乗超から１０の５乗程度に削減、計算時間は１００秒超から１０秒以内に短縮できた．. |
| 12. | 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.. |
| 13. | Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Rong Huang, Wenxin Yu, Maximum Satisfiability Formulation for Optimal Scheduling in Overloaded Real-Time Systems, PRICAI 2019: 16th Pacific Rim International Conference on Artificial Intelligence, 10.1007/978-3-030-29908-8_49, 1, 618-631, 2019.08. |
| 14. | Emi Watanabe, Miyuki Koshimura, Yuko Sakurai, Makoto Yokoo, Solving Coalition Structure Generation Problems over Weighted Graph, PRIMA 2019: Principles and Practice of Multi-Agent Systems - 22nd International Conference, 10.1007/978-3-030-33792-6_21, 338-353, 2019.10. |
| 15. | 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.. |
| 16. | 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.. |
| 17. | 査 澳龍，越村 三幸，櫻井 祐子，横尾 真, 分割決定木を用いた分割関数ゲームの提携構造形成アルゴリズム, 電子情報通信学会論文誌 D, 10.14923/transinfj.2018JDP7037, J102-D, 4, 313-323, 2019.04. |
| 18. | 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. |
| 19. | 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. |
| 20. | 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.. |
| 21. | 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.. |
| 22. | 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.. |
| 23. | 小川徹, 劉洋洋, 長谷川 隆三, 越村 三幸, 藤田 博, Modulo 計算に基づく基数制約のCNF符号化方式の提案と評価, システム情報科学紀要, 18, 2, 85-92, 2013.07. |
| 24. | 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. |
| 25. | 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. |
| 26. | 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. |
| 27. | 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. |
| 28. | 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. |
| 29. | 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. |
| 30. | 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. |
| 31. | 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. |
| 32. | 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. |
| 33. | 力 規晃，越村 三幸，藤田 博，長谷川 隆三, 推薦理由を考慮した情報推薦システム, システム情報科学紀要, 16, 2, 75-81, 2011.09. |
| 34. | 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.. |
| 35. | 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. |
| 36. | 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. |
| 37. | 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. |
| 38. | 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. |
| 39. | 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. |
| 40. | 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. |
| 41. | 矢野 明浩，中村 徹，長谷川 隆三，藤田 博，越村 三幸, 極小モデル生成器MiniMGの試作, 九州大学大学院システム情報科学紀要, 15, 2, 91-98, 2010.09. |
| 42. | Noriaki Chikara, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa, Rule Extraction from Blog Using Inductive Logic Programming, Proc. of WEBPRESS 2010, 269-272, 2010.08. |
| 43. | 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. |
| 44. | Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05. |
| 45. | 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. |
| 46. | 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. |
| 47. | 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. |
| 48. | 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. |
| 49. | 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. |
| 50. | Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03. |
| 51. | Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12. |
| 52. | 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. |
| 53. | Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Efficient Minimal Model Generation Using Branching Lemmas, Proc. of CADE-17, 1831, 184-199, LNAI1831, 2000.06. |
| 54. | Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, MGTP: A Parallel Theorem-Proving System Based on Model Generation, Proc. of INAP98, 34-41, 1998.09. |
| 55. | 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. |
| 56. | 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. |
| 57. | Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09. |
| 58. | Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06. |
| 59. | Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa, Embedding Negation as Failure into a Model Generation Theorem Prover, Proc. of CADE-11, 400-415, 1992.06. |
| 60. | 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. |
| 61. | 大石 哲也，倉元 俊介，峯 恒憲，長谷川 隆三，藤田 博，越村 三幸, 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成, 電子情報通信学会論文誌D, J92-D, 3, 281-292, 2009.03. |
| 62. | 梅田 眞由美，越村 三幸，長谷川 隆三, 抽象モデル生成による不要節の削除, 電子情報通信学会論文誌D, J89-D, 10, 2288-2295, 2006.10. |
| 63. | Miyuki Koshimura, Megumi Iwaki, and Ryuzo Hasegawa, Minimal Model Generation with Factorization and Constrained Search, 情報処理学会論文誌, 44, 4, 1163-1172, 2003.04. |
| 64. | 新田 克己, 柴崎 真人, 安村 禎明, 長谷川 隆三, 藤田 博, 越村 三幸, 井上 克已, 白井 康之, 小松 弘, ダイアグラムに基づく法的論争支援システム, 人工知能学会論文誌, 17, 1, 32-43, 2002.01. |
| 65. | 越村 三幸、長谷川 隆三, 幅優先ノンホーンマジックセット法の完全性の証明とその応用, 情報処理学会論文誌, 42, 9, 2201-2212, 2001.09. |
| 66. | 長谷川 隆三、藤田 博、越村 三幸, 分岐補題の抽出による極小モデル生成の効率化, 人工知能学会論文誌, 16, 2, 234-245, 2001.03. |
| 67. | 越村 三幸、長谷川 隆三, 証明の依存性解析によるモデル生成法の冗長探索の削除, 人工知能学会誌, 15, 6, 1064-1073, 2000.11. |
| 68. | 長谷川 隆三，井上 克已，太田 好彦，越村 三幸, 上昇型定理証明の探索効率を高めるノンホーンマジックセット, 情報処理学会論文誌, 38, 3, 453-456, 1997.03. |
| 69. | 長谷川 隆三，越村 三幸，井上 克已，太田 好彦, 上昇型定理証明のためのノンホーン・マジックセット, 九州大学大学院システム情報科学研究科報告, 1, 1, 85-90, 1996.09. |
| 70. | 長谷川 隆三，越村 三幸，藤田 博, ボトムアップ定理証明器の効率的アルゴリズムとその評価, 情報処理学会論文誌, 36, 3, 531-541, 1995.03. |
| 71. | 佐藤 裕幸，越村 三幸，近山 隆，藤瀬 哲朗，松尾 正治，和田 久美子, PIMOSの資源管理方式, 情報処理学会論文誌, 30, 12, 1646-1655, 1989.12. |
| 72. | 越村 三幸，長谷川 隆三, モデル生成型定理証明系のAND並列化方式, 電子情報通信学会論文誌 D-I, J78-D-I, 2, 531-541, 1995.02. |
| 73. | 鹿田憲秀，谷口清則，長谷川隆三，藤田博，越村三幸, DPLL型SATソルバを用いた極小モデル生成について, 九州大学大学院システム情報科学紀要, 第12巻，第2号，pp.81-86．, 2007.09. |
| 74. | 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. |
| 75. | 大森晋作，松下幸之助，長谷川隆三，藤田博，越村三幸, JavaによるSATソルバHerrsatの実装と学習節の削除法について, 九州大学大学院システム情報科学紀要, 第12巻，第1号，pp.41-47, 2007.03. |
| 76. | 松本 誉史，越村 三幸，久保山 哲二，長谷川 隆三, MGTPにおけるケース分割の重複削除手法とその評価, 九州大学大学院システム情報科学研究科報告, Vol. 2, No. 1, pp. 75-80, 1997.03. |
| 77. | 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. |
| 78. | 越村 三幸，長谷川 隆三，田中 智浩, ノンホーン・マジックセット変換節数削減手法とその評価, 九州大学大学院システム情報科学研究科報, Vol. 2, No. 2, pp. 247-252, 1997.09. |
| 79. | 長谷川 隆三，藤田 博，越村 三幸, 分岐補題導入による極小モデルの効率的生成法, 九州大学大学院システム情報科学研究科報告, Vol.4， No.2， pp.145-150, 1999.09. |
| 80. | 松下 慎，長谷川 隆三，藤田 博，越村 三幸, 畳込みと分岐補題を統合したモデル生成, 九州大学大学院システム情報科学紀要, 第7巻，第1号，pp.23-28, 2002.03. |
| 81. | 越村 三幸，長谷川 隆三, 深さ優先ノンホーンマジックセット法の完全性証明, 九州大学大学院システム情報科学紀要, 第7巻，第2号，pp.111-118, 2002.09. |
| 82. | 清水 純一，越村 三幸，藤田 博，長谷川 隆三, 一般化補題を利用したモデル生成法, 九州大学大学院システム情報科学紀要, 第8巻，第1号，pp.55-60, 2003.03. |
| 83. | 岡 雄一郎，長谷川 隆三，越村 三幸, 二分決定グラフによるモデル生成木の刈込み, 九州大学大学院システム情報科学紀要, 第8巻，第1号，pp.49-54, 2003.03. |
| 84. | 高砂 信吾，長谷川 隆三，藤田 博，越村 三幸, ユーザに特化した情報収集エージェントの作成, 九州大学大学院システム情報科学紀要, 第9巻，第1号，pp.25-30, 2004.03. |
| 85. | 大石 哲也，長谷川 隆三，藤田 博，越村 三幸, WEB検索におけるキーワード関連語提案システム, 九州大学大学院システム情報科学紀要, 第9巻，第1号，pp.19-24, 2004.03. |
| 86. | 大神茂之，清水亮，越村三幸，川村正，藤田博，長谷川隆三, 鉄道信号システムのモデル検査器ＳＰＩＮによる検証, 九州大学大学院システム情報科学紀要, 第10巻，第1号，pp.33-38, 2005.03. |
| 87. | 梅永明寛，竹下日出男，久本学，長谷川隆三，藤田博，越村三幸, キーワード関連語提案システムの精度向上と関連語を観点とした WEBページ要約文抽出について, 九州大学大学院システム情報科学紀要, 第10巻，第1号，pp.27-32, 2005.03. |
| 88. | 藤田博，長谷川隆三，越村三幸，木之下昇平，松田純一, FPGA上のSATソルバPCMGTPの改良について, 九州大学大学院システム情報科学紀要, 第10巻，第1号，pp.21-26, 2005.03. |
| 89. | 長谷川隆三，藤田博，雨宮聡史，越村三幸，雨宮真人, FUCE上のストリーム処理とその記述言語, 九州大学大学院システム情報科学紀要, 第１１巻，第１号，pp.31-38, 2006.03. |
| 90. | 雨宮聡史，長谷川隆三，藤田博，越村三幸，雨宮真人, FUCE言語とその処理系について, 九州大学大学院システム情報科学紀要, 第１１巻，第１号，pp.23-30, 2006.03. |
| 91. | 雨宮聡史，平兮亮，越村三幸，藤田博，長谷川隆三, Fuce言語HALの設計と実装, 九州大学大学院システム情報科学紀要, 第１１巻，第２号，pp.103-108, 2006.09. |
| 92. | 松田純一，越村三幸，藤田博，長谷川隆三, FPGA上のSATソルバPCMGTPへの前処理の導入, 九州大学大学院システム情報科学紀要, 第１１巻，第２号，pp.109-114, 2006.09. |
本データベースの内容を無断転載することを禁止します。
九大関連コンテンツ
QIR 九州大学学術情報リポジトリ システム情報科学研究院
システム情報科学研究院
- デバイスシミュレータを用いた論理回路のソフトエラー解析
- ハイブリッド環境下の大学図書館における学術情報サービスの構築
- A Run-Time Power Analysis Method using OS-Observable Parameters for Mobile Terminals
- Microwave-assisted magnetization reversal in a Co/Pd multilayer with perpendicular magnetic ...
- Modeling Costs of Access Control with Various Key Management Systems