Uiua

(added language tag)

Quiet here, isn't it?

Here's part1 to be going on with.

# AOC 2025 Day 10 - Wiring maze
D ← "[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}\n[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2}\n[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5}"
# D      ← &fras"randomAOC/AOC2025day10.txt"
Digits ← ⊜⋕⊸∊+@0⇡10
Parse  ← ⊜(□⊜□⊸≠@\s)⊸≠@\n
Part₁ ← (
  ≡◇(
    =@#↘₁↘₋₁°□°⊂↘¯1  # target
    ⊙⬚0≡◇(°⊚Digits)  # presses
    ⧻⊢path(≡⌞≠|=0/+) # find shortest path
  )
  /+-1
)
Part₁ Parse D

I've given up on Part 2. I knew what I needed to do but didn't have the understanding of how to use the matrix elimination method to get beyond the first stages. But I did find this:

C++

BFS for part 1, "Z3 of shame" for part 2. On the plus side, it's not that goddamned hailstones question from 2023 day 24 again. On the minus side, if I wanted to be reminded how bad I am at maths, then I could head on over to Project Euler and struggle with the questions there.

Z3 is incredibly fast. Well done, Microsoft research.

#include <boost/log/trivial.hpp>
#include <boost/unordered/unordered_flat_map.hpp>
#include <boost/unordered/unordered_flat_set.hpp>
#include <fstream>
#include <sstream>
#include <stdexcept>
#include <vector>
#include <z3++.h>

namespace {

using Button = boost::unordered::unordered_flat_set<size_t>;
using Joltage = std::vector<int>;

struct Machine {
  std::string pattern;
  std::vector<Button> buttons;
  Joltage joltage;
};

using Machines = std::vector<Machine>;
using PatternCount = boost::unordered::unordered_flat_map<std::string, size_t>;

auto parse_button(const std::string &in) {
  auto rval = Button{};
  auto start = size_t{};
  while (start < in.size()) {
    auto comma = in.find(',', start);
    if (comma == std::string::npos)
      comma = in.size();
    rval.insert(std::stoull(in.substr(start, comma - start)));
    start = comma + 1;
  }
  return rval;
}

auto parse_joltage(const std::string &in) {
  auto rval = Joltage{};
  auto start = size_t{};
  while (start < in.size()) {
    auto comma = in.find(',', start);
    if (comma == std::string::npos)
      comma = in.size();
    rval.push_back(std::stoi(in.substr(start, comma - start)));
    start = comma + 1;
  }
  return rval;
}

auto read() {
  auto rval = Machines{};
  auto ih = std::ifstream{"10.txt"};
  if (!ih)
    throw std::runtime_error{"file?"};
  auto line = std::string{};
  while (std::getline(ih, line)) {
    auto m = Machine{};
    auto ss = std::istringstream{line};
    auto str = std::string{};
    ss >> m.pattern;
    m.pattern = m.pattern.substr(1, m.pattern.size() - 2);
    while (ss >> str) {
      if (str.at(0) == '(')
        m.buttons.push_back(parse_button(str.substr(1, str.size() - 2)));
      else
        m.joltage = parse_joltage(str.substr(1, str.size() - 2));
    }
    rval.push_back(std::move(m));
  }
  return rval;
}

auto minimum_presses(const Machine &m) {
  auto presses = size_t{};
  auto pattern = PatternCount{};
  auto first = std::string(m.pattern.size(), '.');
  auto next_iter = std::vector<std::string>{};

  pattern[first] = 0;
  next_iter.push_back(first);

  while (true) {
    auto this_iter = next_iter;
    next_iter.clear();
    ++presses;

    for (auto &iter : this_iter) {
      for (auto &button : m.buttons) {
        auto copy = iter;
        for (auto toggle : button)
          copy[toggle] = copy[toggle] == '.' ? '#' : '.';
        if (copy == m.pattern)
          return presses;
        if (auto f = pattern.find(copy); f != pattern.end())
          continue;
        pattern[copy] = presses;
        next_iter.push_back(std::move(copy));
      }
    }
  }
}

auto part1(const Machines &machines) {
  auto rval = size_t{};
  for (const auto &machine : machines)
    rval += minimum_presses(machine);
  return rval;
}

auto solve(const Machine &m) {
  z3::context context;
  z3::optimize opt(context);

  auto array = std::vector<z3::expr>{};
  auto sum = z3::expr{context.int_val(0)};
  for (auto i = size_t{}; i < m.buttons.size(); ++i) {
    auto name = std::string{"a"};
    name[0] += i;
    auto x = context.int_const(name.c_str());
    opt.add(x >= 0);
    sum = sum + x;
    array.push_back(std::move(x));
  }
  auto z = context.int_const("z");
  opt.add(sum == z);

  for (auto joltage = size_t{}; joltage < m.joltage.size(); ++joltage) {
    auto ex = z3::expr{context.int_val(0)};
    for (auto button = size_t{}; button < m.buttons.size(); ++button) {
      if (m.buttons.at(button).contains(joltage))
        ex = ex + array.at(button);
    }
    opt.add(ex == m.joltage.at(joltage));
  }

  z3::optimize::handle handle = opt.minimize(z);
  opt.check();
  return opt.lower(handle).as_uint64();
}

auto part2(const Machines &machines) {
  auto total = size_t{};
  for (auto &machine : machines)
    total += solve(machine);
  return total;
}

} // namespace

