:: Dynamic Programming for the Subset Sum Problem :: by Hiroshi Fujiwara , Hokuto Watari and Hiroaki Yamamoto :: :: Received January 13, 2020 :: Copyright (c) 2020-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PRSUBSET, NUMBERS, NAT_1, FINSEQ_1, CARD_1, RELAT_1, SUBSET_1, XBOOLE_0, FUNCT_1, TARSKI, ORDINAL4, ARYTM_1, ARYTM_3, REAL_1, ZFMISC_1, XXREAL_0, CARD_3, XBOOLEAN, MARGREL1, VALUED_0, FUNCOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, BINOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, FUNCOP_1, VALUED_0, FINSEQ_1, FINSEQOP, XBOOLEAN, MARGREL1, RVSUM_1, RVSUM_3; constructors FINSEQOP, RELSET_1, REAL_1, RVSUM_1, MARGREL1, VALUED_0, RVSUM_3; registrations XBOOLE_0, FUNCT_1, ORDINAL1, NUMBERS, XREAL_0, NAT_1, FINSEQ_1, VALUED_0, RELAT_1, CARD_1, XBOOLEAN, MARGREL1, RVSUM_1; requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL; begin :: Recurrence Relation of Dynamic Programming for the Subset Sum Problem definition let x be FinSequence; let I be set; func Seq (x, I) -> FinSequence equals :: PRSUBSET:def 1 Seq (x | I); end; registration let D be set; let x be D-valued FinSequence; let I be set; cluster Seq (x, I) -> D-valued; end; registration let x be real-valued FinSequence; let I be set; cluster Seq (x, I) -> real-valued; end; registration let D be set; let x be D-valued FinSequence; let i be Nat; cluster x | i -> D-valued for FinSequence-like Function; end; registration let x be real-valued FinSequence; let i be Nat; cluster x | i -> real-valued for FinSequence-like Function; end; definition let x be REAL-valued FinSequence; let a be Real; pred x exist_subset_sum_eq a means :: PRSUBSET:def 2 ex I being set st I c= dom x & Sum (Seq (x, I)) = a; end; definition let x be REAL-valued FinSequence; func Q_ex(x) -> Function of [:Seg (len x), REAL:], BOOLEAN means :: PRSUBSET:def 3 for i being Nat, s being Real st 1 <= i <= len x holds (x | i exist_subset_sum_eq s implies it . (i, s) = TRUE) & (not x | i exist_subset_sum_eq s implies it . (i, s) = FALSE); end; registration let A be Subset of NAT; let i be Nat, s be Real; let f be Function of [:A, REAL:], BOOLEAN; cluster f . (i, s) -> boolean; end; definition let a, b be object; func a _eq_ b -> object equals :: PRSUBSET:def 4 IFEQ(a,b,TRUE,FALSE); end; registration let a, b be object; cluster a _eq_ b -> boolean; end; definition let a, b be ExtReal; func a _le_ b -> object equals :: PRSUBSET:def 5 IFGT(a,b,FALSE,TRUE); end; registration let a, b be ExtReal; cluster a _le_ b -> boolean; end; theorem :: PRSUBSET:1 for s being Real, x being REAL-valued FinSequence st 1 <= len x holds (Q_ex(x)) . (1, s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0); theorem :: PRSUBSET:2 for f,g being Function, X,Y being set st rng g c= X holds (f | (X \/ Y)) * g = (f | X) * g; theorem :: PRSUBSET:3 for x being REAL-valued FinSequence, i being Nat, I0 being set st I0 c= Seg i & Seg (i+1) c= dom x holds Seq (x | (i+1), I0 \/ {i+1}) = Seq (x | i, I0) ^ <* x . (i+1) *>; theorem :: PRSUBSET:4 ::: should be somewhere for x being real-valued FinSequence st x <> {} & x is positive holds 0 < Sum x; theorem :: PRSUBSET:5 for x being real-valued FinSequence, i being Nat st x is positive & 1 <= i <= len x holds x | i is positive & x | i <> {}; theorem :: PRSUBSET:6 for x being real-valued FinSequence, I being set st x is positive & I c= dom x & I <> {} holds Seq (x, I) is positive & Seq (x, I) <> {}; :: Recurrence Relation: Induction Case theorem :: PRSUBSET:7 for x being REAL-valued FinSequence st x is positive holds for i being Nat, s being Real st 1 <= i < len x holds ((Q_ex(x)) . (i+1, s)) = ((Q_ex(x)) . (i, s)) 'or' ((x . (i+1) _le_ s) '&' ((Q_ex(x)) . (i, s - x . (i+1))));