Theory Subset_Sum
theory Subset_Sum
imports
Main
Partition
"Jordan_Normal_Form.Matrix"
begin
section ‹Subset Sum Problem›
text ‹The Subset Sum Problem is a common NP-hard Problem. ›
definition subset_sum :: "((int vec) * int) set" where
"subset_sum ≡ {(as,s). (∃xs::int vec.
(∀i<dim_vec xs. xs$i ∈ {0,1}) ∧ xs ∙ as = s ∧ dim_vec xs = dim_vec as)}"
definition subset_sum_nonzero :: "((int vec) * int) set" where
"subset_sum_nonzero ≡ {(as,s). (∃xs::int vec.
(∀i<dim_vec xs. xs$i ∈ {0,1}) ∧ xs ∙ as = s ∧ dim_vec xs = dim_vec as) ∧ dim_vec as ≠ 0}"
definition subset_sum_list :: "((int list) * int) set" where
"subset_sum_list ≡ {(as,s). (∃xs::int list.
(∀i<length xs. xs!i ∈ {0,1}) ∧ (∑i<length as. as!i * xs!i) = s ∧ length xs = length as)}"
text ‹Reduction Subset Sum to Partition.›
definition reduce_subset_sum_partition:: "(int list) ⇒ ((int list) * int)" where
"reduce_subset_sum_partition ≡
(λ a. (a, (if sum_list a mod 2 = 0 then sum_list a div 2 else (∑i<length a. ¦a!i¦) + 1)))"
text ‹Well-definedness of reduction function›
lemma sum_list_map_2:
assumes "length a = length xs"
shows "(sum_list (map2 (*) a xs)) = (∑i<length a. a!i * xs!i)"
using assms proof (induct rule: list_induct2)
case (Cons x xs y ys)
have "(∑i<length ys. (x # xs) ! i * (y # ys) ! i) + (x # xs) ! length ys * (y # ys) ! length ys =
(∑i≤length ys. (x # xs) ! i * (y # ys) ! i)"
by (metis (no_types, lifting) lessThan_Suc_atMost sum.lessThan_Suc)
also have "… = (x # xs) ! 0 * (y # ys) ! 0 +
(∑i<length ys. (x # xs) ! (i+1) * (y # ys) ! (i+1))"
using sum.atMost_shift[of "(λi. (x # xs) ! i * (y # ys) ! i)" "length ys"] by auto
also have "… = x * y + sum_list (map2 (*) xs ys)" using Cons by auto
finally have "x * y + sum_list (map2 (*) xs ys) = (∑i<length ys. (x # xs) ! i * (y # ys) ! i) +
(x # xs) ! length ys * (y # ys) ! length ys" by presburger
then show ?case using Cons by auto
qed auto
lemma ex_01_list:
assumes "I⊆{0..<n}"
shows "∃xs::int list. (∀i∈I. xs ! i = 1) ∧ (∀i∈{0..<n}-I. xs ! i = 0) ∧ length xs = n"
using assms proof (induct n arbitrary: I)
case (Suc n)
define I' where "I' = I ∩ {0..<n}"
then have "I'⊆ {0..<n}" by auto
obtain xs'::"int list" where xs'_def:
"(∀i∈I'. xs' ! i = 1) ∧ (∀i∈{0..<n} - I'. xs' ! i = 0) ∧ length xs' = n"
using Suc(1)[OF ‹I'⊆{0..<n}›] by blast
define xs where "xs = xs' @ [if n ∈ I then 1 else 0]"
then have eq: "xs ! i = xs' ! i" if "i<n" for i using that
by (simp add: nth_append xs'_def)+
have 1: "(∀i∈I. xs ! i = 1)" unfolding xs_def
proof (split if_split, safe, goal_cases)
case (1 i)
then have "¬ i < n ⟹ [1] ! (i - n) = 1"
by (metis Suc.prems atLeast0LessThan atMost_iff cancel_comm_monoid_add_class.diff_cancel
lessThan_Suc_atMost linorder_neqE_nat not_le nth_Cons_0 subset_eq)
with 1 show ?case by (subst nth_append)
(use eq in ‹auto simp add: xs'_def I'_def Suc xs_def›)
next
case (2 i)
then have "i < n"
by (metis Suc.prems atLeastLessThan_iff less_antisym subset_eq)
with 2 show ?case by (subst nth_append)
(use eq in ‹auto simp add: xs'_def I'_def Suc xs_def›)
qed
moreover have 2: "(∀i∈{0..<Suc n} - I. xs ! i = 0)"unfolding xs_def
proof (split if_split, safe, goal_cases)
case (1 i)
then have "i<n" by (metis atLeastLessThan_iff less_antisym)
with 1 show ?case by (subst nth_append) (auto simp add: xs'_def I'_def Suc xs_def)
next
case (2 i)
then show ?case by (subst nth_append) (auto simp add: xs'_def I'_def Suc xs_def)
qed
moreover have "length xs = Suc n" by (auto simp add: xs'_def I'_def Suc xs_def)
ultimately have "(∀i∈I. xs ! i = 1) ∧ (∀i∈{0..<Suc n} - I. xs ! i = 0) ∧ length xs = Suc n"
by auto
then show ?case by (subst exI, auto)
qed auto
lemma sum_list_even:
assumes "a ∈ partition_problem"
shows "sum_list a mod 2 = 0"
using assms unfolding partition_problem_def
proof (safe, goal_cases)
case (1 I)
then have "sum ((!) a) {0..<length a} = sum ((!) a) I + sum ((!) a) ({0..<length a} - I)"
by (metis finite_atLeastLessThan sum.subset_diff)
then have "sum ((!) a) {0..<length a} = 2 * sum ((!) a) I" using 1 by auto
then show ?case by (simp add: sum_list_sum_nth)
qed
lemma well_defined_reduction_subset_sum:
assumes "a ∈ partition_problem"
shows "reduce_subset_sum_partition a ∈ subset_sum_list"
using assms unfolding partition_problem_def reduce_subset_sum_partition_def subset_sum_list_def Let_def
proof (safe, goal_cases)
case (1 I)
have sum_even: "sum_list a mod 2 = 0" using sum_list_even[OF assms] by auto
then have if_rewrite:
"(if sum_list a mod 2 = 0 then sum_list a div 2 else (∑i<length a. ¦a!i¦) + 1) =
sum_list a div 2" by auto
have split_set: "{0..<length a} = I ∪ ({0..<length a}-I)"
using 1(1) by (subst Un_Diff_cancel, auto)
have disjoint: "I ∩ ({0..<length a}-I) = {}" by auto
have "∃xs::int list. (∀i∈I. xs ! i = 1) ∧ (∀i∈{0..<length a}-I. xs ! i = 0) ∧
length xs = length a" using ex_01_list[OF ‹I ⊆ {0..<length a}›] by auto
then obtain xs::"int list" where
xs_prop: "∀i∈I. xs ! i = 1"
"∀i∈{0..<length a}-I. xs ! i = 0"
"length xs = length a" by blast
then have eq: "(∑i<length a. a!i * xs!i) = (∑i∈I. a!i)" using split_set 1(1)
by (metis (no_types, lifting) finite_lessThan lessThan_atLeast0 mult_cancel_left2
mult_cancel_right2 sum.cong sum.mono_neutral_right)
have "sum_list a = (∑i∈I. a!i) + (∑i∈{0..<length a}-I. a!i)" using 1(1)
by (smt (verit) finite_atLeastLessThan sum.subset_diff sum_list_sum_nth)
also have "… = 2 * (∑i∈I. a!i)" using 1(2)[symmetric] by auto
also have "… = 2 * (sum_list (map2 (*) a xs))" using eq xs_prop by (subst sum_list_map_2, auto)
finally have "sum_list (map2 (*) a xs) = (sum_list a) div 2" by simp
then show ?case using xs_prop sum_list_map_2 ‹2 * sum ((!) a) I = 2 * sum_list (map2 (*) a xs)› eq
by (subst exI[of _ xs], auto simp add: if_rewrite)
qed
text ‹NP-hardness of reduction function›
lemma NP_hardness_reduction_subset_sum:
assumes "reduce_subset_sum_partition a ∈ subset_sum_list"
shows "a ∈ partition_problem"
using assms unfolding partition_problem_def reduce_subset_sum_partition_def subset_sum_list_def Let_def
proof (safe, goal_cases)
case (1 xs)
have "(sum_list a) mod 2 = 0" using 1
proof -
have "(∑i<length a. a ! i * xs ! i) ≤ (∑i<length a. ¦a!i¦)" using 1 by (subst sum_mono, auto)
then have "(∑i<length a. a ! i * xs ! i) ≠ (∑i<length a. ¦a!i¦) + 1" by auto
then show ?thesis using 1 by presburger
qed
obtain I where I_prop: "I = {i. i< length xs ∧ xs!i = 1}" by blast
then have split_set: "{0..<length a} = I ∪ ({0..<length a}-I)"
using I_prop 1 by (subst Un_Diff_cancel, auto)
have "I⊆{0..<length a}" using I_prop 1 by auto
moreover have "sum ((!) a) I = sum ((!) a) ({0..<length a} - I)"
proof -
have eq: "(∑i∈I. a!i) = (∑i<length a. a!i * xs!i)" using split_set I_prop 1
by (smt (verit, ccfv_threshold) Diff_iff ‹I ⊆ {0..<length a}› atLeast0LessThan
atLeastLessThan_iff empty_iff finite_atLeastLessThan insert_iff mem_Collect_eq
mult_cancel_left2 mult_cancel_right2 sum.cong sum.mono_neutral_right)
have "(∑i∈{0..<length a}-I. a!i) = sum ((!) a) {0..<length a} - (∑i∈I. a!i)" using split_set
by (meson ‹I ⊆ {0..<length a}› finite_atLeastLessThan sum_diff)
also have "… = sum_list a - sum_list a div 2"
by (metis "1"(2) ‹sum_list a mod 2 = 0› eq sum_list_sum_nth)
also have "… = sum_list a div 2" using ‹(sum_list a) mod 2 = 0› by auto
finally have "(∑i∈{0..<length a}-I. a!i) = (∑i∈I. a!i)"
using "1"(2) ‹sum_list a mod 2 = 0› eq by presburger
then show ?thesis by auto
qed
ultimately show ?case by (subst exI, auto)
qed
text ‹The Subset Sum on lists is NP-hard.›
lemma "is_reduction reduce_subset_sum_partition partition_problem subset_sum_list"
unfolding is_reduction_def
proof (safe, goal_cases)
case (1 a)
then show ?case using well_defined_reduction_subset_sum by auto
next
case (2 a)
then show ?case using NP_hardness_reduction_subset_sum by auto
qed
text ‹Subset Sum on vectors is the same as on lists›
lemma subset_sum_vec_list:
"(as,s) ∈ subset_sum ⟷ (list_of_vec as,s) ∈ subset_sum_list"
proof (safe, goal_cases)
case 1
then have "∃xs. (∀i<dim_vec xs. xs $ i ∈ {0, 1}) ∧ xs ∙ as = s ∧ dim_vec xs = dim_vec as"
unfolding subset_sum_def by auto
then have " ∃xs. (∀i<length xs. xs ! i ∈ {0, 1}) ∧
(∑i<length (list_of_vec as). (list_of_vec as) ! i * xs ! i) = s ∧
length xs = length (list_of_vec as)"
unfolding scalar_prod_def
by (metis (no_types, lifting) atLeast0LessThan length_list_of_vec mult.commute
sum.cong vec_list vec_of_list_index)
then show ?case unfolding subset_sum_list_def by auto
next
case 2
then have " ∃xs. (∀i<length xs. xs ! i ∈ {0, 1}) ∧
(∑i<length (list_of_vec as). (list_of_vec as) ! i * xs ! i) = s ∧
length xs = length (list_of_vec as)"
unfolding subset_sum_list_def by auto
then have "∃xs. (∀i<dim_vec xs. xs $ i ∈ {0, 1}) ∧ xs ∙ as = s ∧ dim_vec xs = dim_vec as"
unfolding scalar_prod_def
by (metis (no_types, lifting) dim_vec_of_list lessThan_atLeast0 mult.commute
sum.ivl_cong vec_list vec_of_list_index)
then show ?case unfolding subset_sum_def by auto
qed
end