# Find partial solution for underdetermined system of Boolean equations (Minesweeper)

In this article about creating a Minesweeper solver, the author talks about using matrices to solve given portions of a Minesweeper board. While reading that, I thought of a different way to limit the domain to {0,1}: instead of using substitutions after RowReduce, use Boolean algebra, specifically counting functions. But here I run into a problem: using SatisfiabilityInstances gives one or more solutions, but unless if all of the instances are compared, I (and the code) wouldn't know which of the hundreds or thousands of variables have the same value in all instances, i.e. are guaranteed. (One does not want to make unnecessary guesses in Minesweeper!) Is there some way to get the complete solution domain (e.g. {a,b,c}->{True, False, Unknown}) without going through all of the possibilities?

EDIT: Here is a more specific example. Start with this Minesweeper layout:

abcd
#22e
##2f
###g


(The #s indicate nonspecific squares assumed by the numbers to be non-mines. If they do contain marked mines, adjust the numbers accordingly. This won't really matter that much for this example, though.)

The corresponding matrix (formatted according to the link) is this:

[1 1 1 0 0 0 0 | 2]
[0 1 1 1 1 1 0 | 2]
[0 0 0 0 1 1 1 | 2]


which row-reduces to:

[1  0  0 -1  0  0  1 | 2]
[0  1  1  1  0  0 -1 | 0]
[0  0  0  0  1  1  1 | 2]


The first row indicates that a and g are mines, and that d isn't. However, the code doesn't know that without the restriction to the domain of {0,1}, which would be a suitable alternative, but I don't know how to implement that.

(Incidentally, which RowReduce method would be best for this application, if the domain problem is solved? The documentation doesn't go into the specifics of what each method does.)

The corresponding Boolean function would be something along the lines of this:

And[BooleanCountingFunction[{2}, 3][a, b, c],
BooleanCountingFunction[{2}, 5][b, c, d, e, f],
BooleanCountingFunction[{2}, 3][e, f, g]]


What I was wanting was a function boolsolve[eqns,vars] to output something along the lines of {a->True,d->False,g->True} in this particular instance, and similarly for other starting positions, once they're marked suitably; I feel like I might be able to handle the marking portion of the code. (After reconsideration, I realized that the Unknowns in the results would just get in the way.)

(Said function could also operate off of just a list of the counting functions; one just needs to substitute in Apply[And,list] for the equation above.)

• There isn't really enough code or description here to determine what it is you are trying to do. It would be good to have in this post a smallish example of the input and desired output, extracted from the Minesweeper world and just translated into text and code. – Daniel Lichtblau Apr 4 '16 at 22:51
• @DanielLichtblau Added an example, and realized that this problem might just come down to a domain restriction after a RowReduce. – 404UserNotFound Apr 5 '16 at 5:25
• Re formatting, it is better to use cut-and-pastable Mathematica InputForm. – Daniel Lichtblau Apr 5 '16 at 14:42

One approach is to place inequality and domain restrictions in Solve. I show this below, using the example in the post.

mat = {{1, 1, 1, 0, 0, 0, 0}, {0, 1, 1, 1, 1, 1, 0}, {0, 0, 0, 0, 1,
1, 1}};
vars = Array[x, Length[mat[[1]]]];
rhs = {2, 2, 2};

• No, this is not what I'm looking for, as it displays all of the results, like with SatisfiabilityInstances; this would easily be resolved by looking through all of the possibilities and figuring out which variables have the same values over all of them. I'm looking more for something like SolveAlways, if it included an option for a choice of domain like Solve does. (SolveAlways apparently doesn't look through all possibilities, as there are infinitely many possibilities in any non-discrete domain.) Or is there no better way to do such a thing, since Minesweeper is NP? – 404UserNotFound Apr 5 '16 at 22:38
• You can iterate FindInstance with similar conditions and alternately setting a specific variable to 0 or 1. Any time you get no solution for one case you have forced that variable to take on the other value. Any time both give solutions it gets "unknown". – Daniel Lichtblau Apr 5 '16 at 23:33