Search code examples
javasatsat4j

Representing Minesweeper Constraints in Sat4J/CNF

I'm trying to implement a minesweeper solver using a SAT solver (sat4j) and I have a simple understanding of how they work. But one thing I can't figure out is how to represent the x+y+Z+....=2 for mines, since SAT solvers use Boolean input. Something such as in the table below:

| a | b | c | d | e |
| f | 2 | g | 3 | h |
| i | j | k | l | m |

You could write a+b+c+f+g+i+j+k = 2 and c+d+e+g+h+k+l+m= 3.

Solution

  • if by a+b+c+f+g+i+j+k = 2 you mean that the surrounding cells contain exactly two mines, then your letters really are Boolean variables, and that constraint is called a cardinality constraint.

    This is supported out of the box by Sat4j.

    You may find some hints here: https://sat4j.gitbooks.io/case-studies/content/