From 48c2d7f41a0b6c9bb4279f6ab0ce16c2c94155d8 Mon Sep 17 00:00:00 2001 From: "J.J" Date: Sun, 24 Dec 2023 16:20:24 -0500 Subject: racket day 24 parts 1 and 2 complete --- aoc2023-other/day-24/day-24.ipynb | 216 -------------------------------------- aoc2023-other/day-24/day-24.rkt | 43 -------- aoc2023-other/day-24/day-24a.rkt | 43 ++++++++ aoc2023-other/day-24/day-24b.rkt | 34 ++++++ 4 files changed, 77 insertions(+), 259 deletions(-) delete mode 100644 aoc2023-other/day-24/day-24.ipynb delete mode 100644 aoc2023-other/day-24/day-24.rkt create mode 100644 aoc2023-other/day-24/day-24a.rkt create mode 100644 aoc2023-other/day-24/day-24b.rkt 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": [ - "sat" - ], - "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": [ - "[t2 = 474506740599,\n", - " t0 = 931974028142,\n", - " v0 = -337,\n", - " t1 = 829702369046,\n", - " v1 = -6,\n", - " v2 = 155,\n", - " p0 = 446533732372768,\n", - " p2 = 180204909018503,\n", - " p1 = 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 deleted file mode 100644 index f366df1..0000000 --- a/aoc2023-other/day-24/day-24.rkt +++ /dev/null @@ -1,43 +0,0 @@ -#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 diff --git a/aoc2023-other/day-24/day-24a.rkt b/aoc2023-other/day-24/day-24a.rkt new file mode 100644 index 0000000..f366df1 --- /dev/null +++ b/aoc2023-other/day-24/day-24a.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 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) -- cgit v1.2.3