I am currently trying to solve the puzzle "Kuromasu" with a SAT solver, that takes input in the common DIMACS format, i.e. as Conjunctive Normal Form (CNF).
In Kuromasu, you have a rectangular board with mxn cells. A cell is either black or white. The goal of the game is to decide which cell is which color. Some of the cells contain a number. Cells that contain a number are always white. The number tells you how many cells, including itself, are supposed to be visible from this cell. All white cells in the same row and column are visible, up to the first black cell.
Example 5x4 grid, # represents a black cell:
___________
| | |#| |2| <-- 2 cells including itself visible
___________
| | |#| |#|
___________
| |#|3| |#| <-- 3 cells including itself visible
___________
| | | | | |
___________
I need to formulate this constraint to find the positions of the black fields in a way the SAT solver understands. I am already able to generate a version in Disjunctive Normal Form (DNF) per number by going through all cells to the left,right,top,bottom of the numbered cell and checking if coloring them black would satisfy the constraint. This gives me a list of possible constellations of black cells in DNF. I encode the game by introducing a variable per cell, if it is false it is black, if it is true, the cell is white. Below are all the variables for the field above (1-indexed, since the DIMACS format specifies false variables as negative integers, and true variables as their positive counterpart):
________________
| 1| 2| 3| 4| 5|
________________
| 6| 7| 8| 9|10|
________________
|11|12|13|14|15|
________________
|..|..| | | |
________________
For only the 2-number constraint from the example above, I would generate the following:
___________
| | | | |2| <-- 2 cells including itself visible
___________
| | | | | |
___________
| | | | | |
___________
| | | | | |
___________
(-4 & -15) | (-3 & -10) (Eq 1.)
This represents both ways the constraint can be followed. However, to input this to the SAT-Solver, I need to convert (Eq 1.) to CNF. I implemented a (naive) converter, which works, but is really slow and memory-intensive due to the complexity of converting to CNF. It is unfeasible to do this for constraints that have more than 4 ways to fulfill them.
How do I formulate the constraint in a way that I can feed directly to the Solver? Is it possible? I've been thinking about this for quite some time, and can't quite get it.
Thanks!
The Tseytin transform mentioned in the comments above works well. Here is some code in java, in case anyone else ever needs it.
Be aware: This is not a full implementation of the Tseytin transform, it just works if the input is already in DNF. The code below is also just an example hacky solution, e.g. it is not very type-safe to have the input and output be essentially the same format, just different interpretations. Feel free to modify as needed.
Edit: For my own safety/ academic honesty, I will add the code once the class assignment for which this was made due date is over (Jan. 8th).