Proof for LeetCode: 11. Container With Most Water problem

Question

UPDATE: I abandoned this initial approach in favor of a more powerful invariant I worked out after posting. I've detailed that one in an answer below.

---

I'm new to algorithm correctness proof-writing but am keen to improve my skill there.

I have a first attempt here, but I think I'm missing a final step. The algorithm is for the LeetCode: 11. Container With Most Water problem.

I've shown to my satisfaction that only an "advance the lesser" move at any given point can possibly result in a greater area (water volume), but it feels like I'm missing the part where I can say "therefore this algorithm will always find the maximum".

Any pointers on process, notation, or formalisms is also greatly appreciated. This proof strikes me a bit as "workshop-grade" and I wouldn't mind getting a bit more elegant about it as I do others.

Problem Statement:

Given an array of non-negative integers hs (heights) where each represents a point at coordinate (i, hs[i]), n vertical lines are drawn such that the two endpoints of line i is at (i, hs[i]) and (i, 0). Find two lines, which together with the x-axis form a container, such that the container contains the most water.

Notation:

• H - Height
• W - Width
• A - Area

       |--W--|

       |           ___  
       |     |      |
       |  |  |  |   H
    |  |  |  |  |   |
    +--+--+--+--+  ---
    0  1  2  3  4

For example, a maximal cross-section A of H ✕ W = 3 ✕ 2 = 6 is between offsets 1 and 3. Note there's another one of area 6 for range [1..4], so the maximum is not necessarily unique.

The solution approach which seems to work is the following:

1. Create index variables left (L) and right (R) initially positioned at the extreme left (0) and right (|hs|-1) of array hs.

2. Calculate the area as A = H ✕ W where H = min(hs[L], hs[R]) and W = R - L and record it as the maximal area so far.

3. Move the lesser of L or R toward the other.

4. Repeat until R == L, then return the maximum recorded.

Code would look something like this in Python

def max_water(hs):
    L, R = 0, len(hs) - 1
    max_A = 0

    while L < R:
        A = min(hs[L], hs[R]) * (R - L)
        max_A = max(max_A, A)
        if hs[L] <= hs[R]:
            L += 1
        else:
            R -= 1

    return max_A

My proof approach is to show that only advancing the lesser-height index can possibly increase the current area. The thing I don't quite get is whether this proves correctness; my sense is I'm missing a last step:

Proof

There are four possible cases produced by choosing to advance the lesser or greater-height index (toward the middle) and whether the "advanced-to" height is greater or lesser that the prior. For concise expression, I use L and R to represent the heights of those two positions:

Case 1: Advance greater, new height is greater

    |-----W-----|

             |     
             |  |  ___
    |        |  |   |  H
    |  ...   |  |   | 
    +--+--------+  ---
    L  ...   R' R  

    L < R, advance R to R', R' > R

    then:

    * H' = H -- because L is unchanged and L = H is still the upper bound.
    * W' < W
    * => H' ✕ W' < H ✕ W
    * => A' < A

Case 2: Advance greater, new height is lower (or equal).::

    |-----W-----|

                |  
             |  |  ___
    |        |  |   |  H
    |  ...   |  |   | 
    +--+--------+  ---
    L  ...   R' R  

    L < R, advance R to R', R' <= R

    then:

    * H' <= H -- H' cannot be greater than it was because L = H is still an upper bound.
    * W' < W
    * => H' ✕ W' < H ✕ W
    * => A' < A

Case 3: Advance lesser, new height is lower (or equal).::

    |-----W-----|

                |  
                |  ___
    |           |   |  H
    |  |  ...   |   | 
    +--+--------+  ---
    L  L' ...   R  

    L < R, advance L to L', L' <= L

    then:

    * H' <= H
    * W' < W
    * => H' ✕ W' < H ✕ W
    * => A' < A

