### Abstract

We consider the problem of comparing two multisets via the generalized multiset ordering. We show that the corresponding decision problem is NP-complete. To be more precise, we encode multiset-comparisons into propositional formulas or into conjunctive normal forms of quadratic size; we further prove that satisfiability of conjunctive normal forms can be encoded as multiset-comparison problems of linear size. As a corollary, we also show that the problem of deciding whether two terms are related by a recursive path order is NP-hard, provided the recursive path order is based on the generalized multiset ordering.

### License

BSD License

### Topics

- Logic/Rewriting

### Session Multiset_Ordering_NPC

- Multiset_Ordering_More
- Propositional_Formula
- Multiset_Ordering_in_NP
- Multiset_Ordering_NP_Hard
- RPO_NP_Hard

### Depends on

- A Formalization of Weighted Path Orders and Recursive Path Orders

### Auto-related entries

- A Verified Efficient Implementation of the Weighted Path Order

## Cite

×

Multiset_Ordering_NPC-AFP

    @article{Multiset_Ordering_NPC-AFP,
      author  = {René Thiemann and Lukas Schmidinger},
      title   = {The Generalized Multiset Ordering is NP-Complete},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Multiset_Ordering_NPC.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Apr 22, 2022 : Isabelle2021-1