Unable to load image

A fast AoC day 15 part 2 solution without cheating*

[*] with blatant cheating that would make @Snakes blush

pip install z3-solver

    import z3
    x, y = z3.Ints('x y')
    zs = z3.Solver()
    zs.add(0 <= x, x <= size_limit)
    zs.add(0 <= y, y <= size_limit)
    for it in data:
        zs.add(z3.Abs(x - it.sx) + z3.Abs(y - it.sy) > it.r)
    assert zs.check() == z3.sat
    return zs.model().eval(x * 4000_000 + y).as_long()

15_1 took 0.212 seconds

6
Jump in the discussion.

No email address required.

Hey now. Getting Mathematica to solve it is still programming :p

Jump in the discussion.

No email address required.

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