auto main() -> int {
  auto machine = read();
  BOOST_LOG_TRIVIAL(info) << "Day 10: read " << machine.size();
  BOOST_LOG_TRIVIAL(info) << "1: " << part1(machine);
  BOOST_LOG_TRIVIAL(info) << "2: " << part2(machine);
}

In this case, I formulated both questions as a linear algebra question. The first one is over the finite field F2, which I solved by using the library galois and some manual row reduction. The second was over positive integers which is not a field, so I solved it over Q using sympy and then looked for positive integer minimal solutions. In some cases these are under determined, and in some cases exactly solvable systems of the form Ax = b for x where A is the vector made from button switch vectors, b is the light switch pattern vector in the first case or jolts in the second. For under determined ones, your solutions are of the form particular + linear combinations of null space (mod 2 in the first case) so you only search for the minimal one there and in the second you have to search both minimal and positive integer one (because your solution will be over Q and not Z+) in the second case. Wonders of vectorization makes a quick work of these last parts (0.2 second in the first problem about 20s in the second). Also nullspace seems to generally have less than or equal to two dimensions so search space is much smaller than using all the button press vectors.

import itertools as it
from pathlib import Path

import numpy as np
import galois
from sympy import Matrix, symbols, linsolve

cwd = Path(__file__).parent
GF2 = galois.GF(2)

def convert_line(line):

  target = line.split('] ')[0][1:]
  vectors = line.split('] ')[1].split(' ')[:-1]
  jolts = line.split('] ')[1].split(' ')[-1].strip()

  ndims = len(target)

  target = np.array([0 if l=='.' else 1 for l in target], dtype=int)
  jolts = np.array(list(map(int,jolts[1:-1].split(','))))

  M = []

  for v in vectors:
    coords = [int(x) for x in v if x.isnumeric()]
    vec = np.zeros(ndims, dtype=int)
    vec[coords] = 1
    M.append(vec)

  return np.array(M).T,target,jolts


def parse_input(file_path):
  with file_path.open("r") as fp:
    manual = list(map(convert_line, fp.readlines()))

  return manual


def find_pivots(R):
    pivots = []
    m, n = R.shape
    row = 0

    for col in range(n):
      if row < m and R[row, col] == 1:
        pivots.append(col)
        row += 1

    return pivots


def solve_GF2(A, x):

  nullspace = A.null_space()

  M = GF2(np.hstack([np.array(A), np.array(x)[:,None]]))
  R = M.row_reduce()

  pivots = find_pivots(R)

  m, n = R.shape
  n -= 1

  particular = GF2.Zeros(n)

  for r, c in enumerate(pivots):
      particular[c] = R[r, n]

  return np.array(particular), nullspace


def solve_Q(M, x):
  b = symbols(" ".join([f"b{i}" for i in range(M.shape[1])]))
  solution = list(linsolve((M, x), b))[0]
  syms = list(solution.free_symbols)
  func = Matrix(solution)

  particular = np.array(func.subs({s:0 for s in syms}).tolist()).flatten().astype(float)
  nullspace = np.array([np.array(x.tolist()).flatten() for x in M.nullspace()]).astype(float)

  return particular, nullspace


