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!