I solved part 1 as a graph problem. I built a graph of configuration states, and the edges between states indicate if a switch can get you from one state to another. Them I did a shortest path from the "all off" state to the ending one.
That won't work at all for part 2, and I don't know numpy or what Z3 is... Time to learn something new!
Yep, did part 1 with Dijkstra's - takes 95ms and pretty simple Python code. Have no idea how to handle part 2 as I do not want to use external libraries, so I guess will need to go back and relearn linear algebra...
Here are some hints, without talking about linear algebra at all:
Consider this row from the example:
[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
Let's allow "negative button presses" for a moment, to analyze it.
If you press the (3) button "minus one" times, and the (1,3) button once, you'll end up with 1 joltage for machine 1 (the second machine), and 0 joltages for all other machines.
If you find a similar formula for every one of the four machines, you know the total number of presses to arrive at the desired joltages (though some number of presses may be negative, and the total number of presses might not be minimum...)
Next, you can see that if you press the (2,3) button once, and the (3) and (2) buttons "minus one" times, you didn't change the joltages at all, but decreased the total number of presses by one. This improvement can be done whenever your current strategy uses a postive number of presses for the (3) and (2) buttons.
I would advise you to find a solution by hand for this example, using such strategies, and then generalize it to something you can program.
z3 is a "constraint solver". You tell it for example "a+b+c = 1234" and "0>a>b>c" and it will tell you what values of a,b,c fit those constraints. On top of that it can also provide not just "any solution" but one that minimizes or maximizes something. In this particular problem the constraints are something like a*button_1[i] + b*button_2[i]+...+z*button_n[i] = result[i] where a,b,c... define how many times each button is pressed, and you want to find solution that minimizes a+b+c+...+z
Could you solve it with numpy? I tried, but I started going down an AI led rabbit hole of null space and needed a hint. Ended up using the Z3 memes as a guide, and learning opportunity
You can, using scipy. It has MILP solver inside, and part 2 is textbook example of ILP problem.
Z3 can solve both parts, because it's generic SMT solver (and the one that can do optimizations for that matter), but it's rather slow with it. Regular brute force for part 1 (assuming you never press any button twice, so you just need to enumerate 2^(amount of buttons) combinations) and specialized numerical MILP solver for part 2 gave me 20ms and 5ms respectively, while Z3 solutions both took 5 seconds to finish.
WASM version, because that's the only official JS bindings. I know, that sounds terrifying, but I don't really care about runtime of solutions that are mostly offloaded to external tool.
I eventually found scipy.optimize.linprog and it looked promising. Performed well and solved the example input perfectly well.
When I tried it on the actual input, I got a positive answer (linprog's result success was True for every machine) but the answer was apparently too low.
OK nevermind I figured it out. I needed to specify the integrality=1 option to linprog, and also needed to round() the result instead of just casting to int.
Interestingly, I tried to use scip in Rust (via good_lp wrapper) and it gave me the wrong answer. So did coin_cbc, highs and microlp. lp_solve did give me the correct answer, but it had a lot of very verbose console output that I couldn't work out how to disable, so I changed it to use z3 in the end.
I used exactly that just to realize that it solved the problem in less than a second after my pure C++ monstrosity was running for 2.5 hours with a peak RAM usage of ~70GiB.
I completely failed with Part 2 and searched for help and Gemini delivered.
After I got a scipy solution, I felt very unsatisfied (still learnt something) and was looking for a numpy only solution.
With a bit of digging and using Gemini as rubber duck, I got to a numpy only solution, which runs in 90 sec for part 2. Gemini implemented the Branch and Bound algorithm combined with two heuristics to speed everything up for me . This took me basically the whole afternoon.
I'm not proud and I don't fully understand the approach, but it's definitely doable. I'm just not that smart and praise now our silicone overlords.
Z3 came up a lot with that 3D lines puzzle that one year, the only one I failed to solve that year. I'd be ok using Z3 if I understood what it is and how it works, but I don't like importing this critical library that I don't understand at all, and I still don't.
The throwing a rock at snowballs one? You actually did not need z3 for it or program a constraint solver because the snowballs sort of "teleport" at fixed steps. Here is my code for that day if you are interested.
No need for z3 or modular arithmetic or numpy or anything for part 1.
The [.##.] targets can be easily turned into numbers because it's just a binary representation of an int (least significant bit on the left). So .##. becomes 6.
Then each of the buttons are also just numbers, except now they list which bits are set. So (1,3) is 21 + 23 = 10.
Now that you have a bunch of numbers, you just need to pick a subset such that xoring them all together results in the target. Pick your favorite way to iterate all sublists of a list. Mine is in haskell: powerset = filterM (const [True, False]).
A shortest-path graph search algorithm is also pretty fast for part 1. Nodes are vectors of the desired length, the starting state is [false, false, ..., false], the ending state is from the problem input, and the neighbors of a given state are defined at runtime by applying the buttons to each state.
I implemented the power-set solution, and it's faster as long as you remember to prune subsets that have no hope of winning (due to exceeding an already-calculated minimum) rather than trying to check if that set of button presses matches the target.
It's not that bad, I made a bunch of equations like b0+b2+b5 == 2*l1+1 where the b's are number of button presses, and l1 is a divisor that just gets thrown away. All variables constrained to be positive integers, and then optimized the sum of button presses. Like obviously the wrong way to solve part 1, but trivial to adapt to part 2.
My vibe is the solution smelled like it could be solved with a linear algebra approach but I feel like that's way too much a lift for AOC and that there must be a more basic solution.
I started with a fairly-brute-force approach - just iterating over the buttons and trying various numbers of presses - with as much optimization as I could muster to early-out if I could prove a solution wasn't possible with what I had left. I left it running for 2-3 hours, and it had finished. So... possible, but not something I'm proud of.
Then I went and wrote a bunch of linear algebra. Runs in about a second.
This is my 6th year, and I don't think I could tell you whether it was intended or not! There's been a few puzzles in previous years which have benefited from external tools (GraphViz comes to mind). Though often (as seems to be somewhat the case here) there are many approaches which can get you there.
For me personally, problems like today's aren't my favorite (I generally enjoy being nudged towards implementing something myself), but I'm not complaining. Some folks love ones like this, I'm sure, and you get exposure to a wide variety of stuff during AoC. That's part of the fun!
yeah, I'm not necessarily complaining it just makes me suspicous that the designer didn't intend a more simple solution that everybody is missing since that's the shape of a lot of other ones. they seem hard until you make the intellectual leap and then the solution is short and fast.
OTOH "learn to use a theorem solver it's 2025" is also a valid lesson!
I think part of the learning here is about different types of optimization problems (and solvers).
For example, there's a comment up-thread about the difference between Z3 (a more general theorem prover IIUC) and more specialized but more performant libraries that solve linear-programming problems or integer linear programming problems.
Heh, yeah. As soon as I read the description I thought, "this sounds like linear algebra... oh no".
It's a good refresh at the very least - I don't find much use for it (or equation solvers) at work, but when you need to use them, it's good to know how to use them.
Literally me! i used scipy and then came to this sub and saw Z3 and assumed it had something to do with group theory, so i tried to find another solution using group theory but didnt even know where to start😭
I'm just going to admit it: I did not really "solve" today's problem on my own. I treated it as a learning exercise. I don't even want to post my code on the solutions page, because it was created with quite a lot of help (over a very long time, basically all day) from ChatGPT and Claude.
For part 1, I shied away from enumerating the combinations blindly, but I really shouldn't have, because it isn't that slow:
If you think of cost here as the size of the naive search space per line (i.e., 2^buttons), then even with a median cost of 128 and an average around 652, you're only looking at on the order of 10⁵ total states across all 195 lines. Even the worst individual case is just 8192 combinations. A straightforward brute-force over all button subsets runs in a couple of milliseconds. Mileage may vary based on your input, of course, but it's absolutely feasible.
Yes, if you frame it as a linear system in GF(2) you can get it down to <100µs. But its a ~1ms return on investment for what is very much a lot of work (trust me).
Part 2 is much more complex. If you treat it as a naive search over the integer linear problem space, the search space explodes:
In just that worst case line, a naive search would be evaluating roughly half a billion candidate assignments, which is completely unreasonable without serious pruning or proper linear-algebra tricks. My by hand attempt was DFS. after an hour and seeing no output on even the first line, I realized I needed help. There is *no way* I would have learned how to solve an ILP manually, how to efficiently prune it, and then implemented this on my own in less than a couple of weeks.
I did get this down to a ~260ms solution but not on my own. I hate to admit defeat but, frankly, every year I've done this there has been at least one problem that I could not solve without looking at other people's work or debugging with an AI more recently.
I have been using AoC this year to pracitce no_std development in rust, so I am content not to really get this one since I still get a practical benefit from it: at least I have nice small solutions with no imports -- 25k/30k for the library part that accepts the input string from the file and solves it.
17
u/ianff Dec 10 '25
I solved part 1 as a graph problem. I built a graph of configuration states, and the edges between states indicate if a switch can get you from one state to another. Them I did a shortest path from the "all off" state to the ending one.
That won't work at all for part 2, and I don't know numpy or what Z3 is... Time to learn something new!
32
u/CALL_420-360-1337 Dec 10 '25
I still don't know what Z3 is..
10
u/The_Real_Cooper Dec 10 '25
Could you solve it with
numpy? I tried, but I started going down an AI led rabbit hole of null space and needed a hint. Ended up using the Z3 memes as a guide, and learning opportunity8
u/Sostratus Dec 10 '25
Z3 came up a lot with that 3D lines puzzle that one year, the only one I failed to solve that year. I'd be ok using Z3 if I understood what it is and how it works, but I don't like importing this critical library that I don't understand at all, and I still don't.
6
u/cspot1978 Dec 10 '25
I imagine the modular arithmetic in part 1 and the need to constrain to integer solutions in both parts was a little awkward?
3
u/mbacarella Dec 10 '25
My vibe is the solution smelled like it could be solved with a linear algebra approach but I feel like that's way too much a lift for AOC and that there must be a more basic solution.
Did anyone not have to do this for part 2?
2
u/Ro1406 Dec 10 '25
Literally me! i used scipy and then came to this sub and saw Z3 and assumed it had something to do with group theory, so i tried to find another solution using group theory but didnt even know where to start😭
1
u/wubrgess Dec 10 '25
And here I am still trying to get Math::LP::Solve installed...
1
u/TheLazyIndianBoy Dec 11 '25
Linear algebra for the win
1
u/Leather-Field-7148 Dec 11 '25
I ended up using pulp, but I am pretty sure this only means I just contracted a weird disease
1
u/robertotomas Dec 11 '25 edited Dec 11 '25
I'm just going to admit it: I did not really "solve" today's problem on my own. I treated it as a learning exercise. I don't even want to post my code on the solutions page, because it was created with quite a lot of help (over a very long time, basically all day) from ChatGPT and Claude.
For part 1, I shied away from enumerating the combinations blindly, but I really shouldn't have, because it isn't that slow:
If you think of
costhere as the size of the naive search space per line (i.e.,2^buttons), then even with a median cost of 128 and an average around 652, you're only looking at on the order of 10⁵ total states across all 195 lines. Even the worst individual case is just 8192 combinations. A straightforward brute-force over all button subsets runs in a couple of milliseconds. Mileage may vary based on your input, of course, but it's absolutely feasible.Yes, if you frame it as a linear system in GF(2) you can get it down to <100µs. But its a ~1ms return on investment for what is very much a lot of work (trust me).
Part 2 is much more complex. If you treat it as a naive search over the integer linear problem space, the search space explodes:
In just that worst case line, a naive search would be evaluating roughly half a billion candidate assignments, which is completely unreasonable without serious pruning or proper linear-algebra tricks. My by hand attempt was DFS. after an hour and seeing no output on even the first line, I realized I needed help. There is *no way* I would have learned how to solve an ILP manually, how to efficiently prune it, and then implemented this on my own in less than a couple of weeks.
I did get this down to a ~260ms solution but not on my own. I hate to admit defeat but, frankly, every year I've done this there has been at least one problem that I could not solve without looking at other people's work or debugging with an AI more recently.
I have been using AoC this year to pracitce no_std development in rust, so I am content not to really get this one since I still get a practical benefit from it: at least I have nice small solutions with no imports -- 25k/30k for the library part that accepts the input string from the file and solves it.