Efficient Domain Reduction Only Possible?

[Mr Proof]

I am trying to find a good domain reduction library that does the following:

Imagine, the game of Minesweeper on Windows. 
Each cell has certain options (bomb 💣/not-bomb) etc.

And the numbers in the cells give constraints e.g. c1+c2+c3+..c8=5

My requirements are to use domain reduction to find forced bombs, and forced-empties.
But, I would like it to use efficient domain reduction algorithms and not simply aggregate all possible models (except as a last resort). As an example, a similar program exists here: https://cse.unl.edu/~minesweeper/version1/minesweeper/ Which uses GAC and similar things. A solution which simply aggregates every possible model would be very inefficient in most cases.

For a game like mineswepper in most cases the puzzle cannot be fully solved in one go. Thus, I am interested in simply reducing the domain of as many cells as possible.

(I am giving the example of a Minesweeper solver, but I have more general problems in mind).

OR-Tools seems a good tool as it has C# API, which I require but I'm not sure if it does efficient domain reduction or if it is more optimised towards finding complete models.

Can you suggest if OR-Tools is the right tool for the job or whether another library would be more suited? (e.g. gecode?) Or should I write it myself? (I am a decent programmer but I doubt I could match the efficiency of dedicated lilbraries).

Thanks

[christoph...@gmail.com]

Once you have a model set up, the Google OR-Tools is pretty efficient at finding a solution. The model could have n x n bool variables "there_is_a_mine_here" and n x n variables of ints "cell_number" with domain 0 to 8, and constraints that make the  "cell_number"  equal to the sum of the "there_is_a_mine_here" of the adjacent cells.

The already uncovered cells could then be assigned as cell_number == constant in value. 

But you are not looking for a "solution" to this model-- there will be many, with the program simply assigning arbitrary values to unknown cells such that the constraints are all satisfied.

What you are interested in is finding domain reductions. With the old Google.OrTools.ConstraintSolver you could hook in at the end of the "initial constraint propagation" before the first "decision" is taken (basically making a guess about an unknown cell), and look at the domains of the variables, stopping there and not proceeding to find "solutions". After the initial propagation, the variables now "bound" to a single value will reveal spaces which are guaranteed free or mined.

 In Minesweeper, as play goes on, each new cell uncovered adds a new constraint so the model would have to be modified after each turn to add that constraint, and then the search restarted.

Since you never need to remove constraints, which would require a new model, but only add them, this would be possible in principle.

But my guess is that writing a dedicated program for Minesweeper is going to get you better performance, because you can optimize it for solving this single exact problem.