How Windows FreeCell Gave Rise To Online Crowdsourcing
TPIRman writes "In 1994, a physics doctoral student named Dave Ring assembled more than 100 math and puzzle enthusiasts on Usenet for what became one of the earliest online 'crowdsourcing' projects. Their goal: to determine if every hand in Windows' FreeCell solitaire game was in fact winnable, as the program's help file implied. Their efforts soon focused in on one incredibly stubborn hand: #11,982. They couldn't beat it, but in the process of trying, they proved the viability of an idea that would later be refined with crowdsourcing models like Amazon's Mechanical Turk."
Unless the exploration of the game space was exhaustive, there's no proof.
Wikipedia claims that exhaustive search has been performed, assuming that the same hand numbering is used:
http://en.wikipedia.org/wiki/FreeCell#Impossible_games
This was also done at about the same time in the UK, by a group of people on Cix (a CoSy conferencing system), with the same conclusion, except we found two more unsolvable ones that I suspect the American team didn't look at: -1 and -2. For what it's worth, I invented the notation we used to document solutions, and one of the team produced a solver that exhaustively checked the game space for 11 982 and indeed found it impossible. So give or take formal proof of the solver's correctness, it is proven that not all games are solvable.
Quidnam Latine loqui modo coepi?
http://en.wikipedia.org/wiki/Proof_by_exhaustion
Here's a program that does it.
http://kurage.nimh.nih.gov/tomh/public_html/archives/patsolve-3.0.tgz
The program generates a list of axioms, followed by a list of transformations chosen from a finite set.
After a finite number of steps, the proof reaches a conclusion that that game (and that's the only one
out of the original 32000) is unsolvable. This is a real, valid mathematical proof. It's just very long
and hard to read. But it is of finite size, and follows all the normal rules of mathematical proof.
You're welcome to try to come up with a shorter proof.
FreeCell is not np-anything. It's a finite tree that can be exhaustively searched.
Generalized FreeCell is NP-Complete.
The article seemed to imply that it was proved unwinnable, but never absolutely stated it..
I found something a little better: http://www.solitairelaboratory.com/fcfaq.html
11982 has now eluded solution by probably thousands of human solvers, and at least eight independent computer programs I am aware of (most of which are designed to search exhaustively for a solution), and I am confident in calling it impossible.
I really wish the FAQ had been linked from the slashdot summary, it's far more interesting, and better written than the gaemological.com article.
As I understand the quote above, there is at least 5 different programs (ie. more than half of "at least eight") that have solved hand 11982, and all arrived at the same solution: #11982 is not winnable. This has persuaded the FAQ's author to call [winning the hand] impossible.
Free unix account: freeshell.org