day24: input system for python z3

2023-12-24 11:50:56 +00:00
parent 5b03b8f156
commit 665987395f
2 changed files with 62 additions and 0 deletions
--- a/day24/notes.org
+++ b/day24/notes.org
@@ -103,3 +103,16 @@ 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
+https://z3prover.github.io/papers/programmingz3.html#sec-intro
+
+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]