# 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 (* for executability *)
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).›

datatype Annotation = Unsigned | Positive | Negative

type_synonym 'a ms_elem = "('a × Annotation) + nat"

fun ms_elem_of_lit :: "'a × bool ⇒ 'a ms_elem" where
"ms_elem_of_lit (x,True) = Inl (x,Positive)"
| "ms_elem_of_lit (x,False) = Inl (x,Negative)"

definition vars_of_cnf :: "'a cnf ⇒ 'a list" where
"vars_of_cnf = (remdups o concat o map (map fst))"

text ‹We encode a CNF into a multiset-problem, i.e., a quadruple (xs, ys, S, NS) where
xs and ys are the lists to compare, and S and NS are underlying relations of the generalized multiset ordering.
In the encoding, we add the strict relation S to the non-strict relation NS as this is a somewhat more
natural order. In particular, the relations S and NS are precisely those that are obtained when using
the mentioned recursive path order of \<^cite>‹"RPO_NPC"›.›

definition multiset_problem_of_cnf :: "'a cnf ⇒
('a ms_elem list ×
'a ms_elem list ×
('a ms_elem × 'a ms_elem)list ×
('a ms_elem × 'a ms_elem)list)" where
"multiset_problem_of_cnf cnf = (let
xs = vars_of_cnf cnf;
cs = [0 ..< length cnf];
S = List.maps (λ i. map (λ l. (ms_elem_of_lit l, Inr i)) (cnf ! i)) cs;
NS = List.maps (λ x. [(Inl (x,Positive), Inl (x,Unsigned)), (Inl (x,Negative), Inl (x,Unsigned))]) xs
in (List.maps (λ x. [Inl (x,Positive), Inl (x,Negative)]) xs,
map (λ x. Inl (x,Unsigned)) xs @ map Inr cs,
S, NS @ S))"

subsection ‹Soundness of the Encoding›

lemma multiset_problem_of_cnf:
assumes "multiset_problem_of_cnf cnf = (left, right, S, NSS)"
shows "(∃ β. eval_cnf β cnf)
⟷ ((mset left, mset right) ∈ ns_mul_ext (set NSS) (set S))"
"cnf ≠ [] ⟹ (∃ β. eval_cnf β cnf)
⟷ ((mset left, mset right) ∈ s_mul_ext (set NSS) (set S))"
proof -
define xs where "xs = vars_of_cnf cnf"
define cs where "cs = [0 ..< length cnf]"
define NS :: "('a ms_elem × 'a ms_elem)list" where "NS = concat (map (λ x. [(Inl (x,Positive), Inl (x,Unsigned)), (Inl (x,Negative), Inl (x,Unsigned))]) xs)"
note res = assms[unfolded multiset_problem_of_cnf_def Let_def List.maps_def, folded xs_def cs_def]
have S: "S = concat (map (λ i. map (λ l. (ms_elem_of_lit l, Inr i)) (cnf ! i)) cs)"
using res by auto
have NSS: "NSS = NS @ S" unfolding S NS_def using res by auto
have left: "left = concat (map (λ x. [Inl (x,Positive), Inl (x,Negative)]) xs)"
using res by auto
let ?nsright = "map (λ x. Inl (x,Unsigned)) xs"
let ?sright = "map Inr cs :: 'a ms_elem list"
have right: "right = ?nsright @ ?sright"
using res by auto

