# Theory Multiset_Ordering_NP_Hard

section ‹Deciding the Generalized Multiset Ordering is NP-hard›
text ‹We prove that satisfiability of conjunctive normal forms (a NP-hard problem) can
be encoded into a multiset-comparison problem of linear size. Therefore multiset-set comparisons
are NP-hard as well.›
theory
Multiset_Ordering_NP_Hard
imports
Multiset_Ordering_More
Propositional_Formula
Weighted_Path_Order.Multiset_Extension2_Impl
begin
subsection ‹Definition of the Encoding›
text ‹The multiset-elements are either annotated variables or indices (of clauses).
We basically follow the proof in \<^cite>‹"RPO_NPC"› where these elements are encoded as terms
(and the relation is some fixed recursive path order).›