Description

Model checkers are used to verify properties (written in a specification language) on labelled transition systems. A model checker is used to automatically check whether or not the given property is satisfied or violated. In case the property is violated, a counter-example is returned (i.e. a trace leading to a state that violates the property).

Besides verifying correctness of hardware and software, model checkers can also be used to solve puzzles. In case of a Sokoban puzzle, one can model its state space and provide the property that the puzzle cannot be solved. If the model checker finds a counter-example, the returned trace corresponds to a solution of the puzzle.

The LTSmin model checker can be used in combination with its dlopen interface to specify the state space in C code. The task is to construct a program that automatically generates the Sokoban state space and property, for given input puzzles. Then, LTSmin can be used to solve the puzzle by using its distributed, multi-core and/or symbolic algorithms. You are encouraged to experiment with different methods for representing the puzzle, since this can significantly reduce the resulting state space (which generally improves the model checking performance).

Besides Sokoban, you can also work on code generation for different puzzles/problems (e.g. solving the sliding puzzle), feel free to provide suggestions.

References

1. Online Sokoban puzzles (Digital version available here)
2. The LTSmin website (Digital version available here)
3. LTSmin tool paper (Digital version available here)

Additional Resources

1. The paper