text ‹We first consider completeness: if the formula is sat, then the lists are decreasing w.r.t. the multiset-order.›
{
assume "(∃ β. eval_cnf β cnf)"
then obtain β where sat: "eval β (formula_of_cnf cnf)" unfolding eval_cnf_def by auto
define f :: "'a ms_elem ⇒ bool" where
"f = (λ c. case c of (Inl (x,sign)) ⇒ (β x ⟷ sign = Negative))"
let ?nsleft = "filter f left"
let ?sleft = "filter (Not o f) left"
have id_left: "mset left = mset ?nsleft + mset ?sleft" by simp
have id_right: "mset right = mset ?nsright + mset ?sright" unfolding right by auto
have nsleft: "?nsleft = map (λ x. ms_elem_of_lit (x, ¬ (β x))) xs"
unfolding left f_def by (induct xs, auto)
have sleft: "?sleft = map (λ x. ms_elem_of_lit (x,β x)) xs"
unfolding left f_def by (induct xs, auto)
have len: "length ?nsleft = length ?nsright" unfolding nsleft by simp
{
fix i
assume i: "i < length ?nsright"
define x where "x = xs ! i"
have x: "x ∈ set xs" unfolding x_def using i by auto
have "(?nsleft ! i, ?nsright ! i) = (ms_elem_of_lit (x,¬ β x), Inl (x,Unsigned))"
unfolding nsleft x_def using i by auto
also have "… ∈ set NS" unfolding NS_def using x by (cases "β x", auto)
finally have "(?nsleft ! i, ?nsright ! i) ∈ set NSS" unfolding NSS by auto
} note non_strict = this
{
fix t
assume "t ∈ set ?sright"
then obtain i where i: "i ∈ set cs" and t: "t = Inr i" by auto
define c where "c = cnf ! i"
from i have ii: "i < length cnf" unfolding cs_def by auto
have c: "c ∈ set cnf" using i unfolding c_def cs_def by auto
from sat[unfolded formula_of_cnf_def] c
have "eval β (Disj (map formula_of_lit c))" unfolding o_def by auto
then obtain l where l: "l ∈ set c" and eval: "eval β (formula_of_lit l)"
by auto
obtain x b where "l = (x, b)" by (cases l, auto)
with eval have lx: "l = (x, β x)" by (cases b, auto)
from l c lx have x: "x ∈ set xs" unfolding xs_def vars_of_cnf_def by force
have mem: "(ms_elem_of_lit l) ∈ set ?sleft" unfolding sleft lx using x by auto
have "∃ s ∈ set ?sleft. (s,t) ∈ set S"
proof (intro bexI[OF _ mem])
show "(ms_elem_of_lit l, t) ∈ set S"
unfolding t S cs_def using ii l c_def
by (auto intro!: bexI[of _ i])
qed
} note strict = this

have NS: "((mset left, mset right) ∈ ns_mul_ext (set NSS) (set S))"
by (intro ns_mul_ext_intro[OF id_left id_right len non_strict strict])
{
assume ne: "cnf ≠ []"
then obtain c where c: "c ∈ set cnf" by (cases cnf, auto)
with sat[unfolded formula_of_cnf_def]
have "eval β (Disj (map formula_of_lit c))" by auto
then obtain x where x: "x ∈ set xs"
using c unfolding vars_of_cnf_def xs_def by (cases c; cases "snd (hd c)"; force)
have S: "((mset left, mset right) ∈ s_mul_ext (set NSS) (set S))"
proof (intro s_mul_ext_intro[OF id_left id_right len non_strict _ strict])
show "?sleft ≠ []"  unfolding sleft using x by auto
qed
} note S = this
note NS S
} note one_direction = this

