Theory RPO_NP_Hard

section ‹Deciding RPO-constraints is NP-hard›

text ‹We show that for a given an RPO it is NP-hard to decide whether two terms are in relation,
  following a proof in \<^cite>‹"RPO_NPC"›.›

theory RPO_NP_Hard
  imports 
    Multiset_Ordering_NP_Hard
    Weighted_Path_Order.RPO
begin

subsection ‹Definition of the Encoding›

datatype FSyms = A | F | G | H | U (* unsigned *) | P (* positive sign *) | N (* negative sign *)

text ‹We slightly deviate from the paper encoding, since we add the three constants
  @{const U}, @{const P}, @{const N} in order to be able to easily convert an encoded term
  back to the multiset-element.›

fun ms_elem_to_term :: "'a cnf ⇒ 'a ms_elem ⇒ (FSyms, 'a + nat)term" where
  (* y_i in the paper *)
  "ms_elem_to_term cnf (Inr i) = Var (Inr i)"
| (* t_x in the paper *)
  "ms_elem_to_term cnf (Inl (x, Unsigned)) = Fun F (Var (Inl x) # Fun U [] # 
        map (λ _. Fun A []) cnf)" 
  (* t+_x in the paper *)
| "ms_elem_to_term cnf (Inl (x, Positive)) = Fun F (Var (Inl x) # Fun P [] # 
        map (λ i. if (x,True) ∈ set (cnf ! i) then Var (Inr i) else Fun A []) [0 ..< length cnf])"
  (* t-_x in the paper *)
| "ms_elem_to_term cnf (Inl (x, Negative)) = Fun F (Var (Inl x) # Fun N [] # 
        map (λ i. if (x,False) ∈ set (cnf ! i) then Var (Inr i) else Fun A []) [0 ..< length cnf])"

definition term_lists_of_cnf :: "'a cnf ⇒ (FSyms, 'a + nat)term list × (FSyms, 'a + nat)term list" where
  "term_lists_of_cnf cnf = (case multiset_problem_of_cnf cnf of
       (as, bs, S, NS) ⇒
       (map (ms_elem_to_term cnf) as, map (ms_elem_to_term cnf) bs))" 

definition rpo_constraint_of_cnf :: "'a cnf ⇒ (_,_)term × (_,_)term" where
  "rpo_constraint_of_cnf cnf = (case term_lists_of_cnf cnf of
       (as, bs) ⇒ (Fun G as, Fun H bs))" 

text ‹An RPO instance where all symbols are equivalent in precedence and all symbols have
  multiset-status.›
interpretation trivial_rpo: rpo_with_assms "λ f g. (False, True)" "λ f. True" "λ _. Mul" 0
  by (unfold_locales, auto)

subsection ‹Soundness of the Encoding›

fun term_to_ms_elem :: "(FSyms, 'a + nat)term ⇒ 'a ms_elem" where
  "term_to_ms_elem (Var (Inr i)) = Inr i" 
| "term_to_ms_elem (Fun F (Var (Inl x) # Fun U _ # ts)) = Inl (x, Unsigned)" 
| "term_to_ms_elem (Fun F (Var (Inl x) # Fun P _ # ts)) = Inl (x, Positive)" 
| "term_to_ms_elem (Fun F (Var (Inl x) # Fun N _ # ts)) = Inl (x, Negative)" 
| "term_to_ms_elem _ = undefined" 

lemma term_to_ms_elem_ms_elem_to_term[simp]: "term_to_ms_elem (ms_elem_to_term cnf x) = x" 
  apply (cases x)
  subgoal for a by (cases a, cases "snd a", auto)
  by auto

lemma (in rpo_with_assms) rpo_vars_term: "rpo_s s t ∨ rpo_ns s t ⟹ vars_term s ⊇ vars_term t" 
proof (induct s t rule: rpo.induct[of _ prc prl c n], force, force)
  case (3 f ss y)
  thus ?case
    by (smt (verit, best) fst_conv rpo.simps(3) snd_conv subset_eq term.set_intros(4))