def minimize(nullspace, particular, jolt):

  nvecs = nullspace.shape[0]

  if not jolt:
    coef = np.array(list(it.product(np.arange(0, 2), repeat=nvecs)))
    A = np.sum(np.mod(coef@np.array(nullspace) + particular[None,:],2),axis=-1)
    I = np.argmin(A)
    res = np.mod(coef[I]@np.array(nullspace) + particular[None,:],2)

    return np.sum(res)
  else:
    N = 100
    I = []

    while len(I)==0: # look for a positive integer solution, if does not exist increase N

      coef = np.array(list(it.product(np.arange(-N, N), repeat=nvecs)))
      A = coef@np.array(nullspace) + particular[None,:]
      mask = (A >= 0) & np.isclose(A, A.astype(int))
      I = np.where(mask.all(axis=1))[0]
      N += 500

    return np.min(np.sum(A[I,:],axis=-1))


def solve_problem(file_name, jolt=False):

  manual = parse_input(Path(cwd, file_name))
  sum_press = 0

  for ind,(M, light_target, jolt_target) in enumerate(manual):

    if not jolt:
      #part1 solve over GF2, looks for minimal solution of the form particular + null
      M = GF2(M)
      target = GF2(light_target)
      particular, nullspace = solve_GF2(M, target)

    else:
      #part2 solve over Q, look for minimal integer, positive solution of the form particular + null
      target = Matrix(jolt_target.astype(int))
      M = Matrix(M.astype(int))
      particular, nullspace = solve_Q(M, target)

    sum_press += minimize(nullspace, particular, jolt)

  return sum_press


if __name__ == "__main__":

  assert solve_problem("test_input") == 7
  assert solve_problem("input") == 475
  assert solve_problem("test_input", True) == 33
  assert solve_problem("input", True) == 18273

Rust

Only took four days, but I made it, and without any maths libraries. I tried lots of unsuccessful searches (including A*) before realizing part 2 is a linear equation system. Then I tried to find all solutions by just going row by row, guessing all but one unknown variable and finding the smallest solution, but this was still way too slow due to the high amount of variables guessed.

By looking around on Wikipedia I found that the problem could be simplified by turning the matrix into Smith Normal Form or Hermitian Normal Form, but couldn't find any Rust library implementing these. Their algorithms looked just a bit too complicated to implement myself. Maybe I would have used Python, because sagemath has everything, but the problem of ultimately finding the smallest integer solution still remained, and I already had the search code in Rust without simplifying the matrix.

So put the matrix into echelon form by implementing Gaussian elimination, which wasn't too bad, and it significantly reduced the number of variables to guess. Now part 2 runs in 70ms.

View code on github

Kotlin

Part 1 had me assuming, like a lot of other folks, that Part 2 would be a simple weighted graph. So I coded Part 1 as a non-weighted graph and it was great.

Part 2 looked simple enough, but different. Part 1 was breadth first, I assumed depth first would work for Part 2. When it worked great on the test input, but took 12 seconds, I knew I was in trouble. So I added caching. And it was super quick on the test input.

Real input was a whole 'nother story. I watched my system resources balloon. At last count it was using 8GB of RAM before I killed it. And that was before solving even the first line.

So I went online to find what I'm missing to see people saying it's a linear algebra problem, and that it's best to use some kind of library for it.

I will admit that I leaned pretty heavily on asking Gemini questions to figure out how to use the Google OR-Tools library.

So here's my Part 2 code:

import com.google.ortools.Loader
import com.google.ortools.linearsolver.MPSolver
import com.google.ortools.linearsolver.MPVariable
import utils.*

fun main() {
    val input = getInput(10)
    val machines = parseInput1(input)
    Loader.loadNativeLibraries()
    var total = 0
    for (machine in machines) {
        val buttons = machine.buttons
        val joltages = machine.joltages
        val solver = MPSolver.createSolver("SCIP") ?: throw Exception("Could not create solver")
        val x = arrayOfNulls<MPVariable>(machine.buttons.size)
        for (i in buttons.indices) {
            x[i] = solver.makeIntVar(0.0, Double.POSITIVE_INFINITY, "x$i")
        }
        val target = joltages.map { it.toDouble() }
        val aMatrix = joltages.indices.map { joltageToArray(it, buttons) }.toTypedArray()
        for (j in joltages.indices) {
            val ct = solver.makeConstraint(target[j], target[j], "joltage_constraint_$j")
            for (i in buttons.indices) {
                ct.setCoefficient(x[i], aMatrix[j][i])
            }
        }
        val objective = solver.objective()
        for (i in buttons.indices) {
            objective.setCoefficient(x[i], 1.0)
        }
        objective.setMinimization()
        val resultStatus = solver.solve()
        if (resultStatus == MPSolver.ResultStatus.OPTIMAL) {
            val result = objective.value().toInt()
            total += result
        } else {
            println("Problem could not be solved.")
        }
    }
    println(total)
}

