Improve Nurikabe example

[Skynet0]

The Nurikabe solver is, quite slow when given harder puzzles that have more initial freedom:

E.g. https://puzz.link/p?nurikabe/10/10/p2q8j7m2h7zh4h8m4j2q6p

HEIGHT, WIDTH = 10, 10
GIVENS = {
    (1, 0): 2,
    (2, 2): 8,
    (2, 7): 7,
    (3, 5): 2,
    (3, 8): 7,
    (6, 1): 4,
    (6, 4): 8,
    (7, 2): 4,
    (7, 7): 2,
    (8, 9): 6
}

I've made some (unpushed) improvements that vastly improve performance on this style of puzzle, by hinting the solver - if cells can be trivially shaded according to givens, then we can require those cells to be shaded, and arbitrarily root the sea at one of those. I also replaced some Implies with == where appropriate, which appear to have made improvements as well. This improves the solve time of the above puzzle from ~10 minutes to ~20 seconds.

However, the solver still struggles on ugly puzzles like
https://puzz.link/p?nurikabe/10/10/5ibj4zp7i9j6zz3i8ja

HEIGHT, WIDTH = 10, 10
GIVENS = {
  (0, 0): 5,
  (0, 4): 11,
  (0, 9): 4,
  (4, 0): 7,
  (4, 4): 9,
  (4, 9): 6,
  (9, 0): 3,
  (9, 4): 8,
  (9, 9): 10
}

I tried fixing the root of the sea at a small set of blocks (if you have two givens close together, then there must be some cells shaded between them), but that hasn't helped much (still 9000 seconds to solve and 2000 seconds to prove unique). I don't know if there's anything else that can feasibly be done, but I'd like to hear your thoughts on whether it's possible to make sparse Nurikabe faster. I did forget to try constraining the sea size as well, but I don't know how much of an effect that will have. (And I'd rather not rely on this - some Nurikabe use ? to indicate a region of unknown size!)

[obijywk]

By all means feel free to send a pull request with Nurikabe-specific "hinting" logic. I guess these should just become part of the Nurikabe example? I wonder if there's some way we should consider library-ifying logic like that to make it easier to apply to multiple puzzle solvers... so far everything in the common grilops library is applicable to more than one puzzle type, and I think I'd like to keep it that way, but I've also found myself copying things like "don't allow 2x2 areas of shaded cells" a few times so maybe there's some opportunity for factoring out common logic like that.

$ grep -r 2x2 examples
examples/nurikabe.py: # The sea is not allowed to contain 2x2 areas of black cells.
examples/tapa.py: # Shaded cells may not form a 2x2 square anywhere in the grid.
examples/nanro.py: # No 2x2 group of cells may be fully labeled.
examples/lits.py: """Add the nurikabe constraints (one connected sea with no 2x2 regions)."""
examples/lits.py: # The sea is not allowed to contain 2x2 areas of black cells.

No brilliant ideas here to speed up the sparse puzzle, though. A few insufficient ideas:

• The RegionConstrainer min_region_size can be set to the smallest given (3 in this case), and the max_region_size can be set to the area of the puzzle minus the sum of the givens. I'll submit this change at least, it seems to slightly speed up the easy example at least.
• The size of the sea region can be constrained to be equal to the area of the puzzle minus the sum of the givens (I suppose you did mention this idea at the end). This seems to speed up the example a bit as well so I'll submit this change too.

I suspect this puzzle just has too large of a search space for z3 to be able to deal with quickly. Building some Nurikabe-specific "hinting" logic rules and using those to further constrain the solver might help, if you can come up with any that would be effective for this sparse puzzle. I can't think of any, but I'm also not much a Nurikabe solver myself :-)