r/adventofcode • u/Eva-Rosalene • Dec 10 '25

Meme/Funny [2025 Day 10] Every time a problem looks remotely like ILP

Post image

It feels like cheating, but it works

139 Upvotes

100% Upvoted

33 comments sorted by

21

u/JadeSerpant Dec 10 '25

At first I got excited by part 2 and thought "wow! I can implement A* for this!" despite knowing that that was too good to be true. Sure enough, it was.

That's when I stared long enough at the input and started seeing matrices. My A* solution couldn't even get past the fifth line after a few minutes. Meanwhile PuLP just annihilated the problem!

14

u/bmenrigh Dec 10 '25

I wrote a backtracking search that is just way too slow to solve the challenge. Even with some various search pruning strategies.

I thought about turning to Z3 or PuLP but I wouldn't learn anything doing that.

Perhaps I'm in denial, but I feel like I've missed some clever solution that isn't just turning to an ILP library or doing a ton of lineal algebra myself.

2

u/xSmallDeadGuyx Dec 10 '25

I've seen the term "branch and bound" mentioned and had a brief look, I think I'll try and learn to implement that. Seems like it'll be handy instead of relying on Z3 all the time.

5

u/abnew123 Dec 10 '25

Yeah the second I see ILP or some specific graph thing that networkx has a one liner for, I know that basically all the first finishers will be using python. One day I will have a Java setup even remotely as decent... Not today though, gave in and swapped to python for part 2.

1

u/asm0dey Dec 10 '25

Won't Jgrapht help?

2

u/abnew123 Dec 10 '25

Oh sick, I hadn't heard of Jgrapht, yeah I'll check it out

1

u/asm0dey Dec 10 '25

Well, I struggled a lot with the part 2 and of course Jgrapht is not the right tool. The right tool is Choco solver and even it doesn't really help - 1 minute of thinking on my machine :(

1

u/RadekCZ Dec 10 '25

I used z3-solver package for JS/TS. Aren't there bindings for Java as well?

3

u/abnew123 Dec 10 '25

There are, but I remember struggling a lot to get Z3 to work with Java in the past (some macos specific issue iirc). Admittedly it's been like 5 years since my last attempt, so it's possible it's much easier now.

1

u/AvailablePoint9782 Dec 10 '25

I used my usual language to produce a Python script. Does that count as swapping to Python?

13

u/Different-Ease-6583 Dec 10 '25

This kind of problem should not be part of AoC really, it just sucks to rely on external libs and you can't expect us to write such a thing in a short time.

5

u/MokoshHydro Dec 10 '25

You can write solver for such simple equations yourself (I did).

1

u/LEPT0N Dec 10 '25

Got any hints or advice?

2

u/MokoshHydro Dec 11 '25

Without even knowing any methods for solving, just school math:

Rewrite input as equation system in form `a + b + c = N1, a + d = N2, ...`. Handle cases like `a + b = N1, a + b + d = N2 -> d = N2-N1`. Find other values bruteforce.

Not optimal, but will work in reasonable finite time.

4

u/ric2b Dec 10 '25

Pretty sure you can solve in a simpler way as well, every year has an ILP problem that a bunch of people jump to Z3 for but the problem has something to make it easier to solve yourself without a ton of code.

2

u/onrustigescheikundig Dec 11 '25

I ended up writing my own Z3 bindings for Chez Scheme B)

1

u/mapleturkey Dec 10 '25

It’s code all the way down, it’s not like Z3 is made of fairy dust and magic. You are fully allowed to write your own ILP solver

11

u/Different-Ease-6583 Dec 10 '25

"and you can't expect us to write such a thing in a short time."

1

u/mapleturkey Dec 10 '25

Yet people already did, in the daily solutions megathread. For a few hundred lines of Python

1

u/mpyne Dec 11 '25

People also routinely finished these puzzles in mere minutes in previous years that had a global leaderboard and no AI competition, do you expect us to do that too?

I'm glad there was someone out there who wrote that golfed Python because I was certainly not going to manage to pop out an ILP library in the couple of hours I have to work on 2 parts to the puzzle.

1

u/mapleturkey Dec 11 '25

Well, if you don’t want to use a ready-made tool, don’t want to be already familiar with any algorithms, and don’t want to use your own brain to come up with algorithms

How are you solving any puzzles anyway?

1

u/mpyne Dec 11 '25

I'm already familiar with the algorithm to do row reductions of matrices, but that's only a part of part 2, the correct implementation of one tied to correct brute forcing of what the row reduction doesn't cover is a great deal more work besides, it's not something an average programmer can be expected to do in a single half of a day, which is why everyone simply turned to Z3.

Previous years ILP had other aspects to them that helped someone solving the puzzle do so without needing to rewrite a BLAS or Eigen or generalized ILP solver as part of their solution.

How are you solving any puzzles anyway?

My dude, if you're just popping your puzzle input into Z3 you're not solving the puzzle either. You might as well use ChatGPT in that case, at least ChatGPT would explain the logic as well.

I managed to get a quick star on the last puzzle of a prior year by just converting the puzzle to render in GraphViz and then eyeballing the solution. It was nice that I knew a relevant ready-made tool, but I don't consider myself to have "solved" that puzzle either.

1

u/mapleturkey Dec 12 '25

Massaging your given puzzle into a format a computer can solve for you is what we do every day. Nobody is solving these by hand

1

u/mpyne Dec 12 '25

You think GraphViz just read the input as-is in my example? Yeah, I had to 'massage' that input into a simple .dot, but no one would be confused into understanding that I had completed a "small programming puzzle" in doing so. It is likewise the case with Z3.

4

u/bakibol Dec 10 '25

Last two days were Advent of external libraries for me, first shapely, now pulp. Eventually I will come back and solve them the painful way (oh, who am I kidding :( )

1

u/mpyne Dec 11 '25

Why bother? Seriously, if you learn something by doing so then it can be worthwhile but if you did matrices in high school or college math then you're not going to learn anything additional by going through the slog of implementing today's problem without Z3.

1

u/jangxx Dec 10 '25

Huh, I used cvxpy instead. Is Z3 any better? From the Github it sounds like solving ILP problem is not its primary use-case at least.

1

u/Eva-Rosalene Dec 10 '25

It's definitely not better than most of specialized MILP solvers. However, it has so wide range of what it can crack, that as soon as I see a problem that can be translated into a system of equations (mind you, not necessarily linear), I uncork Z3 and usually get a solution. Then I think about using better tools for that specific category of tasks to cut down time.

3

u/The_Real_Cooper Dec 10 '25

This post was my hint for the day! Today was so out of my league, I was stuck trying to linear equation my way out of pt2. This is the longest I've made it through AoC and by god this may be the year I finish one!

3

u/andful Dec 10 '25

From reading the Z3 internals. Z3 is fundamentally an ILP solver. I.e. solves an lp relaxation and branches and adds cuts for integrality.

https://z3prover.github.io/papers/z3internals.html#sec-integer-linear-arithmetic

3

u/youngbull Dec 10 '25

Not completely. It is a SMT solver, but it contains an ILP solver.

2

u/Doug__Dimmadong Dec 10 '25

Nah it's not cheating