I often think of SAT as the assembly language of discrete optimization.

I specify my problems in a higher-level DSL and a library then "compiles" it to SAT, where many solvers are available.