Case 4: Advance lesser, new height is higher.::

    |-----W-----|

                |  
       |        |  ___
    |  |        |   |  H
    |  |  ...   |   | 
    +--+--------+  ---
    L  L' ...   R  

    L < R, advance L to L', L' <= L

    then:

    * H' > H
    * W' < W
    * => H' ✕ W' is either <, =, or > H ✕ W
    * => A' <, =, or > A

So the only way an area greater than the current area can possibly be found is by following the "advance the lesser" policy. All the other cases lead to a reduction in area.

What I'm not seeing is how that necessarily guarantees this algorithm will find the maximum.

Answer 1

I would suggest the following $O(n)$ approach using a monotone stack which is nothing but a regular stack but also satisifes the invariant that its elements are in monotone order. Say you want to make a strictly monotone stack $S$ which is increasing viewed from the last in to the first out: you would process elements $x$ in order with the following policy: pop $S$ until it is empty, or until the top is $>x$, then push $x$.

Why might such a structure appear? Let's consider the half-problem where we find the largest container whose right side is smaller. (every container has a small side, which is why this is half a solution). Suppose that when viewed from left to right, we have 2 segments $h[i_1]$ and $h[i_2]$ with height $5$. Then clearly any container whose right and small side ends at $i_1$, can be extended to end at $i_2$, and the resulting container is strictly larger. Even further, we see that $i_1$ is made irrelevant by any $i_2>i_1$ and $h[i_2]\geq h[i_1]$. This "being made irrelevant" corresponds to the popping while building the stack, which can be implemented exactly as described above.

So now let's say we went through $i=1$ to $i=n$, and we have our stack. How do we actually calculate the largest containers with segments as the smaller right ends?

Again we go through $i=1$ to $i=n$, but with our stack in hand. Consider $h[1]$. Case 1) it is smaller than the top of the stack (call it $j$) then we can ignore it and move on, since the container formed with left side $h[1]$ and right side $h[j]$ is by definition not the type of container we are considering (we are only looking at right-side-smaller containers). And we can even ignore all containers with left side $h[1]$ and right side $h[j']$ for $j'$ under $j$ in the stack (because it is monotone). Case 2) if $h[1]\geq h[j]$, then $1$ is the best possible left side for a container whose right small side is $h[j]$. Ditto with any $j'$ under $j$ in the stack, which satisfies $h[1]\geq h[j]$. So we pop from the stack until we have some $h[1]< h[j]$, calculating the area each time, then continue with $i=2$, etc. It's not hard to prove that the stack empties, and that each time you pop an element from the stack, you have calculated the largest container with that element as its smaller right side.

Answer 2

UPDATE: Since posting this question I made some progress on my own. Since this question did not attract any other answers I thought I'd add what I came up with.

My conclusion is my original insight into the problem was incomplete. While the "only-advancing-lesser-index-can-increase-area" insight is true, and in the right direction, there is a deeper insight which simplifies the proof substantially.

I won't write it out completely, but I will provide an intuitive sketch.

Key Insight: For any given choice of endpoints, the container produced is the strict maximum of any other containers formed using the lesser endpoint and moving the other endpoint "inward" toward it. This means all those cases can be excluded without computing their area. Advancing the lesser index at each step is doing just that, skipping checking all the cases known to be lower. This brings the time complexity down from O(n^2) to O(n).

Here's a sketch of a proof:

• L and R are the heights of the left and right walls respectively. By convention, L is the lesser (or equal) of the two. The sequence could be reversed as needed to put the lesser on the right if you wanted and all the argumentation would still hold.

• H' <= H. The height of the container can never be greater than it already is because L is unchanged. There are two cases:

  • If R' >= L, min(R', L) = L and so H' still equals L.
  • If R' < L, min(R', L) = R' and H' < H.

• W' < W. Because we are moving R "inward", all containers so produced will be narrower.

• => H' ✕ W' < H ✕ W

  => A' < A for all remaining containers starting at lidx and those can be eliminated from consideration.