next
  case (4 f ss g ts)
  show ?case
  proof (cases "∃s∈set ss. rpo_ns s (Fun g ts)")
    case True
    from 4(1) True show ?thesis by auto
  next
    case False
    obtain ps pns where prc: "prc (f, length ss) (g, length ts) = (ps, pns)" by force
    from False have "(if (∃s∈set ss. rpo_ns s (Fun g ts)) then b else e) = e" for b e :: "bool × bool" by simp
    note res = 4(5)[unfolded rpo.simps this prc Let_def split]
    from res have rel: "∀t∈set ts. rpo_s (Fun f ss) t" by (auto split: if_splits)
    note IH = 4(2)[OF False prc[symmetric] refl]
    from rel IH show ?thesis by auto
  qed
qed


lemma term_lists_of_cnf: assumes "term_lists_of_cnf cnf = (as, bs)" 
  and non_triv: "cnf ≠ []" 
  shows "(∃ β. eval_cnf β cnf)
     ⟷ (mset as, mset bs) ∈ s_mul_ext (trivial_rpo.RPO_NS) (trivial_rpo.RPO_S)"
  "length (vars_of_cnf cnf) ≥ 2 ⟹ 
     (∃ β. eval_cnf β cnf) ⟷ (Fun G as, Fun H bs) ∈ trivial_rpo.RPO_S"
