||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, 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..
||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, 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以下に削減できることを示した． 計算機実験では、エージェント数が３００の時、制約数は１０の７乗超から１０の５乗程度に削減、計算時間は１００秒超から１０秒以内に短縮できた．.
||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..
||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.
||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..
||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.
||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, 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..
||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..
||Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa, Abstract Model Generation for Preprocessing Clause Sets, Proc. of LPAR2004, 3452, 67-78, LNAI 3452, 2005.03.
||Miyuki Koshimura, Ryuzo Hasegawa, Model Generation with Boolean Constraints, Proc. of LPAR2001, 299-308, LNAI2250, 2001.12.
||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.
||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.
||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.
||Ryuzo Hasegawa, Miyuki Koshimura, An AND Parallelization Method for MGTP and Its Evaluation, Proc. of PASCO'94, 194-203, 1994.09.
||Miyuki Koshimura, Ryuzo Hasegawa, Modal Propositional Tableaux in a Model Generation Theorem Prover, Proc. of TABLEAUX-'94, 145-151, 1994.05.
||Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita, MGTP: A Parallel Theorem Prover Based on Lazy Model Generation, Proc. of CADE-11, 776-780, 1992.06.
||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.