[zero_k]

SAT solvers are used _everywhere_. Your local public transport is likely scheduled with it. International trains are scheduled with it. Industrial automation is scheduled with it. Your parcel is likely not only scheduled with it, but even its placement on the ship is likely optimised with it. Hell, it's even used in the deep depths of cryptocurrencies, where the most optimal block composition is computed with it. Even your friendly local nuclear reactor may have had its failure probability computed with (a variation of) it. In other words, it's being used to make your life cheaper/better/safer/easier. Google a bit around, open your eyes Neo ;)

PS: Yes, I develop a propositional SAT solver that used to be SOTA [1]. I nowadays develop a propositional model counter (for computing probabilities), that is currently SOTA [2]

[1] https://github.com/msoos/cryptominisat/ [2] https://github.com/meelgroup/ganak/

[taeric]

I confess I would expect a lot of those would be linear programming more than sat? Mixed integer would not surprise me.

[fulafel]

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?

[JonChesterfield]

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.

[eru]

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.