proof - 
  obtain xs ys S NS where mp: "multiset_problem_of_cnf cnf = (xs,ys,S,NS)" 
    by (cases "multiset_problem_of_cnf cnf", auto)
  from assms(1)[unfolded term_lists_of_cnf_def mp split]
  have abs: "as = map (ms_elem_to_term cnf) xs" "bs = map (ms_elem_to_term cnf) ys" by auto
  from mp[unfolded multiset_problem_of_cnf_def Let_def List.maps_def, simplified]
  have S: "S = concat (map (λi. map (λl. (ms_elem_of_lit l, Inr i)) (cnf ! i)) [0..<length cnf])" 
    and NS: "NS = concat (map (λx. [(Inl (x, Positive), Inl (x, Unsigned)), (Inl (x, Negative), Inl (x, Unsigned))]) (vars_of_cnf cnf)) @ S" 
    and ys: "ys = map (λx. Inl (x, Unsigned)) (vars_of_cnf cnf) @ map Inr [0..<length cnf]" 
    and xs: "xs = concat (map (λx. [Inl (x, Positive), Inl (x, Negative)]) (vars_of_cnf cnf))" by auto
  show one: "(∃ β. eval_cnf β cnf)
     ⟷ (mset as, mset bs) ∈ s_mul_ext (trivial_rpo.RPO_NS) (trivial_rpo.RPO_S)" 
    unfolding multiset_problem_of_cnf(2)[OF mp non_triv]
  proof
    assume "(mset xs, mset ys) ∈ s_mul_ext (set NS) (set S)" 
    hence mem: "(xs, ys) ∈ {(as, bs). (mset as, mset bs) ∈ s_mul_ext (set NS) (set S)}" by simp
    have "(as, bs) ∈ {(as, bs). (mset as, mset bs) ∈ s_mul_ext trivial_rpo.RPO_NS trivial_rpo.RPO_S}" 
      unfolding abs 
    proof (rule s_mul_ext_map[OF _ _ mem, of "ms_elem_to_term cnf"])
      {
        fix a b
        assume "(a,b) ∈ set S" 
        from this[unfolded S, simplified]
        obtain i x s where i: "i < length cnf" and a: "a = ms_elem_of_lit (x,s)" 
          and mem: "(x,s) ∈ set (cnf ! i)" and b: "b = Inr i" by auto
        from mem i obtain t ts where a: "ms_elem_to_term cnf a = Fun F (Var (Inl x) # t # ts)" and len: "length ts = length cnf" and tsi: "ts ! i = Var (Inr i)" 
          unfolding a by (cases s, auto)
        from len i tsi have mem: "Var (Inr i) ∈ set ts" unfolding set_conv_nth by auto
        show "(ms_elem_to_term cnf a, ms_elem_to_term cnf b) ∈ trivial_rpo.RPO_S" 
          unfolding a b by (simp add: Let_def, intro disjI2 bexI[OF _ mem], simp)
      } note S = this
      fix a b
      assume mem: "(a,b) ∈ set NS" 
      show "(ms_elem_to_term cnf a, ms_elem_to_term cnf b) ∈ trivial_rpo.RPO_NS" 
      proof (cases "(a,b) ∈ set S")
        case True
        from S[OF this] show ?thesis using trivial_rpo.RPO_S_subset_RPO_NS by fastforce
      next
        case False
        with mem[unfolded NS] obtain x s where "x ∈ set (vars_of_cnf cnf)" and 
          a: "a = Inl (x, s)" and b: "b = Inl (x, Unsigned)" and s: "s = Positive ∨ s = Negative" 
          by auto
        show ?thesis unfolding a b using s
          apply (auto intro!: all_nstri_imp_mul_nstri)
          subgoal for i by (cases i; cases "i - 1", auto intro!: all_nstri_imp_mul_nstri)
          subgoal for i by (cases i; cases "i - 1", auto intro!: all_nstri_imp_mul_nstri)
          done
      qed
    qed
    thus "(mset as, mset bs) ∈ s_mul_ext trivial_rpo.RPO_NS trivial_rpo.RPO_S" 
      unfolding abs by simp
  next
    assume "(mset as, mset bs) ∈ s_mul_ext trivial_rpo.RPO_NS trivial_rpo.RPO_S" 
    hence mem: "(as, bs) ∈ {(as, bs). (mset as, mset bs) ∈ s_mul_ext trivial_rpo.RPO_NS trivial_rpo.RPO_S}" by simp
    have xsys: "xs = map term_to_ms_elem as" "ys = map term_to_ms_elem bs" unfolding abs map_map o_def
      by (rule nth_equalityI, auto)
    have "(xs, ys) ∈ {(as, bs). (mset as, mset bs) ∈ s_mul_ext (set NS) (set S)}" 
      unfolding xsys
    proof (rule s_mul_ext_map[OF _ _ mem])
      fix a b
      assume ab: "a ∈ set as" "b ∈ set bs" 
      from ab(2)[unfolded abs] obtain y where y: "y ∈ set ys" and b: "b = ms_elem_to_term cnf y" by auto
      from ab(1)[unfolded abs] obtain x where x: "x ∈ set xs" and a: "a = ms_elem_to_term cnf x" by auto
      from y[unfolded ys] obtain v i where y: "y = Inl (v, Unsigned) ∧ v ∈ set (vars_of_cnf cnf)
          ∨ y = Inr i ∧ i < length cnf" by auto
      from x[unfolded xs] obtain w s where s: "s = Positive ∨ s = Negative" and w: "w ∈ set (vars_of_cnf cnf)" 
        and x: "x = Inl (w, s)" by auto
      {
        assume y: "y = Inl (v, Unsigned)" and v: "v ∈ set (vars_of_cnf cnf)" 
        {
          assume "(a,b) ∈ trivial_rpo.RPO_NS" 
          from s this v have "(term_to_ms_elem a, term_to_ms_elem b) ∈ set NS" unfolding a b x y
            by (cases s, auto split: if_splits simp: Let_def NS)
        } note case11 = this
        {
          assume "(a,b) ∈ trivial_rpo.RPO_S" 
          hence "trivial_rpo.rpo_s a b" by simp
          from s this v have False unfolding a b x y
            by (cases, auto split: if_splits simp: Let_def, auto dest!: fst_mul_ext_imp_fst)
        } note case12 = this
        note case11 case12
      } note case1 = this
      {
        assume y: "y = Inr i" and i: "i < length cnf" 
        assume "(a,b) ∈ trivial_rpo.RPO_NS ∪ trivial_rpo.RPO_S" 
        hence "(a,b) ∈ trivial_rpo.RPO_NS"
          using trivial_rpo.RPO_S_subset_RPO_NS by blast
        from s this have "(term_to_ms_elem a, term_to_ms_elem b) ∈ set S" unfolding a b x y
          by (cases, auto split: if_splits simp: Let_def NS S, force+)
      } note case2 = this
      from case1 case2 y
      show "(a, b) ∈ trivial_rpo.RPO_S ⟹ (term_to_ms_elem a, term_to_ms_elem b) ∈ set S" by auto
      from case1 case2 y
      show "(a, b) ∈ trivial_rpo.RPO_NS ⟹ (term_to_ms_elem a, term_to_ms_elem b) ∈ set NS" unfolding NS by auto
    qed
    thus "(mset xs, mset ys) ∈ s_mul_ext (set NS) (set S)" by simp
  qed

  text ‹Here the encoding for single RPO-terms is handled. We do this here and not in a separate
    lemma, since some of the properties of xs, ys, as, bs, etc. are required.›
  assume len2: "length (vars_of_cnf cnf) ≥ 2" 
  show "(∃ β. eval_cnf β cnf) ⟷ (Fun G as, Fun H bs) ∈ trivial_rpo.RPO_S" 
    unfolding one
  proof
    assume mul: "(mset as, mset bs) ∈ s_mul_ext trivial_rpo.RPO_NS trivial_rpo.RPO_S" 
    {
      fix b
      assume "b ∈ set bs" 
      hence "b ∈# mset bs" by auto
      from s_mul_ext_point[OF mul this] have "∃ a ∈ set as. (a,b) ∈ trivial_rpo.RPO_NS"
        using trivial_rpo.RPO_S_subset_RPO_NS by fastforce      
      hence "(Fun G as, b) ∈ trivial_rpo.RPO_S" by (cases b, auto)
    } 
    with mul show "(Fun G as, Fun H bs) ∈ trivial_rpo.RPO_S" 
      by (auto simp: mul_ext_def)
  next
    assume rpo: "(Fun G as, Fun H bs) ∈ trivial_rpo.RPO_S"
    have "¬ (∃s∈set as. trivial_rpo.rpo_ns s (Fun H bs))" 
    proof (rule ccontr)
      assume "¬ ?thesis" 
      then obtain a where a: "a ∈ set as" and "trivial_rpo.rpo_ns a (Fun H bs)" by auto
      with trivial_rpo.rpo_vars_term[of a "Fun H bs"] 
      have vars: "vars_term (Fun H bs) ⊆ vars_term a" by auto
      from a[unfolded abs xs, simplified] obtain x where "vars_term a ∩ range Inl = {Inl x}" 
        by force
      with vars have sub: "vars_term (Fun G bs) ∩ range Inl ⊆ {Inl x}" by auto
      from len2 obtain y z vs where vars: "vars_of_cnf cnf = y # z # vs" 
        by (cases "vars_of_cnf cnf"; cases "tl (vars_of_cnf cnf)", auto)
      have "distinct (vars_of_cnf cnf)" unfolding vars_of_cnf_def by auto
      with vars have yz: "y ≠ z" by auto
      have "{Inl y, Inl z} ⊆ vars_term (Fun G bs)" 
        unfolding abs ys vars by auto
      with sub yz
      show False by auto
    qed
    with rpo have "fst (mul_ext trivial_rpo.rpo_pr as bs)" by (auto split: if_splits)
    thus "(mset as, mset bs) ∈ s_mul_ext trivial_rpo.RPO_NS trivial_rpo.RPO_S" 
      by (auto simp: mul_ext_def Let_def)
  qed
