Yes, the idea of using SAT/SMT for solving/helping AI tasks is far from mainstream. But I was wondering if there is a potential, if so for what tasks?

I said on another comment that I work on a logic checker for English, detecting automatically logical fallacies from text. I consider such a task to be AI and how could SAT help to check if the conclusion of a syllogism follow?

"Internally we use SAT solvers to schedule resources on medical devices" this is cool!