day24: input system for python z3

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]

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)