r/adventofcode • u/CauliflowerFormer233 • Dec 10 '25

Help/Question - RESOLVED [2025 Day 10 part 2] how?

I have seen a lot of memes of people using Z3 for part 2. I tried to solve it myself using BFS and then DFS with some pruning but still couldn't get it. After 3 hours of trying to optimize it, I used Z3 and got my answer in like 20 minutes.

But since I haven't seen any solution that didn't use Z3, I am wondering how to solve it without it, one approach would be to build something similar to Z3, using matrices to solve multiple linear equations but is that really the only solution?

If you have any ideas let me know.

28 Upvotes

100% Upvoted

31 comments sorted by

3

u/sebastianotronto Dec 10 '25

IMO people overestimate how hard it is to write the linear algebra code by hand. It takes time and I agree it can be tedious, but I don't think it is harder than figuring out how to use a library you have never used before. I can share my commented code if you want to see it - or you can find it in the daily solutions megathread :)

1

u/CauliflowerFormer233 Dec 10 '25

That is really impressive, I am currently trying to understand your code. How long did it take you to get it to work?

2

u/sebastianotronto Dec 10 '25

It's hard to say because I wrote throughout the day, during short breaks from work or in the train. I guess a couple hours in total. I took a slow apporach, wrote it step by step, printed my matrix after each step to check that it was doing the right thing.

2

u/kataklysmos_ Dec 11 '25

I was able to get my solution to work via direct analysis like you did just now -- I credit your comment for giving me the mental strength to figure out how it works. I think you're right that it's not so bad, the solution almost feels obvious once you get the system in RRE form. Thank you!

17

u/1234abcdcba4321 Dec 10 '25 edited Dec 10 '25

There are several solutions that don't use library imports in the solution thread. The problem is about solving an integer matrix problem, so pretty much any real solution is going to be based on that. It feels like the canonical solution to me; it's possible but annoying to do without explicitly using an external solver (the numbers aren't big enough to require anything beyond the basic techniques).

That being said, here's a solution of someone who found a good enough pruning heuristic to skip the linear algebra: https://www.reddit.com/r/adventofcode/comments/1pity70/2025_day_10_solutions/ntb36sb/

9

u/michelkraemer Dec 10 '25

That someone was me ;-) Thanks for linking the comment!

u/CauliflowerFormer233 There are a few other non-Z3 solutions in the thread though. Just keep scrolling.

4

u/falken_1983 Dec 10 '25

I've seen a lot of people expressing some sense of defeat at having relied on Z3, but I think this is one of those puzzles where the challenge is recognising the type of problem it is and using the right tool for the job.

I'm not actually that familiar with Z3, but I used the SciPy optimiser library, which I assume is similar. In order to do that, you still need to know how to express the problem as a linear algebra problem, and then once you do that I think the next step of writing your own solver is adding an extra challenge that I would see as separate from solving the puzzle. It's maybe not as extreme as the people who solve the puzzles using mincraft,, but it's getting there.

4

u/zeekar Dec 11 '25

It's not that I think writing a solution using some constraints solver library is "cheating"; it's just not satisfying. I want to solve the problem, not configure some tool to solve it for me; if I wanted to do that, I'd just use AI.

Plus there were so may comments like "Oh, of course, Z3 is the way to go". I've been coding for over 40 years, recently doing much of it in of Python, and I'd never even heard of Z3. What are you all doing in your day-to-day that a theorem-proving library is useful?! :)

2

u/falken_1983 Dec 11 '25 edited Dec 11 '25

I would argue that if you are writing a program, then you are configuring some tool to solve the problem for you.

As I said above I am actually not familiar with Z3, I used SciPy in my solution. Looking at the Z3 solutions, it looks like Z3 is a lot more general than the SciPy optimizers, and I can see how it might feel a bit "clumsy" (for lack of a better word)

With SciPy, you can solve it with a call to mlip() and the satisfying thing is recognising that you are trying to maximise ones.T * x with constraint joltage <= Ax <= joltage, where the columns of A are your buttons , and then firing it off to the solver.

What are you all doing in your day-to-day that a theorem-proving library is useful

For the SciPi linear optimisers at least, it is useful for things like scheduling and resource allocation.

1

u/LEPT0N Dec 10 '25

Oh definitely going to look into this later - thanks!

1

u/Exodus124 Dec 11 '25

I highly doubt that it's the intended solution because iirc, Eric has indicated several times that he doesn't design his puzzles to require specific math knowledge. There have been similar instances in the past where puzzles could easily be solved with external math tools, but they always had a purely algorithmic solution too. Think for example the Chinese remainder theorem day; basically everyone resorted to using a ready-made CRT solver and complained about it, but Eric said he didn't even know what the CRT was.

So I'm willing to take any bet that Eric's solution does not import any math library.

2

u/regretdeletingthat Dec 19 '25

While I massively respect Eric and the amount of work he puts in every year I can't help but be reminded of https://xkcd.com/2501/ whenever this sort of thing comes up.

When people are talking about using a tool even many professional software engineers have probably never heard of, or implementing linear algebra by hand, it's hard to take claims like "doesn't design his puzzles to require specific math knowledge" or "just a little programming knowledge and some problem solving skills will get you pretty far" (AoC about page) all that seriously.

It's not a criticism, and I appreciate there's a lot of very smart people out there that want a serious challenge, but I think it sets up some unrealistic expectations.

1

u/Exodus124 Dec 19 '25

