About
PUMA is a model checker written in Java. It can verify if a puzzle game is solvable or not. This puzzle is moddeled in a custom-made language called InPUMA (examples are provided in the downloadable package), and is translated to an internal representation based on a data structure called binary decision diagrams (BDDs). These BDDs can be represented as graphs and printed to PGN files. Also, a number of huristics can be turned on which in some puzzles yield a performance improvement (and in others they might be ineffective or even produce worse results - see the article for an explanation on this).
Download
- PUMA: Report.
- PUMA: Slides for the report.
- PUMA: Binaries and source (also includes the report and several example models).
Screenshots