data class Machine(val configuration: List<Boolean>, val buttons: List<List<Int>>, val joltages: List<Int>)

fun parseInput1(input: String): List<Machine> {
    return input.lines()
        .filter { it.isNotBlank() }
        .map {
            val split = it.split(" ")
            val configuration = split.first().toCharArray()
                .slice(1..<split.first().length - 1)
                .map { char ->
                    when (char) {
                        '#' -> true
                        else -> false
                    }
                }
            val buttons = split.slice(1..<split.size - 1)
                .map { str ->
                    str.slice(1..<str.length - 1)
                        .split(",")
                        .map { number -> number.toInt() }
                }
            val joltages = split.last()
                .slice(1..<split.last().length - 1)
                .split(",")
                .map { number -> number.toInt() }
            Machine(configuration, buttons, joltages)
        }
}

fun joltageToArray(joltageIndex: Int, buttons: List<List<Int>>): Array<Double> {
    val array = DoubleArray(buttons.size) { 0.0 }.toTypedArray()
    for (i in buttons.indices) {
        if (joltageIndex in buttons[i]) {
            array[i] = 1.0
        }
    }
    return array
}

Rust

Finally got it, but had to use Z3. Getting Z3 to work was a real pain, they really need to doco the rust crate better.

I'll try redo it at some point without Z3, maybe after I forgot what a pain this was.

    struct Puzzle2 {
        target: Vec<u16>,
        buttons: Vec<Vec<u16>>,
    }
    fn solve_puzzle_z3(puzzle2: &Puzzle2) -> usize {
        let optimiser = Optimize::new();
        let num_presses: Vec<Int> = (0..puzzle2.buttons.len())
            .map(|i| Int::new_const(format!("n_{i}")))
            .collect();

        num_presses.iter().for_each(|p| optimiser.assert(&p.ge(0)));

        (0..puzzle2.target.len()).for_each(|i| {
            let r = puzzle2.target[i];

            let buttons = puzzle2
                .buttons
                .iter()
                .enumerate()
                .filter_map(|(j, b)| {
                    if b.contains(&(i as u16)) {
                        Some(&num_presses[j])
                    } else {
                        None
                    }
                })
                .collect::<Vec<&Int>>();

            let sum = buttons.into_iter().sum::<Int>();

            optimiser.assert(&sum.eq(r));
        });

        let all_presses = num_presses.iter().sum::<Int>();

        optimiser.minimize(&all_presses);
        if optimiser.check(&[]) != SatResult::Sat {panic!("Unsolvable")}
        let model = optimiser
                    .get_model()
                    .expect("Optimizer should have a model if sat");
        let t = model.eval(&all_presses, true).unwrap().as_i64().unwrap();
        t as usize
    }

    #[test]
    fn test_y2025_day10_part2() {
        let input = include_str!("../../input/2025/day_10.txt");
        let puzzles = input
            .lines()
            .map(|line| {
                let parts = line.split(" ").collect::<Vec<_>>();
                let display = parts.last().unwrap();
                let display = display[1..display.len() - 1]
                    .split(',')
                    .map(|c| c.parse::<u16>().unwrap())
                    .collect::<Vec<u16>>();

                let buttons = parts[1..parts.len() - 1]
                    .iter()
                    .map(|s| {
                        s[1..s.len() - 1]
                            .split(",")
                            .map(|s| s.parse::<u16>().unwrap())
                            .collect::<Vec<u16>>()
                    })
                    .collect::<Vec<Vec<u16>>>();

                Puzzle2 {
                    target: display,
                    buttons,
                }
            })
            .collect::<Vec<Puzzle2>>();

        let mut min_presses = 0;

        for puzzle in &puzzles {
            min_presses += solve_puzzle_z3(puzzle)
        }

        println!("PRESSED: {}", min_presses);
    }