Representing Minesweeper Constraints in Sat4J/CNF

Question

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.

score 0 · Accepted Answer · answered Mar 17 '18 at 08:19

0

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/

answered Mar 17 '18 at 08:19

Daniel Le Berre

161
3

Whilst the link provided didn't have what I was looking for, searching the SAT4J API for cardinality constraints gave me exactly the methods I was looking for. Thanks. – FRRXX Mar 18 '18 at 18:56

Representing Minesweeper Constraints in Sat4J/CNF

1 Answers1