Advent of Code 2025 - Day 10

I didn’t find any way to solve it with a BFS or some smart DFS, BUT: for those who balk at implementing a equations solver (like me, I was not in the mood today), it is solvable with a genetic programming / iterative reparation approach, the hard part being to get enough guaranties that the solution is the actual minimum.

It is pretty random, and maybe not very elegant, but at least it did the job with my input (and took a lot more time to run than an equation solver would ).

Thats been a tough one.
I used glpsol now. Took one second to run it for some reason:

defmodule Day10.Glpk do
@glpsol “glpsol”

buttons :: [[int]]  (indices der Counters pro Button)

jolts   :: [int]    (Targets)

def solve_machine(buttons, jolts) do
lp = build_lp(buttons, jolts)

tmp_dir = System.tmp_dir!()
id = :erlang.unique_integer([:positive]) |> Integer.to_string()
lp_path = Path.join(tmp_dir, "day10_#{id}.lp")

File.write!(lp_path, lp)

{output, exit_code} =
  System.cmd(@glpsol, ["--lp", lp_path], stderr_to_stdout: true)

File.rm(lp_path)

if exit_code != 0 do
  raise "glpsol failed (exit #{exit_code}):\n#{output}"
end

parse_objective(output)

end

defp build_lp(buttons, jolts) do
k = length(buttons)
m = length(jolts)

var_names = for j <- 0..(k - 1), do: "x#{j}"

objective = """
Minimize
  z: #{Enum.join(var_names, " + ")}
"""

constraints =
  [
    "Subject To"
    | Enum.map(0..(m - 1), fn i ->
        lhs_terms =
          buttons
          |> Enum.with_index()
          |> Enum.reduce([], fn {btn_indices, j}, acc ->
            if i in btn_indices do
              ["x#{j}" | acc]
            else
              acc
            end
          end)
          |> Enum.reverse()

        lhs =
          case lhs_terms do
            [] -> "0"
            _ -> Enum.join(lhs_terms, " + ")
          end

        "  c#{i}: #{lhs} = #{Enum.at(jolts, i)}"
      end)
  ]
  |> Enum.join("\n")

bounds =
  [
    "",
    "Bounds"
    | Enum.map(var_names, fn name ->
        "  #{name} >= 0"
      end)
  ]
  |> Enum.join("\n")

generals = """

Generals
  #{Enum.join(var_names, " ")}

End
"""

[objective, constraints, bounds, generals]
|> Enum.join("\n")

end

“Objective:  z =  33 (MINimum)”

defp parse_objective(output) do
with nil ← match_objective_line(output),
nil ← match_mip_line(output),
nil ← match_objective_value_line(output) do
raise “Could not parse objective value from glpsol output:\n#{output}”
else
value when is_integer(value) → value
end
end

Objective:  z =  33 (MINimum)

defp match_objective_line(output) do
case Regex.run(~r/Objective:\s+\w+\s*=\s*([-0-9.eE+]+)/, output,
capture: :all_but_first
) do
[num_str] → parse_number(num_str)
_ → nil
end
end

+     1: mip =   1.100000000e+01 >=   …

defp match_mip_line(output) do
case Regex.run(~r/mip\s*=\s*([-0-9.eE+]+)/, output,
capture: :all_but_first
) do
[num_str] → parse_number(num_str)
_ → nil
end
end

Objective value =   5.900000000e+01

defp match_objective_value_line(output) do
case Regex.run(~r/Objective value\s*=\s*([-0-9.eE+]+)/, output,
capture: :all_but_first
) do
[num_str] → parse_number(num_str)
_ → nil
end
end

defp parse_number(str) do
case Integer.parse(str) do
{i, “”} → 
i

_ ->
  case Float.parse(str) do
    {f, _} -> round(f)
    _ -> nil
  end

end
end

end

In solver function like this:

  def solve_part2(input) do
    input
    |> parse()
    |> Task.async_stream(
      fn %{button_indices: buttons, jolts: jolts} ->
        Day10.Glpk.solve_machine(buttons, jolts)
      end,
      max_concurrency: System.schedulers_online(),
      timeout: :infinity
    )
    |> Enum.reduce(0, fn
      {:ok, presses}, acc -> acc + presses
      {:exit, reason}, _ -> raise "GLPK failed: #{inspect(reason)}"
    end)
  end

I tried all sorts of things to speed up my native approach to two, including parallelizing it, but alas it’s too large for this approach.

Thanks for the hint on simul equations. Maybe I’ll circle back to see if I can do that before I cheat further and look at your code.

