I just completed all 12 days of Advent of Code 2025! #AdventOfCode https://adventofcode.com/ Now that my solution to Day 12 that needed 75h of compute is done and I can go see what the clever DP solution was
Advent of Code 2025

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.

AdventOfCode2025/Day12/Day12-clean.ipynb at main · johnpmay/AdventOfCode2025

Contribute to johnpmay/AdventOfCode2025 development by creating an account on GitHub.

GitHub
@3j0hn you'll be shocked :>
@leah Angry even - I had the stupid "solution" coded and didn't even try it before building this monstrosity in Pulp
@3j0hn oh no :(
@leah "it can't possibly be that easy" famous last words
@leah I would feel worse if there were a DP or other incremental or recursive solution that I missed.

@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.

@jeff Yeah, I kept trying to think of clever ways to find packing, but I knew that SAT was going to be the only way to prove impossibility - which should have been a clue as you say. SAT often solves AoC problems, but it's never the only way to do them