SAT appears to be rather impervious to statistical methods because it is very non-linear and non-local (besides, of course, being NP-complete). Flip one single literal anywhere and poof!, your formula mght go from SAT to UNSAT, or vice versa, or you might enable a ton of simplifications, etc. So it might be very hard to train a network on such a riotous state space.

Additionally, in practice SAT solvers are also supposed to provide witnesses (i.e., a satisfying assignment or an unsatisfiability core) to back their verdicts, and that may be an ever taller order for ML.