Miyuki Koshimura

article

N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT

Aolong Zha, Miyuki Koshimura, Hiroshi Fujita

Constraints > 2019 > 24 > 2 > 133-161

Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is N P $\mathcal {N}\mathcal {P}$ -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...

article

Improved WPM encoding for coalition structure generation under MC-nets

Xiaojuan Liao, Miyuki Koshimura, Kazuki Nomoto, Suguru Ueda, more

Constraints > 2019 > 24 > 1 > 25-55

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

chapter

Minimal Model Generation with Factorization and Constrained Search

Miyuki Koshimura, Megumi Kita, Ryuzo Hasegawa

Lecture Notes in Computer Science > PRICAI 2000 Topics in Artificial Intelligence > Posters > 793-793

The notion of minimal models is important in a wide range of areas such as logic programming, deductive databases, software verification, and hypothetical reasoning. Some applications in such areas would actually need to generate Herbrand minimal models of a given set of first-order clauses.

chapter

MGTP: A parallel theorem prover based on lazy model generation

Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita

Lecture Notes in Computer Science > Automated Deduction—CADE-11 > 776-780

We have implemented a model-generation based parallel theorem prover in KL1 on a parallel inference machine, PIM. We have developed several techniques to improve the efficiency of forward reasoning theorem provers based on lazy model generation. The tasks of the model-generation based prover are the generation and testing of atoms to be the elements of a model for the given theorem. The problem with...

chapter

Embedding negation as failure into a model generation theorem prover

Katsumi Inoue, Miyuki Koshimura, Ryuzo Hasegawa

Lecture Notes in Computer Science > Automated Deduction—CADE-11 > 400-415

Here, for the first time, we give an implementation which computes answer sets of every class of (function-free) logic programs and deductive databases containing both negation as failure and classical negation. The proposal is based on bottom-up, incremental, backtrack-free computation of the minimal models of positive disjunctive programs, together with integrity constraints over beliefs and disbeliefs...

chapter

A Model Generation Based Theorem Prover MGTP for First-Order Logic

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Yasuyuki Shirai

Lecture Notes in Computer Science > Computational Logic: Logic Programming and Beyond > Automated Reasoning > 178-213

This paper describes the major results on research and development of a model generation theorem prover MGTP. It exploits OR parallelism for non-Horn problems and AND parallelism for Horn problems achieving more than a 200-fold speedup on a parallel inference machine PIM with 256 processing elements. With MGTP, we succeeded in proving difficult mathematical problems that cannot be proven on sequential...

chapter

Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura

Lecture Notes in Computer Science > Automated Deduction—CADE-14 > 176-190

We present a new method, called non-Horn magic sets (NHM), to enhance forward reasoning provers by combining top-down and bottom-up computations. This method is a natural extension of Horn magic sets and is applicable to range-restricted non-Horn clauses. We show two types of transformations to get non-Horn magic sets from the given clause sets: breadth-first NHM and depth-first NHM. The first transformation...

chapter

Related Word Extraction Algorithm for Query Expansion – An Evaluation

Tetsuya Oishi, Tsunenori Mine, Ryuzo Hasegawa, Hiroshi Fujita, more

Studies in Computational Intelligence > Advances in Practical Multi-Agent Systems > Agent-Based Collaboration, Coordination and Decision Support > 33-48

When searching for information a user wants, search engines often return lots of results unintended by the user. Query expansion is a promising approach to solve this problem. In the query expansion research, one of the biggest issues is to generate appropriate keywords representing the user’s intention. The Related Word Extraction Algorithm (RWEA) we proposed extracts such keywords for the query...

chapter

Model Generation with Boolean Constraints

Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa

Lecture Notes in Computer Science > Logic for Programming, Artificial Intelligence, and Reasoning > Experimental Papers > 299-308

We present a simple method for eliminating redundant searches in model generation. The method employs Boolean Constraints which are conjunctions of ground instances of clauses having participated in proofs. Boolean Constraints work as sets of lemmas with which duplicate subproofs and irrelevant model extensions can be eliminated. The method has been tentatively implemented on a constraint logic programming...

chapter

Proof Simplification for Model Generation and Its Applications

Miyuki Koshimura, Ryuzo Hasegawa

Lecture Notes in Computer Science > Logic for Programming and Automated Reasoning > Theorem proving > 96-113

Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

chapter

Efficient Minimal Model Generation Using Branching Lemmas

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura

Lecture Notes in Computer Science > Automated Deduction - CADE-17 > Session 4: > 184-199

An efficient method for minimal model generation is presented. The method employs branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models. This method is applicable to other approaches such as Bry’s complement splitting and constrained search or Niemelä’s groundedness test, and greatly improves their efficiency. We...

chapter

Abstract Model Generation for Preprocessing Clause Sets

Miyuki Koshimura, Mayumi Umeda, Ryuzo Hasegawa

Lecture Notes in Computer Science > Logic for Programming, Artificial Intelligence, and Reasoning > 67-78

model generation refers to model generation for abstract clause sets in which arguments of atoms are ignored. We give two abstract clause sets which are obtained from normal clause sets. One is for checking satisfiability of the original normal clause set. Another is used for eliminating unnecessary clauses from the original one. These abstract clause sets are propositional, i.e. decidable. Thus,...

chapter

MGTP: A model generation theorem prover — Its advanced features and applications —

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura

Lecture Notes in Computer Science > Automated Reasoning with Analytic Tableaux and Related Methods > 1-15

This paper outlines a parallel model-generation based theorem-proving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes...

