Note that traditional SAT and SMT solvers are quite inefficient at computing flood-fills.
The ASP specifications it uses to compute optimal solutions are surprisingly short and readable, and look like:
#const budget=11.
horse(4,4).
cell(0,0).
boundary(0,0).
cell(0,1).
boundary(0,1).
% ...truncated for brevity...
cell(3,1).
water(3,1).
% ...
% Adjacent cells (4-way connectivity)
adj(R,C, R+1,C) :- cell(R,C), cell(R+1,C).
adj(R,C, R-1,C) :- cell(R,C), cell(R-1,C).
adj(R,C, R,C+1) :- cell(R,C), cell(R,C+1).
adj(R,C, R,C-1) :- cell(R,C), cell(R,C-1).
% Walkable = not water
walkable(R,C) :- cell(R,C), not water(R,C).
% Choice: place wall on any walkable cell except horse and cherries
{ wall(R,C) } :- walkable(R,C), not horse(R,C), not cherry(R,C).
% Budget constraint (native counting - no bit-blasting!)
:- #count { R,C : wall(R,C) } > budget.
% Reachability from horse (z = enclosed/reachable cells)
z(R,C) :- horse(R,C).
z(R2,C2) :- z(R1,C1), adj(R1,C1, R2,C2), walkable(R2,C2), not wall( R2,C2).
% Horse cannot reach boundary (would escape)
:- z(R,C), boundary(R,C).
% Maximize enclosed area (cherries worth +3 bonus = 4 total)
#maximize { 4,R,C : z(R,C), cherry(R,C) ; 1,R,C : z(R,C), not cherry( R,C) }.
% Only output wall positions
#show wall/2.[1] https://github.com/spack/spack/blob/develop/lib/spack/spack/...
Therefore, like a good little llm bitch that I have become recently, I straight away went to chatgpt/sonnet/gemini and asked them to compile me a list of more such "whatever this is known as". And holy cow!! This is a whole new world.
My ask to HN community: any good book recommendations related to "such stuff"? Not those research kinds as I don't have enough brain cells for it. But, a little easier and practical ones?
Thanks..
1. Symbolic reasoning
2. SAT/SMT/ASP
3. pre-machine-learning formulations of AI
"Declarative programming"[1] is kind of a superset of logic programming, which may or may not be the aspect that piques your interest.
"Constraint programming"[2] and "Constraint logic programming"[3] are also a perspective on it.
[0] https://en.wikipedia.org/wiki/Logic_programming
[1] https://en.wikipedia.org/wiki/Declarative_programming
[2] https://en.wikipedia.org/wiki/Constraint_programming
[3] https://en.wikipedia.org/wiki/Constraint_logic_programming
- https://www.cs.utexas.edu/~vl/teaching/378/ASP.pdf
It starts with basics of using ASP and gives examples in clingo, not math.
The Potassco book is more comprehensive and will help you understand better what is going on:
Things I don't like include that it's more dense, doesn't use clingo examples (mostly math-style examples so you kind of have to translate them in your head), and while the proofs of how grounding works are interesting, the explanations are kind of short and don't always have the intuition I want.
I still think this is the authoritative reference.
The "how to build your own ASP system" paper is a good breakdown of how to integrate ASP into other projects:
- https://arxiv.org/abs/2008.06692
The Potassco folks are doing amazing work maintaining these tools. I also wish more people knew about them.
EDIT: I forgot to mention that specifically for games stuff like enclose.horse, look at Adam Smith's Applied ASP Course from UCSC:
- https://canvas.ucsc.edu/courses/1338
Forgot to mention that one... we use clingo in Spack for dependency solving and other applications frequently slip my mind.
Great, now I've been double nerd-sniped - once for the thing itself and another for 'What would an optimiser for this look like? Graph cuts? SAT/SMT? [AC]SP?'
The Leetcode version of this is "find articulation points", which is just a DFS, but it's less general than what is presented here.
Edit: apex-4-regular
Is NP hardness proven for just planar graphs? Those are closer to the 2D grid, but still slightly more general. All I could find was a reduction to densest k subgraphs, but Wikipedia tells me that whether that problem is NP hard for planar graphs is an open question.
To be clear, I would be very surprised if the problem turns out to be _not_ NP hard, but there is no trivial equivalence to min cut in general graphs to show that it is.
It might be polytime on planar graphs, but that would be surprising.
For example, in a grid like this:
..####
.....#
#.#..#
#...H#
######
A single wall placed (i.e. vertex removed) can block two edges, and it's not obvious what graph transformation can turn that into a single edge.There is a standard construction for going between vertex and edge cuts.
See
https://gist.github.com/Macuyiko/86299dc120478fdff529cab386f...
You can more precisely track flows and do maximization with ILP, but that often loses conflict-driven clause learning advantages.
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.
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!https://cs.stackexchange.com/questions/176005/how-to-remove-...