Garden of Learning

Advent of Code 2025: Day 10

(modified: )7 min read

Spoiler alert

This is a full solution for Advent of Code 2025, day 10 puzzles with explanations.

If you want to try to solve it yourself first, head over to https://adventofcode.com/2025/day/10 and give it a go and then come back and compare notes.

You can find the full code at https://github.com/Hamatti/adventofcode-2025/blob/main/src/day_10.py

We are almost at the end already. We can see the 12th right around the corner and I’m feeling great about this year’s Advent of Code.

On the third day, we’re treated to an interesting puzzle where a dog ate the homework instructions and it’s up to us to figure it out.

Read input

We have a three part input:

  • Indicator lights’ target state within square brackets []
  • Buttons in parentheses ()
  • Joltage information in curly braces {}
[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2}
[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5}

The mapper function is the most complex we’ve seen so far this year:

LIGHTS_PATTERN = r"\[(.*)\]"
BUTTON_PATTERN = r"\(.*\)"
JOLTAGE_PATTERN = r"\{.*\}"
 
Machine = namedtuple("Machine", ["lights", "buttons", "joltage"])
 
def mapper(line: str) -> Machine:
    lights_binary: str = (
        re.match(LIGHTS_PATTERN, line).groups()[0].replace("#", "1").replace(".", "0")
    )
    buttons: List[str] = re.findall(BUTTON_PATTERN, line)[0].split(" ")
    buttons: List[str] = [
        btn.replace("(", "").replace(")", "").split(",") for btn in buttons
    ]
    joltage: List[int] = [
        int(num)
        for num in re.findall(JOLTAGE_PATTERN, line)[0]
        .replace("{", "")
        .replace("}", "")
        .split(",")
    ]
 
    buttons_binaries = []
    for button in buttons:
        button_binary = ""
        for i in range(len(lights_binary)):
            button_binary += "1" if str(i) in button else "0"
        buttons_binaries.append(button_binary)
 
    return Machine(int(lights_binary, 2), buttons_binaries, joltage)

There’s a lot of parsing and converting things but here’s the key things:

I figured that if I represent the lights and the buttons as binary numbers (where 1 is on and 0 is off), I can use bitwise XOR to simulate a button press without having to loop.

When reading the first section of the input, the lights, I convert # to 1 and . to 0. I can then convert this binary string presentation to an integer with int(binary_str, 2) where 2 refers to binary.

I then do the same for the buttons: I turn the indexed spots to 1 and unindexed ones to 0 and store them as binary representation in our data.

Part 1

In the first part, we need to figure out what’s the shortest amount of button presses on each machine that will turn the lights into its target state.

def part_1() -> int:
    machines = read_input(10, mapper)
    all_presses = 0
 
    for machine in machines:
        target = machine.lights
        presses = 1
        stop = False
        while not stop:
            possible_presses = combinations(
                machine.buttons, presses
            )
 
            for button_presses in possible_presses:
                current_lights = 0
                for _press in button_presses:
                    current_lights ^= int(_press, 2)
                if current_lights == target:
                    all_presses += presses
                    stop = True
                    break
            presses += 1
 
    return all_presses

For each machine, I start with 1 press and go through all one-press combinations. If any of them makes the lights match the target state, we record 1 to our full count and break out. If none of them work, we move on to 2-press combos and so on until we find one.

In Python, we can bitwise XOR two numbers with number1 ^ number2.

I was initially worried about how to find the smallest amount but then realised that I can start from 1 press and move to bigger amounts.

Addendum A: No need for multiple presses of same button

While I was writing this, I realised that you don’t actually need to include multiples of the same button press. A A XOR A is always 0 as it cancels itself out. So I changed from itertools.combinations_with_replacement with itertools.combinations to narrow down the problem space.

Part 2

Not gonna do this today. Maybe later.

Later is here! After solving day 11, I had some extra time at my hand while waiting for our AoC jam session to start, I took a new look at part 2.

I’ll be honest here: I did not come up with this solution. I heard a lot of talk about “ILP”s and “z3” in my communities and decided to pick z3 and try to make sense out of it.

I started by modifying the Machine by adding the raw button input:

Machine = namedtuple("Machine", ["lights", "buttons", "button_raw", "joltage"])

Then I installed Z3Py using Single-file executable Python scripts with uv format to include the dependency in the file so it gets installed with uv when I run the script. That way, I don’t need to deal with manually setting up virtual environments, installing packages and all that. I can simply put it there and run the file as normal. Brilliant concept.

Z3Py is a “theorem prover” but that doesn’t mean a ton to me. I have very vague idea what that means. But people in the interwebs told me that’s what we need today.

Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.

If I’m understanding things correctly, we’re using it for constraint solving today. But don’t quote me on that.

# /// script
# requires-python = ">=3.10"
# dependencies = [
#    "z3-solver",
# ]
# ///
 
import z3
 
def part_2() -> int:
    machines = read_input(10, mapper)
    min_number_of_presses = 0
    for machine in machines:
        optimizer = z3.Optimize()
        presses = [z3.Int(f"push-button-{idx}") for idx in range(len(machine.button_raw))]
 
        for idx, _ in enumerate(machine.button_raw):
            optimizer.add(presses[idx] >= 0)
        for idx, _ in enumerate(machine.joltage):
            optimizer.add(
                sum(presses[j] for j, btn in enumerate(machine.button_raw) if str(idx) in btn)
                == machine.joltage[idx]
            )
 
        optimizer.minimize(sum(presses))
        assert optimizer.check() == z3.sat
 
        model = optimizer.model()
        for press in presses:
            min_number_of_presses += model[press].as_long()
 
    return min_number_of_presses

We initialise an optimizer, that

provides methods for solving using objective functions and weighted soft constraints

We then create N integer constants where N is the amount of buttons our machine has. For each of the buttons, we then add a optimisation asserts that we want the amount for each button press to be 0 or more. I’m assuming that keeps it from trying to optimise for negative button presses.

For each joltage value, we add another assert that says that the sum of those presses needs to match the end result for each of the joltage bits.

We then ask z3 to do the magic for us by minimizing the sum of those presses.

z3.sat is a “satisfiability check” variable that says the optimizer did its job well and it satisfies our constraints.

And then the model is a representation of that so we can get the actual numbers out and count them!

Yay for a star.

Not in a million years would I have found this concept or the right tools if it wasn’t for people who know what they are talking about. I’m quite happy that I was able to somewhat understand how it works by reading through the docs and source code of z3.

And now you know it exists too!

Get in touch

If you want to comment on these solutions, I share them in Mastodon where you can look for the post for the right date or you can start a discussion over email with juhamattisantala@gmail.com.

Follow via RSS

I have created a custom RSS feed for these solutions so you can follow along and not miss any of them!

Recent Notes

Backlinks

Recent Notes