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