I am attempting to prove the following algorithm is fully correct (partial correctness + termination), but I can only seem to prove for arbitrary example inputs (not general ones).
Here is my pseudo-code:
IN :Listofjobs J, maxindex n
1:S ← an array indexed 0 to n, with null at each index
2:Sort J in non-increasing order of profits
3:for i from 0 to n
4:Find the largest t such that S[t] = null and t ≤ J[i].deadline (if one exists) if an index t was found
5: S[t] ← J[i]
OUT: S maximizes the profit of scheduled jobs that can be done in n 1 unit of time blocks
So for example, I created a table with jobs and their associated attributes (deadlines and profit):
jOB J1 J2 J3 J4 J5
Deadline 2 1 3 2 1
profit 62 100 20 40 20
From this example input, we'd be able to do J2,J1,J3 for a total profit of 182.
Can someone help me form a more generic way of showing my pseudo-code algorithm is fully correct?
Adding constraints helps you here.
In step 2 order J first by non-increasing profits, and then by non-increasing deadline.
Of all optimal solutions, at least one must be lexicographically last by the ordering of profits of jobs over time. (If multiple jobs have the same profit and deadlines, there may be multiple optimal solutions that are lexicographically last.)
Prove that any solution that does not have a job of the same profit at the same time as the first job that you place is either not optimal, or is not lexicographically last among optimal solutions.
Prove by induction that the solution that you found is identical in placement of sizes of jobs as any solution that is optimal and lexicographically last among optimal solutions.
Please note that this is an outline only. There are some subtle tricks needed at each step of this proof that I'm deliberately leaving as an exercise.