text ‹We next consider soundness: if the lists are decreasing w.r.t. the multiset-order, then
the cnf is sat.›
{
assume "((mset left, mset right) ∈ ns_mul_ext (set NSS) (set S))
∨ ((mset left, mset right) ∈ s_mul_ext (set NSS) (set S))"
hence "((mset left, mset right) ∈ ns_mul_ext (set NSS) (set S))"
using s_ns_mul_ext by auto
also have "ns_mul_ext (set NSS) (set S) = ns_mul_ext (set NS) (set S)"
unfolding NSS set_append by (rule ns_mul_ext_NS_union_S)
finally have "(mset left, mset right) ∈ ns_mul_ext (set NS) (set S)" .
from ns_mul_ext_elim[OF this]
obtain ns_left s_left ns_right s_right
where id_left: "mset left = mset ns_left + mset s_left"
and id_right: "mset right = mset ns_right + mset s_right"
and len: "length ns_left = length ns_right"
and ns: "⋀ i. i<length ns_right ⟹ (ns_left ! i, ns_right ! i) ∈ set NS"
and s: "⋀ t. t∈set s_right ⟹ ∃s∈set s_left. (s, t) ∈ set S" by blast

text ‹This is the satisfying assignment›
define β where "β x = (ms_elem_of_lit (x,True) ∈ set s_left)" for x
{
fix c
assume ccnf: "c ∈ set cnf"
then obtain i where i: "i ∈ set cs"
and c_def: "c = cnf ! i"
and ii: "i < length cnf"
unfolding cs_def set_conv_nth by force

from i have "Inr i ∈# mset right" unfolding right by auto
from this[unfolded id_right] have "Inr i ∈ set ns_right ∨ Inr i ∈ set s_right" by auto
hence "Inr i ∈ set s_right" using ns[unfolded NSS NS_def]
unfolding set_conv_nth[of ns_right] by force
from s[OF this] obtain s where sleft: "s ∈ set s_left" and si: "(s, Inr i) ∈ set S" by auto
from si[unfolded S, simplified] obtain l where
lc: "l ∈ set c" and sl: "s = ms_elem_of_lit l" unfolding c_def cs_def using ii by blast
obtain x b where lxb: "l = (x,b)" by force
from lc lxb ccnf have x: "x ∈ set xs" unfolding xs_def vars_of_cnf_def by force
have "∃l∈set c. eval β (formula_of_lit l)"
proof (intro bexI[OF _ lc])
from sleft[unfolded sl lxb]
have mem: "ms_elem_of_lit (x, b) ∈ set s_left" by auto
have "β x = b"
proof (cases b)
case True
thus ?thesis unfolding β_def using mem by auto
next
case False
show ?thesis
proof (rule ccontr)
assume "β x ≠ b"
with False have "β x" by auto
with False mem
have "ms_elem_of_lit (x, True) ∈ set s_left"
"ms_elem_of_lit (x, False) ∈ set s_left"
unfolding β_def by auto
hence mem: "ms_elem_of_lit (x, b) ∈ set s_left" for b by (cases b, auto)

have dist: "distinct left" unfolding left
by (intro distinct_concat, auto simp: distinct_map xs_def vars_of_cnf_def cs_def intro!: inj_onI)
from id_left have "mset left = mset (ns_left @ s_left)" by auto
from mset_eq_imp_distinct_iff[OF this] dist have "set ns_left ∩ set s_left = {}" by auto
with mem have nmem: "ms_elem_of_lit (x,b) ∉ set ns_left" for b by auto
have "Inl (x, Unsigned) ∈# mset right" unfolding right using x by auto
from this[unfolded id_right]
have "Inl (x, Unsigned) ∈ set ns_right ∪ set s_right" by auto
with s[unfolded S] have "Inl (x, Unsigned) ∈ set ns_right" by auto
with ns obtain s where pair: "(s, Inl (x, Unsigned)) ∈ set NS" and sns: "s ∈ set ns_left"
unfolding set_conv_nth[of ns_right] using len by force
from pair[unfolded NSS] have pair: "(s, Inl (x, Unsigned)) ∈ set NS" by auto
from pair[unfolded NS_def, simplified] have "s = Inl (x, Positive) ∨ s = Inl (x, Negative)" by auto
from sns this nmem[of True] nmem[of False] show False by auto
qed
qed
thus "eval β (formula_of_lit l)" unfolding lxb by (cases b, auto)
qed
}
hence "eval β (formula_of_cnf cnf)" unfolding formula_of_cnf_def o_def by auto
hence "∃ β. eval_cnf β cnf" unfolding eval_cnf_def by auto
} note other_direction = this

from one_direction other_direction show "(∃ β. eval_cnf β cnf)
⟷ ((mset left, mset right) ∈ ns_mul_ext (set NSS) (set S))"
by blast
show "cnf ≠ [] ⟹ (∃ β. eval_cnf β cnf)
⟷ ((mset left, mset right) ∈ s_mul_ext (set NSS) (set S))"
using one_direction other_direction by blast
qed

