Player (136)
Joined: 9/18/2007
Posts: 389
many things already done, but not functional at the moment. When I tried it with the full puzzle, my machine was quite close to a system crash. The small test puzzle uses 16242 clauses, the real one requires about 4 million clauses to describe the game and all the intermediate states... I am not that sure if I continue this one. I somehow got the impression that brute-forcing might still be faster than this solver.
Player (136)
Joined: 9/18/2007
Posts: 389
My solver, SAT approach, WIP2, + the required framework. You also need minisat.exe or picosat, for example here: http://minisat.se/downloads/MiniSat_v1.14_cygwin (rename the file after the download). It works, but only for very small puzzles.