This is a great right-sized example problem to tackle, thanks for sharing it. Reading through this really made planning click for me, and made me realize the underlying sameness of planning, pathfinding, and model verification.
One note: "there's no way to order things to guarantee all of the n+1 steps are searched before any n+2 step" -- there is, you just need a priority queue instead of a FIFO queue. Then you are essentially using Dijkstra's algorithm to find your best plan. This seems to be essentially what picat is doing if I'm understanding the picat code correctly -- it is memoizing for each state seen and picking the minimum next cost at each step.
This is a great right-sized example problem to tackle, thanks for sharing it. Reading through this really made planning click for me, and made me realize the underlying sameness of planning, pathfinding, and model verification.
One note: "there's no way to order things to guarantee all of the n+1 steps are searched before any n+2 step" -- there is, you just need a priority queue instead of a FIFO queue. Then you are essentially using Dijkstra's algorithm to find your best plan. This seems to be essentially what picat is doing if I'm understanding the picat code correctly -- it is memoizing for each state seen and picking the minimum next cost at each step.