NyaOJ

题目描述

在 0-1 背包问题中，有一个背包和若干物品，需要找出如何选取物品放入背包，能够最大化背包中物品的总价值。本问题中，每件物品要么不放入背包，要么完整地放入背包。

试证明该问题的最优解包含其"子问题"的最优解（这是该问题动态规划算法正确性的基础）。

问题设置

物品数量为 $N : \mathbb{N}$ ，背包容量为 $C : \mathbb{N}$
将各件物品编号为 $1, 2, \ldots, N$
函数 caps : ℕ → ℕ 给出每件物品的体积
函数 vals : ℕ → ℕ 给出每件物品的价值

可以用函数 s : ℕ → Option Bool 表示从物品 $1, 2, \ldots, n$ 中选取物品放入背包的方案：

s i = some true 表示物品 $i$ 放入背包
s i = some false 表示物品 $i$ 不放入背包
s i = none 表示方案中不包含关于物品 $i$ 的信息

任务

1. wf_clr (25 分)

theorem wf_clr (N : ℕ) (s : ℕ → Option Bool) (n : ℕ) :
    1 ≤ n ∧ n ≤ N → wf s n → wf (clear s n) (n - 1)

2. wf_set_s (25 分)

theorem wf_set_s (s : ℕ → Option Bool) (n : ℕ) (b : Bool) :
    1 ≤ n → wf s (n - 1) → wf (set_s s n b) n

3. clr_set (20 分)

theorem clr_set (s : ℕ → Option Bool) (n : ℕ) :
    s n = none → clear (fun j => if j = n then some true else s j) n = s

4. optimal_substructure (80 分)

若 $s$ 是从物品 $1$ 至 $n$ 中选取物品放入背包中容量为 c_rem 的一部分空间中的最优方案，且 $s$ 选择将物品 $n$ 放入背包，则 $s$ 中除去物品 $n$ 以外的部分是从物品 $1$ 至 $n-1$ 中选取物品放入背包中容量为 c_rem - caps n 的一部分空间中的最优方案。

theorem optimal_substructure (N : ℕ) (caps vals : ℕ → ℕ) (s : ℕ → Option Bool) (n c_rem : ℕ) :
    1 ≤ n ∧ n ≤ N → s n = some true → caps n ≤ c_rem →
    opt_s caps vals s n c_rem →
    opt_s caps vals (clear s n) (n - 1) (c_rem - caps n)

提示：可考虑采取反证法思路。

分值

wf_clr: 25 分
wf_set_s: 25 分
clr_set: 20 分
optimal_substructure: 80 分

总计: 150 分