Scala3, Sympy

case class Particle(x: Long, y: Long, z: Long, dx: Long, dy: Long, dz: Long)

def parseParticle(a: String): Option[Particle] = a match
    case s"$x, $y, $z @ $dx, $dy, $dz" => Some(Particle(x.toLong, y.toLong, z.toLong, dx.trim.toLong, dy.trim.toLong, dz.trim.toLong))
    case _ => None

def intersect(min: Double, max: Double)(p: Particle, q: Particle): Boolean =
    val n = p.dx * q.y - p.y * p.dx - q.x * p.dy + p.x * p.dy
    val d = p.dy * q.dx - p.dx * q.dy

    if(d == 0) then false else 
        val k = n.toDouble/d
        val k2 = (q.y + k * q.dy - p.y)/p.dy
        val ix = q.x + k * q.dx
        val iy = q.y + k * q.dy
        k2 >= 0 && k >= 0 && min <= ix && ix <= max && min <= iy && iy <= max

def task1(a: List[String]): Long = 
    val particles = a.flatMap(parseParticle)
    particles.combinations(2).count(l => intersect(2e14, 4e14)(l(0), l(1)))

import re as re2
from sympy import *

p, v, times, eqs = symbols('x y z'), symbols('dx dy dz'), [], []

def parse_eq(i: int, s: str):
    parts = [int(p) for p in re2.split(r'[,\s@]+', s) if p.strip() != '']
    time = Symbol(f't{i}')
    times.append(time)
    for rp, rv, hp, hv in zip(p, v, parts[:3], parts[3:]):
        eqs.append(Eq(rp + time * rv, hp + time * hv))

# need 3 equations for result, everything after that just slows things down
neq = 3
with open('task1.txt', 'r') as fobj:
    for i, s in zip(range(neq), fobj.readlines()):
        parse_eq(i, s)

for sol in solve(eqs, list(p) + list(v) + times):
    x, y, z, *_ = sol
    print(x + y + z)

Rust

github: https://github.com/Treeniks/advent-of-code/blob/master/2023/day24/rust/src/main.rs

codeberg: https://codeberg.org/Treeniks/advent-of-code/src/branch/master/2023/day24/rust/src/main.rs

gitlab: https://gitlab.com/Treeniks/advent-of-code/-/blob/master/2023/day24/rust/src/main.rs

Had to look on reddit for how to solve part 2. Wasn't happy with the idea of using something like Z3, so I ended up brute force guessing the velocity, solving for the position and time and seeing if those are correct.

Lots of unintelligible calculations for solving the equation systems in the code that I just prepared on paper and transferred over.

Python

import numpy as np
import z3

from aoc23.util import assert_full_match
from .solver import Solver

class Day24(Solver):

  def __init__(self):
    super().__init__(24)
    self.test_area = [200000000000000, 400000000000000]
  
  def presolve(self, input: str):
    self.stones = []
    for line in input.splitlines():
      (x, y, z, vx, vy, vz) = assert_full_match(
        r'([0-9-]+), +([0-9-]+), +([0-9-]+) +@ +([0-9-]+), +([0-9-]+), +([0-9-]+)', line).groups()
      self.stones.append((int(x), int(y), int(z), int(vx), int(vy), int(vz)))

  def solve_first_star(self) -> int | str:
    count = 0
    for i, stone_a in enumerate(self.stones):
      for stone_b in self.stones[i+1:]:
        matrix = np.array([[stone_a[3], -stone_b[3]],
                          [stone_a[4], -stone_b[4]],])
        rhs = np.array([[stone_b[0] - stone_a[0]], [stone_b[1] - stone_a[1]]])
        try:
          x = np.linalg.solve(matrix, rhs)
          if not (x > 0).all():
            continue
          intersection_x = stone_a[0] + stone_a[3] * x[0, 0]
          intersection_y = stone_a[1] + stone_a[4] * x[0, 0]
          if (self.test_area[0] <= intersection_x <= self.test_area[1]
              and self.test_area[0] <= intersection_y <= self.test_area[1]):
            count += 1
        except np.linalg.LinAlgError:
          continue
    return count

  def solve_second_star(self) -> int | str:
    x0 = z3.Int('x0')
    y0 = z3.Int('y0')
    z0 = z3.Int('z0')
    vx0 = z3.Int('vx0')
    vy0 = z3.Int('vy0')
    vz0 = z3.Int('vz0')
    t1 = z3.Int('t1')
    t2 = z3.Int('t2')
    t3 = z3.Int('t3')
    solver = z3.Solver()
    solver.add(x0 + vx0 * t1 == self.stones[0][0] + self.stones[0][3] * t1)
    solver.add(y0 + vy0 * t1 == self.stones[0][1] + self.stones[0][4] * t1)
    solver.add(z0 + vz0 * t1 == self.stones[0][2] + self.stones[0][5] * t1)
    solver.add(x0 + vx0 * t2 == self.stones[1][0] + self.stones[1][3] * t2)
    solver.add(y0 + vy0 * t2 == self.stones[1][1] + self.stones[1][4] * t2)
    solver.add(z0 + vz0 * t2 == self.stones[1][2] + self.stones[1][5] * t2)
    solver.add(x0 + vx0 * t3 == self.stones[2][0] + self.stones[2][3] * t3)
    solver.add(y0 + vy0 * t3 == self.stones[2][1] + self.stones[2][4] * t3)
    solver.add(z0 + vz0 * t3 == self.stones[2][2] + self.stones[2][5] * t3)
    assert solver.check() == z3.sat
    model = solver.model()
    return sum([model[x0].as_long(), model[y0].as_long(), model[z0].as_long()])