It probably really depends what sort of problem you're working on, but in my experience it was easier to represent things as mixed integer linear programming, (

It probably really depends what sort of problem you're working on, but in my experience it was easier to represent things as mixed integer linear programming, (MIP) rather than a SAT instance. They're both NP-complete representations, but with the MIP representation you can naturally add constraints like "maximize the sum of these various things" as well as the sort of boolean constraints that work naturally with SAT. And for MIP solving, the Python mip package is quite convenient. https://python-mip.readthedocs.io/en/latest/quickstart.html https://python-mip.readthedocs.io/en/latest/quickstart.html