I am quite proud of having figured out a clean SAT formulation of this problem that could be solved using common optimization packages in python. Here's my cleaned up code for solving with PuLP/CBC (comment out the triviality check at the top to force solving using pulp - like I did on the weekend 😅 ).

https://github.com/johnpmay/AdventOfCode2025/blob/main/Day12/Day12-clean.ipynb

Tips welcome from any optimization gurus with more experience with Z3 / PuLP / ORtools for how this might be made better.

@3j0hn Yeah, I cleaned the list that way in minutes and then spent hours on my backtrack solver and visualizations for combining shapes using Minkowski/etc.

Finding any solution was easy. Proving _impossible_ scenarios like the test case should have been the obvious clue; but I was too deep down the rabbit hole by then.

I just completed all 12 days of Advent of Code 2025!

https://adventofcode.com/

#AdventOfCode

I've completed "Christmas Tree Farm" - Day 12 - Advent of Code 2025

I was _deeply_ unsatisfied with this solution, so I've been turning it into a game and working on an actual solver instead.

https://github.com/jstanden/advent-of-code-python/blob/main/2025/day12.ipynb

#AdventOfCode #Python #Programming

Also, a shoutout and high‑five to a few fellow Mastodons who posted incredible stuff, interacted with me, or are just plain awesome:

@jochie @movq @alrj
@tipiak75 @RogerBW @jeff @everythingalsocan @psf @papajohn
@sol_hsa @mina @Tipa @psychotimmy
@teotwaki @mnvr

Thanks, #AdventOfCode was just so much more fun with you guys 😊.

@JesseSkinner Thanks! I haven't tried to write a linear solver yet, but it would be a fun challenge after AoC.

I always go straight for z3 and have a better appreciation for what it's doing now.

For Day 11's penance for using networkx, I'll probably implement topological sort with BFS. 😅

As penance for using Z3 on Day 10 Part 2, I wrote down some notes and worked examples for linear Diophantine equations and Gaussian Elimination with matrices.

This comes up every year and I never remember it.

I worked a few examples from my Day 10 input.

https://github.com/jstanden/advent-of-code-python/blob/main/2025/journals/diophantine-equations.ipynb

#AdventOfCode #math

@tomlawrence I think it would have been FAR more interesting if the button/counter inputs were intentionally square (same length) and full rank (distinct button effects w/o dupes or linear combos), so linear algebra was possible and we'd possibly learn something about matrix math.

Those solutions could even be done by hand.

@p4bl0 I had the same issue trying to adapt my Part 1 BFS for it, because we switched from XOR to counters. The math approach is instant but less satisfying.

I've completed "Reactor" - Day 11 - Advent of Code 2025

I spent a while severing bottleneck edges in Part 2 before remembering the trick to past problems like this. The result is a couple lines and ~30ms.

https://github.com/jstanden/advent-of-code-python/blob/main/2025/day11.ipynb

#AdventOfCode #Python #Programming

@adw99 Z3's docs + Wikipedia are unnecessarily intimidating because of the SMTLIB syntax.

This is a much better introduction to the Python bindings: https://ericpony.github.io/z3py-tutorial/guide-examples.htm

@brass75 It's possible to BFS Part 1 in reasonable time (and more fun), but I used Z3 on Part 2 also.

Someone mentioned Diophantine equations last time, but I haven't internalized that yet.

Python's namedtuples apparently have major overhead. I replaced my BFS queue state for Day 10 Part 1 with tuples and the runtime dropped from 45s to 14s.

I'm sure I can optimize it further with just math, but the solution is only ~7 lines of code.

#AdventOfCode #Python #Programming