> Does this mean that rustc should integrate an industrial-strength SAT solver?

Well, this is actually what https://github.com/rust-lang/rfcs/blob/master/text/1868-port... would require. There is already chalk, a logic programming language for traits too.

I don't balk at these things. A good logical / relational toolbox is very useful for a lot of tasks.