[sirwhinesalot]

SAT solvers are rarely used directly, they're usually a core component of a more expressive solver type like an LCG solver or an SMT solver.

And if not that, then they are used as the core component of a custom solver that speaks some higher level domain language.

Encoding things in CNF is a pain (even with higher level APIs like PySAT). But it's not usually something you should be doing unless you are developing a solver of some sort yourself.