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.