Proof of Correctness of Codeforces Problem: Boxers (rated 1500)

Question

Consider this problem appearing in Codeforces (rated 1500):

There are n boxers, the weight of the i-th boxer is ai. Each of them can change the weight by no more than 1 before the competition (the weight cannot become equal to zero, that is, it must remain positive). Weight is always an integer number.

It is necessary to choose the largest boxing team in terms of the number of people, that all the boxers' weights in the team are different (i.e. unique).

Write a program that for given current values ​ai will find the maximum possible number of boxers in a team.

It is possible that after some change the weight of some boxer is 150001 (but no more).

Input :The first line contains an integer n (1≤n≤150000) — the number of boxers. The next line contains n integers a1,a2,…,an, where ai (1≤ai≤150000) is the weight of the i-th boxer.

Output :Print a single integer — the maximum possible number of people in a team.

Here is the code I implemented which was accepted by the Codeforces as a correct submission (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))

However, I am not able to rigorously prove that this algorithm necessarily give the correct answer. For example, when inputlist is [1, 1, 1, 2, 2, 5 , 8], both [1, 2, 3, 4, 7, 8](my algorithm) and [1, 2, 3, 6, 7, 8] is the correct output boxerset, although the answer for both the cases comes out to be 6.

My question is this:

How can I prove my algorithm is correct? How will my proof work to show that out of all possible legal selections of boxers, the selection by my algorithm has the maximum amount of boxers (that is how do I show that my there exists no other selection for which the number of boxers can be greater than the selection done by my algorithm)?

I have tried proof by contradiction but to no avail (although I think the proof has to have the natural structure of a proof by contradiction).

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

Answer 1

David Eisenstat's last sentence on the second paragraph of his answer "Hence the dynamic program should track the maximum team size for each fighting weight bound" has inspired me to an alternate solution. I use induction:

Assume that while iterating through the loop, the maximum fighting weight of the fighter selected is k.

The inductive assumption is that this subsequence consists of the maximum team size for weight bound k.

As the inductive step, when the next iterations add the higher fighting weight, this is obviously the maximum team size with weight bound k+1.

To see this, assume this is not the case. Then there exists a subsequence with the more team size than the one created from our algorithm. Remove k+1 fighter from this list. Then this list should be the largest subsequence of weight bound k, which leads to contradiction from the inductive hypothesis. Hence the correctness of the algorithm is proved.

The only case which is not included is where there is only 1 possible fighter in the boxerlist. This case is trivial and hence the proof is complete.

Answer 2

Your code can be viewed as a specialized dynamic program.

First, a structure theorem: there exists an optimal solution where for each pair of boxers with starting weights a_i < a_j that make the team, the fighting weight of boxer i is less than the fighting weight of boxer j. This is because the only way that this could happen is if a_i + 1 = a_j and i's fighting weight is a_i + 1 and j's fighting weight is a_j - 1. In this case, however, we could have let i and j just fight at their starting weights, and the final team would have the same set of weights.

Given this structure theorem, there's a dynamic program that considers each boxer in order of starting weight from lightest to heaviest. The optimal substructure is that, for a prefix of the boxers in sorted order, the two relevant parameters are 1. the number of boxers chosen from the prefix 2. the heaviest fighting weight of a boxer that made the team (thanks to the structure theorem, we can assume that every subsequent boxer must have a larger fighting weight). Hence the dynamic program should track the maximum team size for each fighting weight bound.

Rather than write out this DP, we observe that some of the solutions can be pruned. In particular, if there's a sub-solution of k boxers with weight bound w and another sub-solution of k-1 with weight bound w-1, then there's no point in keeping the second, because the moment we add another boxer to it, it will be no better than the first. On the other hand, maybe we have a sub-solution with k boxers with weight bound w and a sub-solution with k-1 boxers with weight bound w' < w-1. If there are no boxers that can fight at weight less than w, then again we can discard the second sub-solution. After some case analysis, the upshot is that we never have to remember more than one sub-solution.

The final version of the loop looks like this.

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)

Like your code, this solution repeatedly and greedily selects the minimum weight at which the next lightest boxer can fight. Both yield provably optimal results.