algorithmdynamic-programmingproofcorrectnessproof-of-correctness

Proof of dynamic programming solution for Leetcode 818: Racecar


The problem is as follows:

Problem:

"Your car starts at position 0 and speed +1 on an infinite number line. Your car can go into negative positions. Your car drives automatically according to a sequence of instructions 'A' (accelerate) and 'R' (reverse):

When you get an instruction 'A', your car does the following:

When you get an instruction 'R', your car does the following:

For example, after commands "AAR", your car goes to positions 0 --> 1 --> 3 --> 3, and your speed goes to 1 --> 2 --> 4 --> -1.

Given a target position target, return the length of the shortest sequence of instructions to get there."

Source: https://leetcode.com/problems/race-car/description/

Proposed DP solution:

Let DP[i] be the number of instructions needed to travel a distance "i" in the right-hand direction.

Then DP[0] = 0

For our update rule, there are 3 cases.

  1. First reach some j < i without reversing, then reverse and travel some distance to k < j. Finally, reverse again and use the previously solved DP[i-k]

  2. First, reach some j > i without reversing, then reverse and use the previously solved DP[j-i]

  3. We can reach i without reversing

According to the above update rules, we can solve from DP[0] to DP[i] to obtain our solution.

Issue:

This seems to be the widely accepted DP solution to this problem, but I have yet to find a satisfying proof, or even any proof at all, that this algorithm is correct.

For example, how could one prove that the optimal way to traverse a distance "i" isn't to immediately reverse and go to some a < 0, then reverse and travel to some j > i, and finally reverse again and use DP[j-i]?

Or how could one prove that the optimal way to traverse a distance "i" isn't to overshoot to a distance j > 2i, and then reverse and travel a distance 2i - j > i, which is a subproblem that would not yet have been solved?

Many "proofs" I come across make vague statements such as "it should be clear that you don't want to go overshoot to j > 2i" and so on which is less than rigorous.

My current thoughts:

At the moment, I can at least put forth what I think is a valid proof to prove that we would never want to first reverse to some a < 0, then reverse to some j > i, and then make our way back to DP[j-i].

My proof for this is that in this case, we would reverse a total of 3 times. Rather than do this, we could simply make our way to j + a without reversing, then reverse once and go to j, then reverse twice (reverse once to set speed to 0, and then reverse again to point back towards i) and go to i. I believe this should result in the same amount of steps in the end.

However, I still have trouble proving why we would never overshoot to some j > 2i and then make our way back to i?

If anyone could provide a proof for this solution, that would be much appreciated, thank you!


Solution

  • why we would never overshoot to some j > 2i and then make our way back to i?

    Well, how would we get there? Call the vector (the last jump) that led there v.

    If we issued v from a position after i, that would be redundant as we can use the recurrence we defined for j > i without the v jump.

    And if we issued v from before i to get to a distance greater than 2*i, it's simple: we can't. Aside from i = 2^p - 1, which has a trivial solution, we cannot achieve a magnitude greater than i / 2, necessary to leap farther than i, before i.

    (Note that the interpretation of j > i is taken from the recurrence explanation at https://leetcode.com/problems/race-car/solutions/124326/summary-of-the-bfs-and-dp-solutions-with-intuitive-explanation)


    We can prove that going below position 0 is unnecessary by observing that any sequence s starting at 0 and ending at some lowest point l below zero will have a subsequent sequence s' that starts by going higher and takes it all the way to i, never going as low as l. We can switch the order so that s' is executed first and then s. There are two cases, depending on the direction s' ends in.

    One case is when s' ends going left (note that the drawing makes the rightmost point of s and s' the same as their visual right end but the rightmost point in their sequence could be farther):

    <--------0------------->s
    -----------<-->s' (ending <-)
    l          i
    
             0----------<-->s'
               <--------x------------->s
               i
    

    When s' ends going right, define V as the first section of s until it first reverses to go below zero, and define U as the first vector of s' (we defined it already as going right).

    If V's magnitude is smaller than or equal to Us, merge V with s' and apply V again at the end:

               Vector V going right
    <--------0--V-->s
    U------->----------->s' (ending ->)
    l                   i
    
             0------->----------->s'
                  <--------x--V-->s
                  ---V-->
                        i
    

    If V's magnitude is greater than Us, apply V instead of U and apply U at the end:

    Vector V going right
    <--------0-V--->s
    U-->---------------->s' (ending ->)
    
    l                   i
               V
             0-V--->---------------->s'
                     <--------0-V--->s
                     U-->
                        i