6 ms·

Yes. CP SAT crunches through it in no time, but of course larger grids would quickly make it take much longer. See https://gist.github.com/Macuyiko/86299dc120

Yes. CP SAT crunches through it in no time, but of course larger grids would quickly make it take much longer. See https://gist.github.com/Macuyiko/86299dc120478fdff529cab386ffd14a https://gist.github.com/Macuyiko/86299dc120478fdff529cab386f...

ooopdddddd 8mo ago
I don't believe this works in general. If you have a set of tiles that connect to neither the horse nor to an exit, they can still keep each other reachable in this formulation.
- Scaevolus 8mo ago
  Yes, this is the major challenge with solving them with SAT. You can make your solver check and reject these horseless pockets (incrementally rejecting solutions with new clauses), which might be the easiest method, since you might need iteration for maximizing anyways (bare SAT doesn't do "maximize"). To correctly track the flood-fill flow from the horse, you generally need a constraint like reachable(x,y,t) = reachable(nx,ny,t-1) ^ walkable(x,y), and reachable(x,y,0)=is_horse_cell, which adds N^2 additional variables to each cell. You can more precisely track flows and do maximization with ILP, but that often loses conflict-driven clause learning advantages.
- Macuyiko 8mo ago
  Good point. I don't think the puzzles do this and if they would, I would run a pre-solve pass over the puzzle first to flood fill such horseless pockets up with water, no?
  - ooopdddddd 8mo ago
    It's not quite that easy. For the simplest example, look at https://enclose.horse/play/dlctud https://enclose.horse/play/dlctud, where the naive solution will waste two walls to fence in the large area. Obviously, you can construct puzzles that have lots of these "bait" areas. Like the other comment suggested, running a loop where you keep adding constraints that eliminate invalid solutions will probably work for any puzzle that a human would want to solve.
    - Macuyiko 8mo ago
      Oh I see what you mean now, indeed: Score: 7 ~~~~~~ ~····~ ~·~~·~ .#..#. ...... ..#... .#H#.. ..#... However, I think that you do not need 'time' based variables in the form of reachable(x,y,t) = reachable(nx,ny,t-1) Enforcing connectivity through single-commodity flows is IMO better to enforce flood fill (also introduces additional variables but is typically easier to solve with CP heuristics): Score: 2 ~~~~~~ ~....~ ~.~~.~ ...... ...... ..##.. .#H·#. ..##.. Cool puzzle!

ooopdddddd 8mo ago

I don't believe this works in general. If you have a set of tiles that connect to neither the horse nor to an exit, they can still keep each other reachable in this formulation.

Scaevolus 8mo ago
Yes, this is the major challenge with solving them with SAT. You can make your solver check and reject these horseless pockets (incrementally rejecting solutions with new clauses), which might be the easiest method, since you might need iteration for maximizing anyways (bare SAT doesn't do "maximize"). To correctly track the flood-fill flow from the horse, you generally need a constraint like reachable(x,y,t) = reachable(nx,ny,t-1) ^ walkable(x,y), and reachable(x,y,0)=is_horse_cell, which adds N^2 additional variables to each cell. You can more precisely track flows and do maximization with ILP, but that often loses conflict-driven clause learning advantages.
Macuyiko 8mo ago
Good point. I don't think the puzzles do this and if they would, I would run a pre-solve pass over the puzzle first to flood fill such horseless pockets up with water, no?
- ooopdddddd 8mo ago
  It's not quite that easy. For the simplest example, look at https://enclose.horse/play/dlctud https://enclose.horse/play/dlctud, where the naive solution will waste two walls to fence in the large area. Obviously, you can construct puzzles that have lots of these "bait" areas. Like the other comment suggested, running a loop where you keep adding constraints that eliminate invalid solutions will probably work for any puzzle that a human would want to solve.
  - Macuyiko 8mo ago
    Oh I see what you mean now, indeed: Score: 7 ~~~~~~ ~····~ ~·~~·~ .#..#. ...... ..#... .#H#.. ..#... However, I think that you do not need 'time' based variables in the form of reachable(x,y,t) = reachable(nx,ny,t-1) Enforcing connectivity through single-commodity flows is IMO better to enforce flood fill (also introduces additional variables but is typically easier to solve with CP heuristics): Score: 2 ~~~~~~ ~....~ ~.~~.~ ...... ...... ..##.. .#H·#. ..##.. Cool puzzle!