aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJ.J <thechairman@thechairman.info>2023-12-24 16:20:24 -0500
committerJ.J <thechairman@thechairman.info>2023-12-24 16:20:24 -0500
commit48c2d7f41a0b6c9bb4279f6ab0ce16c2c94155d8 (patch)
treeaec8e605773283adf69db060f1443557c63cf3d8
parent11902b67b519a9096d032f5887a33be4fc3e0b04 (diff)
downloadgleam_aoc-48c2d7f41a0b6c9bb4279f6ab0ce16c2c94155d8.tar.gz
gleam_aoc-48c2d7f41a0b6c9bb4279f6ab0ce16c2c94155d8.zip
racket day 24 parts 1 and 2 complete
-rw-r--r--aoc2023-other/day-24/day-24.ipynb216
-rw-r--r--aoc2023-other/day-24/day-24a.rkt (renamed from aoc2023-other/day-24/day-24.rkt)0
-rw-r--r--aoc2023-other/day-24/day-24b.rkt34
3 files changed, 34 insertions, 216 deletions
diff --git a/aoc2023-other/day-24/day-24.ipynb b/aoc2023-other/day-24/day-24.ipynb
deleted file mode 100644
index 0167bf7..0000000
--- a/aoc2023-other/day-24/day-24.ipynb
+++ /dev/null
@@ -1,216 +0,0 @@
-{
- "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-24a.rkt
index f366df1..f366df1 100644
--- a/aoc2023-other/day-24/day-24.rkt
+++ b/aoc2023-other/day-24/day-24a.rkt
diff --git a/aoc2023-other/day-24/day-24b.rkt b/aoc2023-other/day-24/day-24b.rkt
new file mode 100644
index 0000000..38e4317
--- /dev/null
+++ b/aoc2023-other/day-24/day-24b.rkt
@@ -0,0 +1,34 @@
+#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 (->struct f str)
+ (~> str (string-split ",") (map (λ~> string-trim string->number) _) (apply f _)))
+
+(define (parse-hail-record str)
+ (match-define (list p v) (string-split str " @ "))
+ (hail (->struct p posn) (->struct v vel)))
+
+(define hail-paths
+ (for/list ([hail (in-list (string-split input "\n"))] ;
+ [_ (in-range 3)])
+ (parse-hail-record hail)))
+
+(define-symbolic px py pz vx vy vz integer?)
+
+(define sol
+ (solve ;
+ (for ([path (in-list hail-paths)])
+ (define-symbolic* t integer?)
+ (assert (= (+ px (* vx t)) (+ (~> path hail-posn posn-x) (* (~> path hail-vel vel-x) t))))
+ (assert (= (+ py (* vy t)) (+ (~> path hail-posn posn-y) (* (~> path hail-vel vel-y) t))))
+ (assert (= (+ pz (* vz t)) (+ (~> path hail-posn posn-z) (* (~> path hail-vel vel-z) t)))))))
+
+(evaluate (+ px py pz) sol)