Nonogram solver [5 points]

Nonogram is a puzzle in which we are given an encoded description of a picture and the task is to determine the picture. In the puzzle, we are given a rectangle grid, each column and row is tagged with a sequence of numbers the determine the lengths of blocks of black cells in that row and column. The task is to paint some cells black to satisfy the constraints.

Your task is to implement a solver of the nonogram puzzle that is based on using SAT/SMT solver.

Extended description

The input has form of a text file that is similar to DIMACS format of describing CNF formulas. It starts with a header line nonogram n m where n denotes the number of rows and m denotes the number of columns of the grid. After the header line, there are n lines describing the sequences associated with the rows and m lines describing the sequences associated with the columns. Each line is a sequence of positive integers ended with 0 (as in DIMACS CNF format). A line that contains only a 0 represents an empty sequence which means that the corresponding row or column does not have any black cells. The input file may contain empty lines and comment lines starting with c. An example of the file is as follows:

c Nonogram describing letter P
nonogram 11 8
c rows
0
4 0
6 0
2 2 0
2 2 0
6 0
4 0
2 0
2 0
2 0
0
c columns
0
9 0
9 0
2 2 0
2 2 0
4 0
4 0
0