P1 was simple thanks to few observations, but P2 was pain (and there were some issues with Dantzig library that I needed to provide workarounds.

Parse

defmodule Decoder do
  def decode("[" <> pattern), do: do_lights(String.reverse(String.trim_trailing(pattern, "]")), 0)

  def decode("(" <> rest) do
    <<seq::binary-size(byte_size(rest) - 1), ")">> = rest

    seq
    |> String.split(",")
    |> Enum.map(&String.to_integer/1)
  end

  def decode("{" <> rest) do
    <<seq::binary-size(byte_size(rest) - 1), "}">> = rest

    seq
    |> String.split(",")
    |> Enum.map(&String.to_integer/1)
  end
  
  defp do_lights("", num), do: num
  defp do_lights("." <> rest, num), do: do_lights(rest, 2 * num)
  defp do_lights("#" <> rest, num), do: do_lights(rest, 2 * num + 1)
end

indicators =
  puzzle_input
  |> String.split("\n", trim: true)
  |> Enum.map(fn raw ->
    [lights | rest] =
      raw
      |> String.split()
      |> Enum.map(&Decoder.decode/1)

    {buttons, [whatever]} = Enum.split(rest, -1)

    {lights, buttons, whatever}
  end)

Part 1

defmodule Comb do
  def all_possible([]), do: [[]]
  def all_possible([a | rest]) do
    sub = all_possible(rest)

    sub ++ Enum.map(sub, &[a | &1])
  end
end

indicators
|> Enum.sum_by(fn {p, a, _} ->
  a
  |> Enum.map(&Enum.sum_by(&1, fn p -> 2 ** p end))
  |> Comb.all_possible()
  |> Enum.sort_by(&length/1)
  |> Enum.find(fn seq ->
    r = Enum.reduce(seq, 0, &Bitwise.bxor/2)

    p == r
  end)
  |> length()
end)

Part 2

# Here is implementation of Dantzig.HiGHSv1 implementation that adds support for externally provided executable and support for integers

defmodule Joltage do
  alias Dantzig.Polynomial
  alias Dantzig.Constraint
  alias Dantzig.Problem

  def solve({_pat, buttons, goal}) do
    p = Problem.new(direction: :minimize)

    {vars, {p, map}} =
      buttons
      |> Enum.with_index()
      |> Enum.map_reduce({p, %{}}, fn {list, idx}, {p, acc} ->
        {p, var} = Problem.new_variable(p, "v#{idx}", min: 0, type: :integer)

        acc =
          Enum.reduce(list, acc, fn key, map ->
            Map.update(map, key, [var], &[var | &1])
          end)

        {var, {p, acc}}
      end)

    p =
      map
      |> Enum.sort()
      |> Enum.map(&elem(&1, 1))
      |> Enum.zip(goal)
      |> Enum.reduce(p, fn {vars, target}, p ->
        poly = Polynomial.sum(vars)
        const = Constraint.new(poly, :==, target)

        Problem.add_constraint(p, const)
      end)

    p = Problem.increment_objective(p, Polynomial.sum(vars))

    {:ok, s} = Dantzig.HiGHSv1.solve(p)

    Enum.sum_by(vars, &Dantzig.Solution.evaluate(s, &1))
  end
end

indicators
|> Task.async_stream(&Joltage.solve/1, ordered: false)
|> Enum.sum_by(&elem(&1, 1))
|> trunc()

I finally abandonned my heuristic/cache/sorting/pruning semi-brute force approach, couldn not make it work.

I did not know about z3, which seems that everyones uses on the subreddit, so here it goes

defmodule AdventOfCode.Solutions.Y25.Day10 do
  alias AoC.Input

  def parse(input, _part) do
    input
    |> Input.stream!(trim: true)
    |> Enum.map(&parse_line/1)
  end

  defp parse_line(line) do
    "[" <> rest = line
    [lights, " (" <> rest] = String.split(rest, "]")

    lights =
      lights
      |> String.to_charlist()
      |> :lists.reverse()
      |> Enum.map(fn
        ?. -> 0
        ?# -> 1
      end)

    [prev, jolts] = String.split(rest, ") {")
    buttons = String.split(prev, ") (")

    buttons =
      Enum.map(buttons, fn str ->
        str |> String.split(",") |> Enum.map(&String.to_integer/1)
      end)

    jolts =
      jolts
      |> String.trim_trailing("}")
      |> String.split(",")
      |> Enum.map(&String.to_integer/1)

    {lights, buttons, jolts}
  end

  def part_one(machines) do
    machines
    |> Enum.map(fn {lights, buttons, _} ->
      lights = Integer.undigits(lights, 2)
      buttons = Enum.map(buttons, &button_to_int/1)
      {lights, buttons}
    end)
    |> Enum.sum_by(&best_combination/1)
  end

  defp button_to_int(indexes) do
    Enum.reduce(indexes, 0, &(2 ** &1 + &2))
  end

  defp best_combination(machine) do
    {lights, buttons} = machine

    stream_buttons(buttons)
    |> Enum.find_value(fn pressed_buttons ->
      if lights == Enum.reduce(pressed_buttons, 0, &Bitwise.bxor(&1, &2)) do
        length(pressed_buttons)
      else
        nil
      end
    end)
  end

  defp stream_buttons(buttons) do
    n_presses = Stream.iterate(1, &(&1 + 1))

    Stream.flat_map(n_presses, fn n ->
      stream_buttons(n, buttons)
    end)
  end

  # TODO we are repeating: [0, 1] and [1, 0] should be the same XOR result, we
  # should just iterate on digits, right ? But we still need to return [0, 0]
  # somehow

  defp stream_buttons(1, buttons) do
    Enum.map(buttons, &[&1])
  end

  defp stream_buttons(n, buttons) when n > 0 do
    stream_buttons(n - 1, buttons)
    |> Stream.flat_map(fn [top | _] = pressed_buttons ->
      # Basic iteration
      # Stream.map(buttons, fn btn -> [btn | pressed_buttons] end)

      # Only try each combination once
      Stream.flat_map(buttons, fn
        btn when btn >= top -> [[btn | pressed_buttons]]
        _ -> []
      end)
    end)
  end

  def part_two(machines) do
    machines
    |> Task.async_stream(&solve_machine/1, max_concurrency: 200, ordered: false)
    |> Enum.sum_by(&elem(&1, 1))
  end

  defp solve_machine(machine) do
    {_, buttons, target} = machine

    args = Enum.take([:a, :b, :c, :d, :e, :f, :g, :h, :i, :j, :k, :l, :m], length(buttons))

    counter_dependencies =
      target
      |> Enum.with_index()
      |> Enum.map(fn {_, counter_index} ->
        buttons
        |> Enum.zip(args)
        |> Enum.filter(fn {button, _arg} ->
          counter_index in button
        end)
        |> Enum.map(fn {_button, arg} -> arg end)
      end)

    smt2 =
      [
        Enum.map(args, fn arg -> "(declare-const #{arg} Int)" end),
        Enum.map(args, fn arg -> "(assert (>= #{arg} 0))" end),
        Enum.zip_with(target, counter_dependencies, fn t, deps ->
          "(assert (= #{t} (+#{Enum.map(deps, &" #{&1}")})))"
        end),
        """
        (define-fun sum () Int (+#{Enum.map(args, &" #{&1}")}))
        (minimize sum)
        (check-sat)
        (get-value (sum))
        """
      ]

    z3 = System.find_executable("z3")
    port = Port.open({:spawn_executable, z3}, [:binary, args: ["-in"]])
    send(port, {self(), {:command, smt2}})

    int = receive_result(port)
    true = Port.close(port)
    int
  end

  defp receive_result(port) do
    receive do
      {^port, {:data, "sat\n"}} -> receive_result(port)
      {^port, {:data, "((sum " <> result}} -> parse_result(result)
      {^port, {:data, "sat\n((sum " <> result}} -> parse_result(result)
    end
  end

  defp parse_result(result) do
    {int, "))" <> _} = Integer.parse(result)
    int
  end
end

Also maybe @mudasobwa could you tell me how to use z3 with erlang modules. I’ve seen that Cures uses z3 but is there an API for it? I found the same kind of string that we would input to z3 stdin.

Yeah there’s some PRs open to fix both of those issues, so I used that branch from GitHub

Has anybody seen any solution that doesn’t use a solver library? I’ve got to think there is something about the simplicity, 1 and 0 coefficients, of these linear equations that could be taken advantage of.

I found two, one claimed 35minutes runtime, the other one 20 (python)

If anyone is still interested in thinking about this, here is a thought I have. This is my set of simultaneous equations for the first machine of the sample data. The format is a tuple of the coefficients list and result of each equation.

Equations: [
  {[1, 1, 0, 0, 0, 0], 3},
  {[1, 0, 0, 0, 1, 0], 5},
  {[0, 0, 1, 0, 1, 1], 7},
  {[0, 1, 1, 1, 0, 0], 4}
]

The first equation tells us the [b0,b1] pair must be one of these combination: [0,3],[1,2],[2,1],[3,0].

Those combinations will then combine in the next equation to give a set of possible values for b4. For example [3,0] only allows b4 to be 0,1, or 2

Then those combinations will combine in the 3rd equation to add in the combinations of b2 and b5

And then finally add all the combinatorics for the 4th equation.

Also, along the way we’re going to find empty set combinations, i.e. no possible solutions, which means that we can eliminate previous combinations as we go.

It feels like I should sort the equations to minimize the number of new combinations I need to build up in the next step.

Granted this is the simplest machine. But, if you follow this thinking, and did it for one of the “real” problems, would it blow up into the stratosphere? Or would that incremental removal of unsolvable combinations whittle it down as you go into a set of combinations that could actually be evaluated?