z3 or constraint programming comes in very handy in at least one challenge every year in Advent of Code! https://adventofcode.com