Unable to load image

rDrama Advent of Code Day 24: z3 Edition

Summary for those just joining us:

Advent of Code is an annual Christmas themed coding challenge that runs from December 1st until christmas. Each day the coding problems get progressively harder. We have a leaderboard and pretty good turnout, so feel free to hop in at any time and show your stuff!

Whether you have a single line monstrosity or a beautiful phone book sized stack of OOP code, you can export it in a nice little image for sharing at https://carbon.vercel.app

What did you think about today's problem?

https://adventofcode.com/2023

Our Code is 2416137-393b284c (No need to share your profile, you have the option to join anonymously if you don't want us to see your github)

16
Jump in the discussion.

No email address required.

Finally I got to use z3, bitches! Global rank 50 on part 2!

https://i.rdrama.net/images/17034015305229828.webp

  import z3
  x, y, z = z3.Ints('x y z')
  dx, dy, dz = z3.Ints('dx dy dz')
  zs = z3.Solver()
  for i in range(len(positions)):
      t = z3.Int(f't{i}')
      zs.add(t >= 0)
      zs.add(positions[i][0] + t * directions[i][0] == x + t * dx)
      zs.add(positions[i][1] + t * directions[i][1] == y + t * dy)
      zs.add(positions[i][2] + t * directions[i][2] == z + t * dz)

  assert zs.check() == z3.sat
  return zs.model().eval(x + y + z).as_long()
Jump in the discussion.

No email address required.

@not-krampus you don't like people using networkx? Eat your heart out LMAO!

Jump in the discussion.

No email address required.

Did you actually need 12 lines? :marseypathetic:

ps vs←↓⍉↑r
rvs←{(⊂∘⍒⌷⊢)0~⍨{3>≢⍵:0 ⋄ ⊂(≢⍵),⍺}⌸⍵}¨↓⍉↑vs
vr←∊{∩/⍵∘{∪∊⍵∘(+,-)¨∊(+,-)¨(∪⊢∨⍳)∨/0~⍨,(∘.-)⍨(⍺⊃¨ps)/⍨(⍺⊃¨vs)=⍵}¨2⊃¨⍵⊃rvs}¨⍳3
phs vhs←↓⍉↑2↑r ⋄ vc←⊃,¨/vt←vr∘-¨vhs
qc←⊃,¨/phs((1∘⌽⍤⊣ׯ1⌽⊢)-¯1∘⌽⍤⊣×1⌽⊢)¨vt
d←{((qc⊃⍨1⊃⍺)(vc⊃⍨2⊃⍺))÷⍥{-/×⌿0 1⌽↑⍵}((vc⊃⍨1⊃⍵)(vc⊃⍨2⊃⍵))}
⎕←+/d/¨((3 1)(2 1))((1 2)(3 2))((2 3)(1 3))

yes I spend a good part of Christmas working this out on paper

Jump in the discussion.

No email address required.

Global rank 50 on part 2!

:#soyjihadi: :#soyjihadi: :#soyjihadi: :#soyjihadi: :#soyjihadi:

MASHALLAH

Jump in the discussion.

No email address required.

It's impressive that you managed to figure out the equations for pt 2, write them and solve them in 12 mins. It's not exactly quick to run and pt 2 wasn't obvious while you were doing pt 1.

Jump in the discussion.

No email address required.

It's not exactly quick to run

It is actually. About a second, idk.

Jump in the discussion.

No email address required.

It's quick if you use BitVec, that implementation with Int is pretty slow.

Jump in the discussion.

No email address required.

Hello

Problem read from 'input/ac2023d24_input.txt'

24_1 took 0.279 seconds

13910

Problem read from 'input/ac2023d24_input.txt'

24_2 took 2.901 seconds

618534564836937

How do I use BitVec for it?

Jump in the discussion.

No email address required.

Weird it just keeps running on pt2 real for me. Just use BitVec(x, 64) anywhere you use Int(x)

Jump in the discussion.

No email address required.

Interesting, maybe I got lucky with the input! Ty for the tip.

Jump in the discussion.

No email address required.

Link copied to clipboard
Action successful!
Error, please refresh the page and try again.