Solving the Whole Year Puzzle with Z3
6 days ago
- #puzzle-solving
- #algorithm
- #Z3-solver
- The Whole Year Puzzle is a tile-based puzzle where the goal is to fit polyominoes into a grid, leaving only two cells (representing the day) uncovered.
- The author initially considered using Knuth's Algorithm X (DLX) but opted for Z3, an SMT solver, to explore SAT solving.
- The puzzle is converted into a matrix where each row represents a valid polyomino placement and each column represents a cell in the puzzle grid.
- Z3 is used to model the problem by creating Boolean variables for each placement and adding constraints to ensure each cell is covered exactly once (except for the day cells).
- The solver checks for solutions and can enumerate all possible solutions by adding constraints to exclude previously found solutions.
- Results show that each day of the year has a different difficulty level, with the month being the main factor in difficulty.
- The author experimented with rearranging the months and days to create a more consistent difficulty progression, resulting in a less intuitive but more challenging arrangement.
- The full code and analysis are available on the author's GitHub repository.