2 files changed, 259 insertions, 0 deletions
diff --git a/aoc2023-other/day-24/day-24.ipynb b/aoc2023-other/day-24/day-24.ipynb
new file mode 100644
index 0000000..0167bf7
--- /dev/null
+++ b/aoc2023-other/day-24/day-24.ipynb
@@ -0,0 +1,216 @@
+{
+ "cells": [
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import z3"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We don't need to solve for all of the trajectory intersections at once; picking just a handful will do.  \n",
+    "\n",
+    "There are initially six unknowns (the three components each of $\\overrightarrow{x_{rock}}$ and $\\overrightarrow{v_{rock}}$), and each additional equation adds three equations of the form $x_{i\\cdot rock} + v_{i \\cdot rock} t_n = x_{i\\cdot hail\\cdot n} + v_{i \\cdot hail\\cdot n} t_n$, which also contains one new unknown, the time of intersection $t_n$.\n",
+    "\n",
+    "| Hail | Equations | Unknowns |\n",
+    "| ---- | ----------- | ----------- |\n",
+    "| 1 | 3 | 7 |\n",
+    "| 2 | 6 | 8 |\n",
+    "| 3 | 9 | 9 |\n",
+    "\n",
+    "We just need 3 hail trajectories.  The first three in the set are enough."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "[[156689809620606, 243565579389165, 455137247320393, -26, 48, -140],\n",
+       " [106355761063908, 459832650718033, 351953299411025, 73, -206, -52],\n",
+       " [271915251832336, 487490927073225, 398003502953444, 31, -414, -304]]"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "hail = [[int(i) for i in l.replace('@',',').split(',')]\n",
+    "                for l in open('input')]\n",
+    "\n",
+    "hail_sample = hail[0:3]\n",
+    "\n",
+    "hail_position = [h[0:3] for h in hail_sample]\n",
+    "hail_velocity = [h[3:] for h in hail_sample]\n",
+    "\n",
+    "hail_sample"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "start_position = z3.RealVector('p', 3)\n",
+    "start_velocity = z3.RealVector('v', 3)\n",
+    "hit_time = z3.RealVector('t', 3)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "For each of the hailstone trajectories in the sample, the thrown rock's coordinates will be equal to the hailstone's coordinates at a given time $t$: $x_{i\\cdot rock} + v_{i \\cdot rock} t = x_{i\\cdot hail} + v_{i \\cdot hail} t$ for $i \\in \\{x,\\,y,\\,z\\}$."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "solver = z3.Solver()\n",
+    "solver.add(*[start_position[i] + start_velocity[i] * t == hp[i] + hv[i] * t\n",
+    "             for t, hp, hv in zip(hit_time, hail_position, hail_velocity) for i in range(3)])"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Is the solver satisfied?  That is, do none of the constraints conflict with each other?"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "<b>sat</b>"
+      ],
+      "text/plain": [
+       "sat"
+      ]
+     },
+     "execution_count": 5,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "solver.check()"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "The solver model returns the state that satisfies all the constraints:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "[t<sub>2</sub> = 474506740599,\n",
+       " t<sub>0</sub> = 931974028142,\n",
+       " v<sub>0</sub> = -337,\n",
+       " t<sub>1</sub> = 829702369046,\n",
+       " v<sub>1</sub> = -6,\n",
+       " v<sub>2</sub> = 155,\n",
+       " p<sub>0</sub> = 446533732372768,\n",
+       " p<sub>2</sub> = 180204909018503,\n",
+       " p<sub>1</sub> = 293892176908833]"
+      ],
+      "text/plain": [
+       "[t__2 = 474506740599,\n",
+       " t__0 = 931974028142,\n",
+       " v__0 = -337,\n",
+       " t__1 = 829702369046,\n",
+       " v__1 = -6,\n",
+       " v__2 = 155,\n",
+       " p__0 = 446533732372768,\n",
+       " p__2 = 180204909018503,\n",
+       " p__1 = 293892176908833]"
+      ]
+     },
+     "execution_count": 6,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "solver.model()"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "and all that's left to do is extract the results from the state and calculate the answer."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "920630818300104"
+      ],
+      "text/plain": [
+       "920630818300104"
+      ]
+     },
+     "execution_count": 7,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "solver.model().eval(sum(start_position))"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.12.0"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/aoc2023-other/day-24/day-24.rkt b/aoc2023-other/day-24/day-24.rkt
new file mode 100644
index 0000000..f366df1
--- /dev/null
+++ b/aoc2023-other/day-24/day-24.rkt
@@ -0,0 +1,43 @@
+#lang rosette
+
+(require advent-of-code
+         threading)
+
+(struct hail (posn vel) #:transparent)
+(struct posn (x y z) #:transparent)
+(struct vel (x y z) #:transparent)
+
+(define input (fetch-aoc-input (find-session) 2023 24 #:cache #true))
+
+(define LOWER-BOUND 200000000000000)
+(define UPPER-BOUND 400000000000000)
+
+(define (parse-hail-record str)
+  (match-define (list p v) (string-split str " @ "))
+  (hail (~> p (string-split ",") (map (λ~> string-trim string->number) _) (apply posn _))
+        (~> v (string-split ",") (map (λ~> string-trim string->number) _) (apply vel _))))
+
+(define hail-paths
+  (for/list ([hail (in-list (string-split input "\n"))])
+    (parse-hail-record hail)))
+
+;; part 1
+(define (valid-intersection? h1 h2)
+  (match-define (hail (posn x1 y1 _) (vel vx1 vy1 _)) h1)
+  (match-define (hail (posn x2 y2 _) (vel vx2 vy2 _)) h2)
+  (cond
+    [(= (* vy1 vx2) (* vx1 vy2)) #f]
+    [else
+     (define t1 (/ (- (* vy2 (- x1 x2)) (* vx2 (- y1 y2))) (- (* vy1 vx2) (* vx1 vy2))))
+     (define t2 (/ (- (* vy1 (- x2 x1)) (* vx1 (- y2 y1))) (- (* vy2 vx1) (* vx2 vy1))))
+
+     (define x (+ x1 (* t1 vx1)))
+     (define y (+ y1 (* t1 vy1)))
+
+     (and (<= LOWER-BOUND x UPPER-BOUND) (<= LOWER-BOUND y UPPER-BOUND) (<= 0 t1) (<= 0 t2))]))
+
+(for/sum ([(trial-paths) (in-combinations hail-paths 2)] ;
+          #:when (apply valid-intersection? trial-paths))
+         1)
+
+;; part 2 - in Z3 via Python