UUGH I hate the thought of dealing with SAT directly. Maybe writing my own wrapper would be fun, but it doesn't get me where I want this project to go.

https://github.com/python-constraint/python-constraint -- maybe more friendly, https://labix.org/python-constraint Can write constraints as Python functions. But this suggests it may be slower.

https://pypi.org/project/docplex/ -- just a front-end to CPLEX