chapter

Personalized Search Using ODP-based User Profiles Created from User Bookmark

Tetsuya Oishi, Yoshiaki Kambara, Tsunenori Mine, Ryuzo Hasegawa, more

Lecture Notes in Computer Science > PRICAI 2008: Trends in Artificial Intelligence > Regular Papers > 839-848

When searching for intended pages on the Internet, users often have a hard time to find the pages because the pages do not always come at the higher rank of searched results. The Personalized Search is a promising approach to solve this problem. In the Personalized Search, User Profiles (UPs in short) that represent interests of the users, are well used and often created from personal documents of...

chapter

Using MaxSAT to Correct Errors in AES Key Schedule Images

Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Hiroshi Fujita, more

2013 IEEE 25th International Conference on Tools with Artificial Intelligence > 284 - 291

2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI)

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 havebeen devoted to reconstructing the original data from a corrupted version of AES key schedules, based...

chapter

Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers

Toru Ogawa, Yangyang Liu, Ryuzo Hasegawa, Miyuki Koshimura, more

2013 IEEE 25th International Conference on Tools with Artificial Intelligence > 9 - 17

2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI)

Totalizer (TO) by Bailleux et al. and Half Sorting Network (HS) by Asin et al. are typical CNF encoding methods of cardinality constraint. The former is based on unary adder, while the latter is based on odd-even merge. Although TO is inferior to HS in terms of the number of clauses, TO is superior to HS in terms of the number of variables. We propose a new method called Modulo Totalizer (MTO) to...

chapter

Solving the Coalition Structure Generation Problem with MaxSAT

Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa

2012 IEEE 24th International Conference on Tools with Artificial Intelligence > 1 > 910 - 915

2012 IEEE 24th International Conference on Tools with Artificial Intelligence (ICTAI)

Coalition Structure Generation (CSG), a main research issue in the domain of coalition games, involves partitioning agents into exhaustive and disjoint coalitions so that the social welfare is optimized. The advent of compact representation schemes, such as marginal contribution networks (MC-nets), promotes the efficiency of solving the CSG problem. In this paper, inspired by the dramatic speed-up...

chapter

Rule Extraction from Micro-Blog Using Inductive Logic Programming

Noriaki Chikara, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa

2012 Spring Congress on Engineering and Technology > 1 - 4

2012 Spring Congress on Engineering and Technology (S-CET)

Information recommender system attempts to present information that is likely to be useful for the user. Some information recommender systems recommend persons which users are likely to follow in Twitter. Showing recommendation reason is an important role of the systems. However, current recommender systems give only simple or quantitative reasons for the recommendation. In this paper, we aim at giving...

chapter

An efficient hybrid particle swarm optimization for the Job Shop Scheduling Problem

Xue-Feng Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa

2011 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE 2011) > 622 - 626

2011 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE)

This paper proposes a hybrid particle swarm optimization algorithm for solving Job Shop Scheduling Problems (JSSP) to minimize the maximum makespan. A new hybrid heuristic, based on Particle Swarm Optimization (PSO), Tabu Search (TS) and Simulated Annealing (SA), is presented. PSO combines local search (by self-experience) with global search (by neighboring experience), achieving a high search efficiency...

chapter

Hybrid Particle Swarm Optimization with parameter selection approaches to solve Flow Shop Scheduling Problem

Xue-Feng Zhang, Xuanye An, Miyuki Koshimura, Hiroshi Fujita, more

2011 IEEE 10th International Conference on Cybernetic Intelligent Systems (CIS) > 13 - 19

2011 IEEE 10th International Conference on Cybernetic Intelligent Systems (CIS)

A Hybrid Particle Swarm Optimization (HPSO) with parameter selection approaches is proposed to solve Flow Shop Scheduling Problem (FSSP) with the objective of minimizing makespan. The HPSO integrates the basic structure of a Particle Swarm Optimization (PSO) together with features borrowed from the fields of Tabu Search (TS), Simulated Annealing (SA). The algorithm works from a population of candidate...

INFONA - science communication portal

Search results for: Miyuki Koshimura

N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT

Improved WPM encoding for coalition structure generation under MC-nets

Minimal Model Generation with Factorization and Constrained Search

MGTP: A parallel theorem prover based on lazy model generation

Embedding negation as failure into a model generation theorem prover

A Model Generation Based Theorem Prover MGTP for First-Order Logic

Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

Related Word Extraction Algorithm for Query Expansion – An Evaluation

Model Generation with Boolean Constraints

Proof Simplification for Model Generation and Its Applications

Efficient Minimal Model Generation Using Branching Lemmas

Abstract Model Generation for Preprocessing Clause Sets

MGTP: A model generation theorem prover — Its advanced features and applications —

Personalized Search Using ODP-based User Profiles Created from User Bookmark

Using MaxSAT to Correct Errors in AES Key Schedule Images

Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers

Solving the Coalition Structure Generation Problem with MaxSAT

Rule Extraction from Micro-Blog Using Inductive Logic Programming

An efficient hybrid particle swarm optimization for the Job Shop Scheduling Problem

Hybrid Particle Swarm Optimization with parameter selection approaches to solve Flow Shop Scheduling Problem

Filter options

Publication date

Publication type

Keywords

Data set

INFONA - science communication portal

Search results for: Miyuki Koshimura

Add recipient

Sending message cancelled

Are you sure you want to cancel sending this message?

Send message

Filter options

Publication date

Date range setting

Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.

Publication type

Keywords

Data set

Reporting an error / abuse

Sending the report failed

Accessibility options