So, I was wasting time before going to bed last night, like, by setting up this site, and by playing Sokoban. KSokoboan to be precise. Now, I made it up to level 12 of David W. Skinner's Microban level set, which is rightfully said to be pretty easy. Well, level 12 wasn't, at least not to me. (I admit that that's embarassing, but who cares.)
So, I made it to the "I can prove this unsolvable" stage of puzzle solving. But since I reckoned that someone would have noticed that this level is unsolvable, my mind immediately went to cheating. Unfortunately, nobody had published move sequences to solve Microban. I was absolutely clueless as to how this level might be solvable, and I just had to know. So, I wrote a Python program to solve Sokoban levels. You'll find sokosolve.py and a few demo levels in the sokoban-solver module of my 2004-public arch tree.
The program itself has two nested applications of A*, a usable (but half-baked) heuristic and a complete game model. In just 215 lines. Python never fails to impress me. Attached to this story you can see a dump of the program solving the level that had me so confused.