Are there open source examples of usage for real world problems, for example train scheduling or something else than software engineering practicioners might find relatable?
Register allocation, instruction selection and instruction scheduling can, with a degree of bloodyminded patience, all be solved with boolean SAT. That's a compiler backend.
I like the higher level CSP more as an interface but those are _probably_ best solved by compilation to SAT. SMT also worth a look.
When I used to work at Deutsche Bahn, the German railway operator, in the mid 2000s as a research student, we were using Mixed Integer Linear Programming.
