@pavel Thinking about it a bit more, the first time I wanted a serious solver was when I messed with storing programs on an arm microcontroller with special alignment requirements.
That was awkward to code in Python, so I replaced the entire thing with Z3 and added my adjustments.
I think we as an industry underutilize general solvers and I want to check this hypothesis with the Prolog experiment.