Making the water gallon brainteaser rigorous

I would approach this as a problem in finding paths through a graph.

Let the vertices of the graph be the pairs $\def\gn#1#2{\left\langle {#1}, {#2}\right\rangle}\gn ab$ where $0\le a\le 4$ and $0\le b \le 7$. Directed edges on the graph from $\gn ab$ are of three types:

1. To $\gn 0b$ and $\gn a0$, for emptying a bucket.
2. To $\gn 4b$ and $\gn a7$, for filling a bucket.
3. To $\gn {a+x}{b-x}$, where $x=\min(4-a, b)$, for pouring bucket 7 into bucket 4, and to $\gn {a-y}{b+y}$, where $y=\min(a, 7-b)$, for pouring bucket 4 into bucket 7.

We can trim the graph to omit all the nodes that are not reachable from the initial position $\gn 00$, and all the edges incident to those nodes. For example, there is no way to reach position $\gn 11$, which has 1 gallon in each bucket. (To see this, just ask what the quantities could have been just prior to the last move.)

The edges are directed, and we can do a breadth-first enumeration of the nodes reachable from the initial position $\gn00$, and delete all the "back edges", which are edges that point from a node back to a previously-visited node. These correspond to suboptimal solutions for example, suppose we know a sequence of moves $S$ that solves the problem from position $\gn 40$. Then a complete solution starting from $\gn 00$ is: fill bucket 4, then do $S$. Another complete solution starting from $\gn 00$ is: Fill bucket 7, then fill bucket 4, then empty bucket 7, then do $S$. Eliminating the "back edge" from $\gn47$ to $\gn40$ removes this solution from the graph.

We then get something like this:

The blue node $\gn 00$ at the far left is where we start. The green nodes are nodes of interest where we have measured exactly $n$ gallons into bucket 7, for various $n$. The solution you want, $\gn05$, is the rightmost green node on the bottom path. We see that there is exactly one solution with minimal moves, corresponding to the one path from the blue node $\gn00$ to this green node.

Your alternative solution through $\gn43, \gn30, \gn46, \gn42, \gn 20, \gn45$ is the other path through the graph, along the top row of nodes, and then against the arrows after reaching $\gn20$ on the far right.

If you want to find all the ways to measure 5 gallons, you can leave in the back edges. Then the graph is much more complicated:

Node $\gn 50$ is the red node in the middle of the diagram. I left in the back edges, except the ones leading back to the starting position $\gn 00$. There are now an infinite number of solutions, all of them silly variations on the unique shortest solution, which you can see snaking its way along the middle. For example, after you get to $\gn 44$ you can empty bucket 4 and refill it again as many times as you want before continuing onward to $\gn 17$. Later once you get to $\gn 41$, you can return to $\gn 40$, essentially starting over.

The classic solution is programmed at the Water Pouring Problem demonstration. For this case, you make a 60-degree parallelogram with sides 4 and 7, label the sides with 0 to 7 and 0 to 4, and start a beam on the 120 degree corner.

As the beam hits the sides of the parallelogram, it marks out steps in the solution.