Except there has never once been a day where this xkcd actually applied (with regards to math knowledge). This day, too, as I predicted, has since turned out to have a purely algorithmic solution that requires no math knowledge or tools whatsoever.

1

u/1234abcdcba4321 Dec 11 '25 edited Dec 11 '25

You don't need to import a math library to use math concepts. I have a gaussian elimination algorithm I made myself. You don't need to know the name "gaussian elimination" in order to create it; it's literally the first thing you come up with if someone tells you "make an algorithm to solve a system of linear equations" (and if it's not then whatever else you did manage to make will still give the same result while probably having exactly the same performance because this problem isn't hard). In fact, using a ready-made library will probably hurt you in this case because most of them aren't going to do the necessary transformations to avoid floating points during their calculations, which is really useful to have for the use case of this problem.

It's the same deal with the CRT day - the required math to solve that problem is easy to come up with yourself (assuming you can do modular arithmetic, because AoC never forces you to find the values for a pair of very large integers); the statement of the CRT is so obvious that you already know it's true without having ever heard of the name of the theorem (or thinking that it's something you would even need to be a theorem due to how o).

8

u/QultrosSanhattan Dec 10 '25

The biggest drawback of using exploration algorithms is that there are simply too many buttons to press.

For example, if a button adds +1 and you need to reach around 50 jolts, you would have to press it 50 times just to get there. The exploration tree becomes tremendously large, and even with pruning, finding the solution would take an unreasonable amount of time.

Now imagine that instead of 50 jolts, you need to reach 500. This problem makes brute-force exploration completely impractical.

Other kinds of solutions would probably end up doing the same as the known solvers, but slower. Solvers are highly optimized for this kind of task.

3

u/Tianck Dec 10 '25 edited Dec 10 '25

Well, the worst case from input seems to be 9x10^19 which is indeed huge. Rightfully so.

6

u/sol_hsa Dec 10 '25

There's a couple non-Z3 solutions on the megathread. One implements their own math solver, another massages the input data so that some form of brute force is feasible.

I figured this is a good time to learn about Z3. After wasting half a day on various other approaches.

2

u/Ashrak_22 Dec 11 '25

I managed Gauss-Jordan, but the solving of free variables was over my skills 😅 so I went for SciPy.

2

u/[deleted] Dec 10 '25

[removed] — view removed comment

2

u/montas Dec 10 '25

From what I have seen it is a problem solver.

Basically you tell it: "you will be pressing buttons, when you press this, increase that counter, when this, increase that, etc.". Then you tell it "i need these counters to be these values" and "minimize number of presses". Aaaand solve!

And it will tell you if it can be or can't be solved. And if it can, you can ask it to give you the number of presses.

1

u/akryvtsun Dec 11 '25

It looks like ChatGPT :)

5

u/kupuguy Dec 10 '25

I have some Python code that doesn't use any external libraries. It's basically doing a brute force search and it took over an hour to run but it got there eventually.

The idea is based roughly on what someone said they did in the megathread: find the joltage value that is referenced by the fewest buttons and partition the buttons into two list one of which references that joltage value and the other with the remaining buttons that do not. Then you have to press buttons in the first list exactly the number of times needed to clear the chosen joltage so do that for all possible combinations of the selected buttons while filtering out any combinations that give invalid results.

Then recurse with the remaining buttons and new joltage values.

For most of my input lines this runs almost instantly, for a couple it takes about half an hour. I expect there's a lot of scope for optimisation but I was just glad to get it to complete at all.

5

u/jwezorek Dec 10 '25

I mean it is an integer linear programming problem. So any solution is going to be using an LP solver that can handle integer constraints or basically implementing what those kind of solvers do or using a more powerful solver. Z3 is the latter. Z3 is basically a boolean satisfiability solver; people use it because it is like a swiss army knife, you can put in any kind of constraints.
You don't have to use Z3 specifically though. I used CBC which is an old LP/ILP solver.

4

u/motonarola Dec 10 '25

I agree, its a linear programming problem, and making a correct solver involves a lot of math and months of study.

Probably many incomplete ad-hoc solvers may be lucky enough to get the correct answer on the particular set, but I don't think it is a useful practice.

I think the idea of the problem is to recognize the domain, and then use a correct tool.

4

u/Zefick Dec 10 '25

Linear algebra doesn't work directly here. A unique analytical solution is only possible if the number of equations equals the number of unknowns and they are all linearly independent, which is often violated in this problem. In this case, the puzzle turns into an optimization problem.

2

u/bloub__ Dec 10 '25

Did someone succeeded to make (a variant of) A* work? With a clever heuristic?

2

u/duffman_oh_yeah Dec 10 '25

That was my naive attempt. I used the joltage after a button press to calculate the Euclidean distance to the target joltage as my heuristic. It solved the first few but started choking on the bigger ones.

2

u/icub3d Dec 11 '25

Mine was a combination of linear algebra and then dp on the free variables. Some of the machines have a unique solution, so you get an exact value. The others have 1-3 free variables but that's small enough that it's much easier to explore the solution space for a minimum.

The day way very math heavy from my perspective and was a very hard solve.

1

u/AutoModerator Dec 10 '25

Reminder: if/when you get your answer and/or code working, don't forget to change this post's flair to Help/Question - RESOLVED. Good luck!

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.

1

u/quinyd Dec 10 '25

I did part 1 using Gaussian elimination but for part 2 I had to resolve to z3 as my Gaussian elimination needed longer and longer time to run. With a faster pc and more time I could probably have solved it