lemma multiset_problem_of_cnf_mul_ext:
assumes "multiset_problem_of_cnf cnf = (xs, ys, S, NS)"
and non_trivial: "cnf ≠ []"
shows "(∃ β. eval_cnf β cnf)
⟷ mul_ext (λ a b. ((a,b) ∈ set S, (a,b) ∈ set NS)) xs ys = (True,True)"
proof -
have "(∃ β. eval_cnf β cnf) = ((∃ β. eval_cnf β cnf) ∧ (∃ β. eval_cnf β cnf))"
by simp
also have "… = (((mset xs, mset ys) ∈ s_mul_ext (set NS) (set S)) ∧ ((mset xs, mset ys) ∈ ns_mul_ext (set NS) (set S)))"
by (subst multiset_problem_of_cnf(1)[symmetric, OF assms(1)], subst multiset_problem_of_cnf(2)[symmetric, OF assms], simp)
also have "… = (mul_ext (λ a b. ((a,b) ∈ set S, (a,b) ∈ set NS)) xs ys = (True,True))"
unfolding mul_ext_def Let_def by auto
finally show ?thesis .
qed

subsection ‹Size of Encoding is Linear›

lemma size_of_multiset_problem_of_cnf: assumes "multiset_problem_of_cnf cnf = (xs, ys, S, NS)"
and "size_cnf cnf = s"
shows "length xs ≤ 2 * s" "length ys ≤ 2 * s" "length S ≤ s" "length NS ≤ 3 * s"
proof -
define vs where "vs = vars_of_cnf cnf"
have lvs: "length vs ≤ s" unfolding assms(2)[symmetric] vs_def vars_of_cnf_def o_def size_cnf_def
by (rule order.trans[OF length_remdups_leq], induct cnf, auto)
have lcnf: "length cnf ≤ s" using assms(2) unfolding size_cnf_def by auto
note res = assms(1)[unfolded multiset_problem_of_cnf_def Let_def List.maps_def, folded vs_def, simplified]
have xs: "xs = concat (map (λx. [Inl (x, Positive), Inl (x, Negative)]) vs)" using res by auto
have "length xs ≤ length vs + length vs" unfolding xs by (induct vs, auto)
also have "… ≤ 2 * s" using lvs by auto
finally show "length xs ≤ 2 * s" .
have "length ys = length (map (λx. Inl (x, Unsigned)) vs @ map Inr [0..<length cnf])" using res by auto
also have "… ≤ 2 * s" using lvs lcnf by auto
finally show "length ys ≤ 2 * s" .
have S: "S = concat (map (λi. map (λl. (ms_elem_of_lit l, Inr i)) (cnf ! i)) [0..<length cnf])"
using res by simp
have "length S = sum_list (map length cnf)"
unfolding S length_concat map_map o_def length_map
by (rule arg_cong[of _ _ sum_list], intro nth_equalityI, auto)
also have "… ≤ s" using assms(2) unfolding size_cnf_def by auto
finally show S: "length S ≤ s" .
have NS: "NS = concat (map (λx. [(Inl (x, Positive), Inl (x, Unsigned)), (Inl (x, Annotation.Negative), Inl (x, Unsigned))]) vs) @ S"
using res by auto
have "length NS = 2 * length vs + length S"
unfolding NS by (induct vs, auto)
also have "… ≤ 3 * s" using lvs S by auto
finally show "length NS ≤ 3 * s" .
qed

subsection ‹Check Executability›

value (code) "case multiset_problem_of_cnf [
[(''x'',True),(''y'',False)],              ― ‹clause 0›
[(''x'',False)],                           ― ‹clause 1›
[(''y'',True),(''z'',True)],               ― ‹clause 2›
[(''x'',True),(''y'',True),(''z'',False)]] ― ‹clause 3›
of (left,right,S,NS) ⇒ (''SAT: '', mul_ext (λ x y. ((x,y) ∈ set S, (x,y) ∈ set NS)) left right = (True,True),
''Encoding: '', left, '' >mul '', right, ''strict element order: '', S,''non-strict: '', NS)"

end
```