Codeforces 问题的正确性证明：Boxers（评级为 1500）答案

【问题标题】：Proof of Correctness of Codeforces Problem: Boxers (rated 1500)Codeforces 问题的正确性证明：Boxers（评级为 1500）
【发布时间】：2019-09-18 12:41:39
【问题描述】：

考虑出现在 Codeforces（额定 1500）中的这个问题：

有n个拳击手，第i个拳击手的重量是ai。他们每个人在比赛前可以改变权重不超过1（权重不能变为零，即必须保持正数）。权重始终是整数。

需要选择人数最多的拳击队，团队中所有拳击手的体重都不同（即唯一）。

编写一个程序，对于给定的当前值，ai 将找到一个团队中可能的最大拳击手数。

有可能一些拳击手的体重在一些改变后是 150001（但不会更多）。

输入 : 第一行包含一个整数 n (1≤n≤150000)——拳击手的数量。下一行包含 n 个整数 a1,a2,…,an，其中 ai (1≤ai≤150000) 是第 i 个拳击手的体重。

输出 :打印一个整数——团队中可能的最大人数。

这是我实现的代码，被 Codeforces 接受为正确提交（Python 3.7）：

n=int(input())
inputlist=list(map(int, input().split()))
inputlist.sort()
boxerset=set()
for i in inputlist:
    if i-1 not in boxerset and i!=1:
        boxerset.add(i-1)
    elif i not in boxerset:
        boxerset.add(i)
    elif i+1 not in boxerset:
        boxerset.add(i+1)
    else:
        continue
print(len(boxerset))

但是，我无法严格证明该算法一定会给出正确答案。例如，当 inputlist 为 [1, 1, 1, 2, 2, 5 , 8] 时，[1, 2, 3, 4, 7, 8]（我的算法）和 [1, 2, 3, 6, 7, 8] 是正确的输出 boxerset，尽管这两种情况的答案都是 6。

我的问题是这样的：

如何证明我的算法是正确的？我的证明如何证明在所有可能的合法拳击手选择中，我的算法选择的拳击手数量最多（这就是我如何证明我不存在其他选择拳击手的数量可以是大于我的算法所做的选择）？

我尝试过反证法但无济于事（尽管我认为证明必须具有反证法的自然结构）。

https://codeforces.com/problemset/problem/1203/E

【问题讨论】：

标签： algorithm proof proof-of-correctness

【解决方案1】：

您的代码可以被视为一个专门的动态程序。

首先，一个结构定理：存在一个最优解，对于每对起始体重为a_i < a_j的拳击手组成球队，拳击手i的战斗重量小于拳击手j的战斗重量.这是因为发生这种情况的唯一方法是如果a_i + 1 = a_j 和i 的战斗重量是a_i + 1 和j 的战斗重量是a_j - 1。但是，在这种情况下，我们可以让 i 和 j 以他们的起始体重进行比赛，而最终的队伍将拥有相同的体重。

根据这个结构定理，有一个动态程序会按照起始重量从最轻到最重的顺序考虑每个拳击手。最优子结构是，对于排序顺序的拳击手前缀，两个相关参数是 1. 从前缀中选择的拳击手数量 2. 组成团队的拳击手的最重战斗重量（感谢结构定理，我们可以假设每个后续的拳击手都必须有更大的战斗重量）。因此，动态程序应该跟踪每个战斗重量界限的最大团队规模。

我们观察到一些解决方案可以被修剪，而不是写出这个 DP。特别是，如果有一个k boxers 的子解决方案，其重量为w，另一个k-1 的子解决方案为w-1，那么保留第二个没有意义，因为我们添加的那一刻另一个拳击手，它不会比第一个更好。另一方面，也许我们有一个带有k 重量限制w 的拳击手的子解决方案和一个带有k-1 重量限制w' < w-1 的拳击手的子解决方案。如果没有拳击手的体重低于w，那么我们可以再次丢弃第二个子解决方案。经过一些案例分析，结果是我们永远不必记住多个子解决方案。

循环的最终版本如下所示。

maxweightonteam = 0
countonteam = 0
for ai in inputlist:
    if ai < maxweightonteam:
        continue
    assert ai + 1 >= maxweightonteam + 1
    maxweightonteam = max(maxweightonteam + 1, ai - 1)
    countonteam += 1
print(countonteam)

与您的代码一样，此解决方案反复且贪婪地选择下一个最轻的拳击手可以战斗的最小重量。两者都产生了可证明的最佳结果。

【讨论】：

感谢您的回答。我理解结构定理（我认为你错误地写了“这可能发生的唯一方式”而不是“这不可能发生的唯一方式”）但我根本不明白我的代码和“循环的最终版本”。我什至不明白你的代码是如何工作的。你能解释一下吗？再次感谢。

【解决方案2】：

David Eisenstat 在他的回答第二段中的最后一句话“因此，动态程序应该跟踪每个战斗重量限制的最大团队规模”，这启发了我另一种解决方案。我使用归纳法：

假设在循环中迭代时，所选战斗机的最大战斗重量为k。

归纳假设是这个子序列由权重限制k的最大团队规模组成。

作为归纳步骤，当下一次迭代添加更高的战斗权重时，这显然是权重限制k+1的最大团队规模。

要看到这一点，假设情况并非如此。然后存在一个比我们的算法创建的团队规模更大的子序列。从此列表中删除 k+1 战斗机。那么这个列表应该是权重界限k的最大子序列，这导致与归纳假设相矛盾。从而证明了算法的正确性。

唯一不包括在内的情况是拳击手列表中只有 1 个可能的拳手。这个案例是微不足道的，因此证明是完整的。

【讨论】：