Skip to content

Commit 9fe53a1

Browse files
natsukagaminatsukagami
authored
Something about day 12 (#934)
1 parent 5118e82 commit 9fe53a1

File tree

1 file changed

+224
-0
lines changed

1 file changed

+224
-0
lines changed

‎docs/2025/puzzles/day12.md‎

Lines changed: 224 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,234 @@ import Solver from "../../../../../website/src/components/Solver.js"
22

33
# Day 12: Christmas Tree Farm
44

5+
by [@natsukagami](https://github.com/natsukagami)
6+
57
## Puzzle description
68

79
https://adventofcode.com/2025/day/12
810

11+
## Inspecting the input
12+
13+
Today's problem gives us various shapes contained in a 3x3 box, and asks us whether we can place them in a larger MxN space.
14+
The number of shapes of each kind is given.
15+
16+
This is eerily reminiscent of the [Bin Packing problem](https://en.wikipedia.org/wiki/Bin_packing_problem), therefore we should
17+
expect to figure out some patterns in the input, as the general problem is likely to be untractable.
18+
19+
We are given the following 6 shapes:
20+
21+
```
22+
0:
23+
###
24+
##.
25+
##.
26+
27+
1:
28+
###
29+
##.
30+
.##
31+
32+
2:
33+
.##
34+
###
35+
##.
36+
37+
3:
38+
##.
39+
###
40+
##.
41+
42+
4:
43+
###
44+
#..
45+
###
46+
47+
5:
48+
###
49+
.#.
50+
###
51+
```
52+
Note that they can be rotated and flipped, so the total number of shapes is actually about 72.
53+
54+
The input asks for spaces of size ~2000 (at 40-50 cells for each edge), with the total amount of shapes hovering around a few hundreds, so simply backtracking is not possible (but we tried anyway!).
55+
56+
However, we can weed out some special cases:
57+
- If the space given is spacious enough to fit each shape in its own 3x3 box (i.e. without fitting them together), we can trivially place them:
58+
```scala 3
59+
def triviallyPossible(maxRows: Int, maxCols: Int, requirements: Map[Shape, Int]) =
60+
val totalCount = requirements.values.sum // total number of required shapes
61+
(maxRows / 3) * (maxCols / 3) >= totalCount
62+
```
63+
- If the space given is _not enough to fit the total number of cells occupied by the shapes_, then no matter how we fit them, we cannot fit all the shapes into the given space:
64+
```scala 3
65+
case class Shape(cells: Array[Array[Char]]):
66+
def cellCount =
67+
cells
68+
.iterator
69+
.map(row => row.count(_ == '#'))
70+
.sum
71+
72+
def triviallyImpossible(maxRows: Int, maxCols: Int, requirements: Map[Shape, Int]) =
73+
val totalCellCount =
74+
requirements
75+
.iterator
76+
.map((shape, count) => shape.cellCount * count)
77+
.sum
78+
maxRows * maxCols < totalCellCount
79+
```
80+
81+
Fortunately, **all of our input queries fall into one of these categories!** Therefore, we avoid endless search and grab our last star of the year. Cheers!
82+
83+
## Bonus: Can Z3 solve it?
84+
85+
I have always heard that these NP-complete problems can sometimes be quickly solved by a general purpose SMT solving library, such as [Z3](https://github.com/Z3Prover/z3).
86+
In a nutshell: SMT solvers like Z3 allow us to find solutions to inequalities (called _constraints_ in SMT terms) with multiple variables. So, if we manage to encode the problem as a set of arithmetic inequalities, then perhaps Z3 would give us the answer?
87+
88+
To use Z3 from Scala, I opted for the [ScalaZ3](https://github.com/epfl-lara/ScalaZ3) wrapper made by EPFL's LARA lab.
89+
Unfortunately the library seems to not be able on Maven, so I compiled it myself and manually include it as an unmanaged JAR.
90+
It was painless to compile however (`sbt +package` as the README says does the job), and including it is a single directive with the `scala` command-line as a build tool:
91+
92+
```scala
93+
//> using jar ./scalaz3_3-4.8.14.jar
94+
```
95+
96+
In the code, we can set up a Z3 context as follows, preparing to build our constraints.
97+
98+
```scala 3
99+
import z3.scala.*
100+
val ctx = new Z3Context("MODEL" -> true) // this allows us to receive a specific solution later on
101+
val i = ctx.mkIntSort() // declare an int-like type in the SMT context
102+
// some constants that we shall mention later
103+
val zero = ctx.mkInt(0, i)
104+
val one = ctx.mkInt(1, i)
105+
106+
// as we will build up the complex constraints one-by-one, mutable collections make them easier to work with
107+
val constraints = mutable.ListBuffer[Z3AST]()
108+
```
109+
110+
Now, how do we encode our problem as a bunch of arithmetic inequalities? From a glance, here are the requirements that we have
111+
to encode:
112+
- For shape `i`, we have to use `count(i)` amount of shapes.
113+
- The shapes should be laid on a `N x M` space.
114+
- Layered shapes should not overlap.
115+
116+
A simple way to encode the _choice_ of putting a shape at a specific position, is to turn them into a *binary variable*.
117+
For shape `i` and a location for the top-left corner `(x, y)`, we would put `i` at this location if the variable `v(i, x, y)`
118+
holds true.
119+
As we shall be working with Z3's integers (we will see why later), we will add the following constraints to our list:
120+
- `v(i, x, y) >= 0`
121+
- `v(i, x, y) <= 1`
122+
123+
```scala 3
124+
case class Variable(shape: Shape, ti: Int, tj: Int, variable: Z3AST)
125+
126+
def setupShape(shape: Shape): Seq[Variable] =
127+
val vars = for
128+
s <- shape.allRotationsAndFlips
129+
# every possible top-left corners
130+
ti <- 0 to maxRows - shape.rows
131+
tj <- 0 to maxCols - shape.cols
132+
yield
133+
// create a new variable of type `i`, this is our v(i, x, y)
134+
val v = ctx.mkConst(ctx.mkFreshStringSymbol(), i)
135+
constraints ++= Seq(
136+
ctx.mkGE(v, zero), // v >= 0
137+
ctx.mkLE(v, one) // v <= 1
138+
)
139+
Variable(s, ti, tj, v)
140+
```
141+
142+
That was simple! Either we put the shape, or we don't.
143+
Now, we can easily encode the first requirement: simply require that the _sum_ of all our binary variables for every position
144+
of shape `i` to be equal to `count(i)` itself:
145+
146+
```scala 3
147+
constraints += ctx.mkEq(
148+
ctx.mkAdd(vars*), // sum of all our variables above
149+
requirements(shape)
150+
)
151+
```
152+
153+
Incidentally, since we encoded the fact that we put them at only valid locations, the second requirement is already satisfied!
154+
155+
The last requirement is that every cell is only filled at most once.
156+
To see how we could encode this, let's look at how a certain `v(i, x, y)` affects the filled space.
157+
Let's say we try to fit the 4th shape to location (2, 3):
158+
159+
```
160+
\0123456
161+
0.......
162+
1.......
163+
2...###.
164+
3...#...
165+
4...###.
166+
5.......
167+
```
168+
169+
It affects cells (2,3), (2,4), (2,5), (3,3), (4,3), (4,4) and (4,5). So, if cell `(p, q)` in the shape is filled, then
170+
cell `(x + p, y + q)` would be filled in our space! We would say that `v(4, 2, 3)` would "contribute" to all cells
171+
(2,3), (2,4), (2,5), (3,3), (4,3), (4,4) and (4,5).
172+
173+
Let's try to construct the list of all possible "contributors" for each cell:
174+
```scala 3
175+
// defined globally and mutable ;)
176+
val contributors = Array.fill(maxRows, maxCols)(mutable.ListBuffer[Z3AST]())
177+
```
178+
`Z3AST` is the type of a constraint in Z3: it is a syntax node of the larger constraint expression.
179+
180+
```scala 3
181+
// in the setupShape function, in our vars for expression
182+
for i <- 0 until s.rows
183+
j <- 0 until s.cols
184+
if shape.isFilled(i, j)
185+
do
186+
contributors(ti + i)(tj + j) += v
187+
```
188+
189+
Once all the contributors have been found, we simply require that _at most one_ of the contributors can actually be filled.
190+
In terms of arithmetic, we can require that the _sum_ of the contributors is at most 1, so at most one of the contributors can be one.
191+
```scala 3
192+
constraints ++=
193+
for i <- 0 until maxRows
194+
j <- 0 until maxCols
195+
cs = contributors(i)(j) // contributors to cell (i, j)
196+
if !cs.isEmpty
197+
yield ctx.mkLE( // <=
198+
ctx.mkAdd(cs.toSeq*), // sum of all the contributors
199+
one
200+
)
201+
```
202+
203+
And that's it! We just have to summon the solver, and asks whether it can find a solution.
204+
205+
```scala 3
206+
val solver = ctx.mkSolver()
207+
solver.assertCnstr(
208+
ctx.mkAnd(constraints.toSeq*), // require all our constraints to be true
209+
)
210+
solver.check().get // will fail if Z3 time outs before finding a solution
211+
```
212+
213+
Also, we can ask Z3 to find one specific solution for us:
214+
```scala 3
215+
solver
216+
.checkAndGetAllModels()
217+
.nextOption()
218+
.map: model =>
219+
val toFill =
220+
variables // the Seq of all variables for all shapes
221+
.filter:
222+
case Variable(shape, ti, tj, v) =>
223+
model.evalAs[Int](v) == 1
224+
// we can now draw shapes in toFill down!
225+
```
226+
227+
So, how does this fare?
228+
229+
Well, Z3 can solve the example... (that the trivial code cannot)
230+
231+
But no luck for any tests in the actual input :( So yes, it was fun, but we still created tens of thousands of variables, and solvers still cannot deal with that much yet.
232+
9233
## Solutions from the community
10234
- [Solution](https://github.com/rmarbeck/advent2025/blob/main/day12/src/main/scala/Solution.scala) by [Raphaël Marbeck](https://github.com/rmarbeck)
11235

0 commit comments

Comments
 (0)