qed

lemma rpo_constraint_of_cnf: assumes non_triv: "length (vars_of_cnf cnf) ≥ 2" 
shows "(∃ β. eval_cnf β cnf) ⟷ rpo_constraint_of_cnf cnf ∈ trivial_rpo.RPO_S"
proof -
  obtain as bs where res: "term_lists_of_cnf cnf = (as,bs)" by force
  from non_triv have cnf: "cnf ≠ []" unfolding vars_of_cnf_def by auto
  show ?thesis unfolding rpo_constraint_of_cnf_def res split
    by (subst term_lists_of_cnf(2)[OF res cnf non_triv], auto)
qed 

subsection ‹Size of Encoding is Quadratic›

fun term_size :: "('f,'v)term ⇒ nat" where
  "term_size (Var x) = 1" 
| "term_size (Fun f ts) = 1 + sum_list (map term_size ts)" 

lemma size_of_rpo_constraint_of_cnf:
  assumes "rpo_constraint_of_cnf cnf = (s,t)" 
  and "size_cnf cnf = n" 
  shows "term_size s + term_size t ≤ 4 * n⇧2 + 12 * n + 2" 
proof -
  obtain as bs S NS where mp: "multiset_problem_of_cnf cnf = (as, bs, S, NS)" 
    by (cases "multiset_problem_of_cnf cnf", auto)
  from size_of_multiset_problem_of_cnf[OF mp assms(2)]
  have las: "length as ≤ 2 * n" "length bs ≤ 2 * n" by auto
  have tl: "term_lists_of_cnf cnf = (map (ms_elem_to_term cnf) as, map (ms_elem_to_term cnf) bs)" 
    unfolding term_lists_of_cnf_def mp split by simp
  from assms(1)[unfolded rpo_constraint_of_cnf_def tl split]
  have st: "s = Fun G (map (ms_elem_to_term cnf) as)" "t = Fun H (map (ms_elem_to_term cnf) bs)" by auto
  have [simp]: "term_size (if b then Var (Inr x) :: (FSyms, 'a + nat) Term.term else Fun A []) = 1" for b x 
    by (cases b, auto)
  have len_n: "length cnf ≤ n" using assms(2) unfolding size_cnf_def by auto
  have "term_size (ms_elem_to_term cnf a) ≤ 3 + length cnf" for a
    by (cases "(cnf,a)" rule: ms_elem_to_term.cases, auto simp: o_def sum_list_triv)
  also have "… ≤ 3 + n" using len_n by auto
  finally have size_ms: "term_size (ms_elem_to_term cnf a) ≤ 3 + n" for a .
  {
    fix u
    assume "u ∈ {s,t}" 
    then obtain G cs where "cs ∈ {as, bs}" and u: "u = Fun G (map (ms_elem_to_term cnf) cs)" 
      unfolding st by auto
    hence lcs: "length cs ≤ 2 * n" using las by auto
    have "term_size u = 1 + (∑x←cs. term_size (ms_elem_to_term cnf x))" unfolding u by (simp add: o_def size_list_conv_sum_list)
    also have "… ≤ 1 + (∑x←cs. 3 + n)" 
      by (intro add_mono lcs le_refl sum_list_mono size_ms)
    also have "… ≤ 1 + (2 * n) * (3 + n)" unfolding sum_list_triv
      by (intro add_mono le_refl mult_mono, insert lcs, auto)
    also have "… = 2 * n^2 + 6 * n + 1" by (simp add: field_simps power2_eq_square)
    finally have "term_size u ≤ 2 * n⇧2 + 6 * n + 1" .
  }
  from this[of s] this[of t]
  show "term_size s + term_size t ≤ 4 * n⇧2 + 12 * n + 2" by simp
qed

subsection ‹Check Executability›

value (code) "case rpo_constraint_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 (s,t) ⇒ (''SAT: '', trivial_rpo.rpo_s s t, ''Encoding: '', s, '' >RPO '', t)" 

hide_const (open) A F G H U P N


end