From 306d1dd203f26780e9abd77c313bd993959b4eaf Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Fri, 12 Dec 2025 20:01:34 +0100 Subject: [PATCH 1/3] Something about day 12 --- docs/2025/puzzles/day12.md | 222 +++++++++++++++++++++++++++++++++++++ 1 file changed, 222 insertions(+) diff --git a/docs/2025/puzzles/day12.md b/docs/2025/puzzles/day12.md index f6c2c51aa..6c4fed169 100644 --- a/docs/2025/puzzles/day12.md +++ b/docs/2025/puzzles/day12.md @@ -6,6 +6,228 @@ import Solver from "../../../../../website/src/components/Solver.js" https://adventofcode.com/2025/day/12 +## Inspecting the input + +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. +The number of shapes of each kind is given. + +This is eerily reminiscent of the [Bin Packing problem](https://en.wikipedia.org/wiki/Bin_packing_problem), therefore we should +expect to figure out some patterns in the input, as the general problem is likely to be untractable. + +We are given the following 6 shapes: + +``` +0: +### +##. +##. + +1: +### +##. +.## + +2: +.## +### +##. + +3: +##. +### +##. + +4: +### +#.. +### + +5: +### +.#. +### +``` +Note that they can be rotated and flipped, so the total number of shapes is actually about 72. + +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!). + +However, we can weed out some special cases: +- 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: + ```scala 3 + def triviallyPossible(maxRows: Int, maxCols: Int, requirements: Map[Shape, Int]) = + val totalCount = requirements.values.sum // total number of required shapes + (maxRows / 3) * (maxCols / 3) >= totalCount + ``` +- 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: + ```scala 3 + case class Shape(cells: Array[Array[Char]]): + def cellCount = + cells + .iterator + .map(row => row.count(_ == '#')) + .sum + + def triviallyImpossible(maxRows: Int, maxCols: Int, requirements: Map[Shape, Int]) = + val totalCellCount = + requirements + .iterator + .map((shape, count) => shape.cellCount * count) + .sum + maxRows * maxCols < totalCellCount + ``` + +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! + +## Bonus: Can Z3 solve it? + +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). +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? + +To use Z3 from Scala, I opted for the [ScalaZ3](https://github.com/epfl-lara/ScalaZ3) wrapper made by EPFL's LARA lab. +Unfortunately the library seems to not be able on Maven, so I compiled it myself and manually include it as an unmanaged JAR. +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: + +```scala +//> using jar ./scalaz3_3-4.8.14.jar +``` + +In the code, we can set up a Z3 context as follows, preparing to build our constraints. + +```scala 3 +import z3.scala.* +val ctx = new Z3Context("MODEL" -> true) // this allows us to receive a specific solution later on +val i = ctx.mkIntSort() // declare an int-like type in the SMT context +// some constants that we shall mention later +val zero = ctx.mkInt(0, i) +val one = ctx.mkInt(1, i) + +// as we will build up the complex constraints one-by-one, mutable collections make them easier to work with +val constraints = mutable.ListBuffer[Z3AST]() +``` + +Now, how do we encode our problem as a bunch of arithmetic inequalities? From a glance, here are the requirements that we have +to encode: +- For shape `i`, we have to use `count(i)` amount of shapes. +- The shapes should be laid on a `N x M` space. +- Layered shapes should not overlap. + +A simple way to encode the _choice_ of putting a shape at a specific position, is to turn them into a *binary variable*. +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)` +holds true. +As we shall be working with Z3's integers (we will see why later), we will add the following constraints to our list: +- `v(i, x, y) >= 0` +- `v(i, x, y) <= 1` + +```scala 3 +case class Variable(shape: Shape, ti: Int, tj: Int, variable: Z3AST) + +def setupShape(shape: Shape): Seq[Variable] = + val vars = for + s <- shape.allRotationsAndFlips + # every possible top-left corners + ti <- 0 to maxRows - shape.rows + tj <- 0 to maxCols - shape.cols + yield + // create a new variable of type `i`, this is our v(i, x, y) + val v = ctx.mkConst(ctx.mkFreshStringSymbol(), i) + constraints ++= Seq( + ctx.mkGE(v, zero), // v >= 0 + ctx.mkLE(v, one) // v <= 1 + ) + Variable(s, ti, tj, v) +``` + +That was simple! Either we put the shape, or we don't. +Now, we can easily encode the first requirement: simply require that the _sum_ of all our binary variables for every position +of shape `i` to be equal to `count(i)` itself: + +```scala 3 + constraints += ctx.mkEq( + ctx.mkAdd(vars*), // sum of all our variables above + requirements(shape) + ) +``` + +Incidentally, since we encoded the fact that we put them at only valid locations, the second requirement is already satisfied! + +The last requirement is that every cell is only filled at most once. +To see how we could encode this, let's look at how a certain `v(i, x, y)` affects the filled space. +Let's say we try to fit the 4th shape to location (2, 3): + +``` +\0123456 +0....... +1....... +2...###. +3...#... +4...###. +5....... +``` + +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 +cell `(x + p, y + q)` would be filled in our space! We would say that `v(4, 2, 3)` would "contribute" to all cells +(2,3), (2,4), (2,5), (3,3), (4,3), (4,4) and (4,5). + +Let's try to construct the list of all possible "contributors" for each cell: +```scala 3 +// defined globally and mutable ;) +val contributors = Array.fill(maxRows, maxCols)(mutable.ListBuffer[Z3AST]()) +``` +`Z3AST` is the type of a constraint in Z3: it is a syntax node of the larger constraint expression. + +```scala 3 + // in the setupShape function, in our vars for expression + for i <- 0 until s.rows + j <- 0 until s.cols + if shape.isFilled(i, j) + do + contributors(ti + i)(tj + j) += v +``` + +Once all the contributors have been found, we simply require that _at most one_ of the contributors can actually be filled. +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. +```scala 3 +constraints ++= + for i <- 0 until maxRows + j <- 0 until maxCols + cs = contributors(i)(j) // contributors to cell (i, j) + if !cs.isEmpty + yield ctx.mkLE( // <= + ctx.mkAdd(cs.toSeq*), // sum of all the contributors + one + ) +``` + +And that's it! We just have to summon the solver, and asks whether it can find a solution. + +```scala 3 +val solver = ctx.mkSolver() +solver.assertCnstr( + ctx.mkAnd(constraints.toSeq*), // require all our constraints to be true +) +solver.check().get // will fail if Z3 time outs before finding a solution +``` + +Also, we can ask Z3 to find one specific solution for us: +```scala 3 +solver + .checkAndGetAllModels() + .nextOption() + .map: model => + val toFill = + variables // the Seq of all variables for all shapes + .filter: + case Variable(shape, ti, tj, v) => + model.evalAs[Int](v) == 1 + // we can now draw shapes in toFill down! +``` + +So, how does this fair? + +Well, Z3 can solve the example... (that the trivial code cannot) + +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. + ## Solutions from the community - [Solution](https://github.com/rmarbeck/advent2025/blob/main/day12/src/main/scala/Solution.scala) by [Raphaël Marbeck](https://github.com/rmarbeck) From 4014893521917a9311a11fe8879c8d215b1303e7 Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Fri, 12 Dec 2025 20:04:07 +0100 Subject: [PATCH 2/3] Add my name --- docs/2025/puzzles/day12.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/2025/puzzles/day12.md b/docs/2025/puzzles/day12.md index 6c4fed169..894866f86 100644 --- a/docs/2025/puzzles/day12.md +++ b/docs/2025/puzzles/day12.md @@ -2,6 +2,8 @@ import Solver from "../../../../../website/src/components/Solver.js" # Day 12: Christmas Tree Farm +by [@natsukagami](https://github.com/natsukagami) + ## Puzzle description https://adventofcode.com/2025/day/12 From 086d0c2c259680f86008b9e51fc40e76d1f691ce Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Mon, 15 Dec 2025 12:59:47 +0100 Subject: [PATCH 3/3] Typo Co-authored-by: Merlin Hughes --- docs/2025/puzzles/day12.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/2025/puzzles/day12.md b/docs/2025/puzzles/day12.md index 894866f86..5179a5ebe 100644 --- a/docs/2025/puzzles/day12.md +++ b/docs/2025/puzzles/day12.md @@ -224,7 +224,7 @@ solver // we can now draw shapes in toFill down! ``` -So, how does this fair? +So, how does this fare? Well, Z3 can solve the example... (that the trivial code cannot)