diff --git a/day24/notes.org b/day24/notes.org index c9ab37d..cb1e52a 100644 --- a/day24/notes.org +++ b/day24/notes.org @@ -103,3 +103,14 @@ let's try? z + Dz * t2 == 390970075767404 + -149 * t2 solve for x, y, z, Dx, Dy, Dz, t1, t2, t3. ti > 0 #+end_src +* got some solution +enefedov@LLF33A87M:~/Documents/personal/advent-of-code-2023$ python day24/pythonZ3/forInput.py +Solution: [t0 = 666003776903, + t2 = 779453185471, + t1 = 654152070134, + Dz = 18, + Dx = 47, + Dy = -360, + z = 273997500449219, + y = 463222539161932, + x = 239756157786030] diff --git a/day24/pythonZ3/forInput.py b/day24/pythonZ3/forInput.py new file mode 100644 index 0000000..d7a97e9 --- /dev/null +++ b/day24/pythonZ3/forInput.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 + +from z3 import * + +s = Solver() + +x = Real('x') +Dx = Real('Dx') +y = Real('y') +Dy = Real('Dy') +z = Real('z') +Dz = Real('Dz') +t0 = Real('t0') +eqT0 = t0 >= 0 +eq0x = x + Dx * t0 == (185 * t0) + 147847636573416 +eq0y = y + Dy * t0 == (49 * t0) + 190826994408605 +eq0z = z + Dz * t0 == (219 * t0) + 140130741291716 +t1 = Real('t1') +eqT1 = t1 >= 0 +eq1x = x + Dx * t1 == (-26 * t1) + 287509258905812 +eq1y = y + Dy * t1 == (31 * t1) + 207449079739538 +eq1z = z + Dz * t1 == (8 * t1) + 280539021150559 +t2 = Real('t2') +eqT2 = t2 >= 0 +eq2x = x + Dx * t2 == (-147 * t2) + 390970075767404 +eq2y = y + Dy * t2 == (-453 * t2) + 535711685410735 +eq2z = z + Dz * t2 == (-149 * t2) + 404166182422876 +#solve for x, y, z, Dx, Dy, Dz, t1, t2, t3. + + +s.add(eqT0, + eq0x, + eq0y, + eq0z, + eqT1, + eq1x, + eq1y, + eq1z, + eqT2, + eq2x, + eq2y, +eq2z) + +if s.check() == sat: + print("Solution:", s.model()) +else: + print("No solution found") + +print(273997500449219 + 463222539161932 + 239756157786030)