Nonograms are picture puzzles based on a grid. A set of numbers for each row and column in the grid describes the lengths of non-adjacent horizontal or vertical stretches of grid cells that are to be colored out. The order of the numbers is significant, as it describes the order of these blocks. By combining column and row information, the player can deduce which particular cells need to be colored. The solution often is some pretty pixel art. See here for a full description.
Conventional approaches to solve nonograms (by hand) first try to find partial solutions, e.g., by deducing which cells must or can't possibly be filled. By repeatedly applying techniques to the puzzle, more and more of the cells are known.
The approach to solve nonograms in this project is much simpler: The set of numbers for each row and column in a nonogram can also be seen as a boolean term that describes which combinations of colored cells are possible (taking just the information for the respective row or column into account).
E.g., consider the following (simple) nonogram:
| | 1 | 1 | 1 | |
| 3 | 1 | 1 | 1 | 3 |
----+---+---+---+---+---+
3 | | | | | |
----+---+---+---+---+---+
1 1 | | | | | |
----+---+---+---+---+---+
1 1 | | | | | |
----+---+---+---+---+---+
1 1 | | | | | |
----+---+---+---+---+---+
3 | | | | | |
----+---+---+---+---+---+
For the topmost row, the following term describes the allowed combination of colored out grid cells (coordinates starting top left):
----+---+---+---+---+---+
#1 3 | X | X | X | - | - |
----+---+---+---+---+---+
#2 3 | - | X | X | X | - |
----+---+---+---+---+---+
#3 3 | - | - | X | X | X |
----+---+---+---+---+---+
(X0Y0 & X1Y0 & X2Y0 & ~X3Y0 & ~X4Y0) |
(~X0Y0 & X1Y0 & X2Y0 & X3Y0 & ~X4Y0) |
(~X0Y0 & ~X1Y0 & X2Y0 & X3Y0 & X4Y0)
For the second row, these are the allowed combinations:
----+---+---+---+---+---+
#1 1 1 | X | - | X | - | - |
----+---+---+---+---+---+
#2 1 1 | X | - | - | X | - |
----+---+---+---+---+---+
#3 1 1 | X | - | - | - | X |
----+---+---+---+---+---+
#4 1 1 | - | X | - | X | - |
----+---+---+---+---+---+
#5 1 1 | - | X | - | - | X |
----+---+---+---+---+---+
#6 1 1 | - | - | X | - | X |
----+---+---+---+---+---+
(X0Y1 & ~X1Y1 & X2Y1 & ~X3Y1 & ~X4Y1) |
(X0Y1 & ~X1Y1 & ~X2Y1 & X3Y1 & ~X4Y1) |
(X0Y1 & ~X1Y1 & ~X2Y1 & ~X3Y1 & X4Y1) |
(~X0Y1 & X1Y1 & ~X2Y1 & X3Y1 & ~X4Y1) |
(~X0Y1 & X1Y1 & ~X2Y1 & ~X3Y1 & X4Y1) |
(~X0Y1 & ~X1Y1 & X2Y1 & ~X3Y1 & X4Y1)
The number of allowed combination depends on the sizes of the blocks and the width or height of the entire grid.
The solution of a nonogram satisfies all row and column terms, i.e. at least one of the combinations must be true for a valid coloring of the grid. Thus, the column and row terms are ANDed together. This forms an equation that returns true for every valid solution of the nonogram.
A SAT solver is used in this project to generate a solution that satisfies the equation deduced from the nonogram puzzle specification.
Of course, I am not the first who has had this idea. Here is some related work:
The idea is one thing, the actual implementation is another :)
First, we need a way to store nonograms in machine-readable format. For this purpose, I use the following straightforward structure in JSON files:
{
"cols": [[3],[1,1],[1,1],[1,1],[3]],
"rows": [[3],[1,1],[1,1],[1,1],[3]]
}
Both "rows" and "cols" in the top-level dictionary contain a list of tuples
describing the rows and columns, respectively.
Next, we need to generate all possible combinations for each row and column. This is done in Python using a simple recursive algorithm that traverses the tree of solutions following the starting position of the first block.
From these combinations (in a list of lists in Python), we next need to generate the boolean equations for each row and column, each consisting of the terms describing all possible combination inside a row or column ORed together. The boolean equations for rows and columns are then ANDed together. For this purpose, we need a library that allows us to generate symbolic boolean expressions of which multiple exist for Python 3. In this project, PyEDA is used which conveniently also includes PicoSAT. PyEDA per default also simplifies the term on-the-fly when modifying a boolean expression.
Once the combination of column and row terms is complete, we have a boolean equation that returns True for any valid solution, which we can find using a SAT solver. However, most SAT solvers I encountered require the constraints in CNF. This means we need to transform our arbitrary boolean expression into CNF first. Luckily, PyEDA has us covered here: It provides multiple ways to convert an arbitrary expression into CNF:
.to_cnf() transforms to CNF .tseitin() uses Tseitin's encoding to obtain a more compact CNF (with the help of additional variables). This is the method I use to convert the term to CNF.The most important step follows now: Using PyEDA's built-in version of picoSAT, we generate a valid solution for the term describing the nonogram.
Finally, we convert the symbolic variable names back into coordinates and print out a ASCII graphic of the solution.
This is how the solver looks in action (solving a small nonogram)
This project was a fun little exercise for me to learn about SAT solvers and encoding problems for them. It is not a very fast or efficient way to solve nonograms, especially larger ones.
The code can be found here