Not sure if related, to Schaefer's theorem, but I dove into Answer Set Programming [1] recently, which follows this approach, enabling the use of fast-ish SMT solvers, which are a generalization of SAT solvers! Boolean/Propositional Logic is to Predicate Logic as SAT is to SMT. There's a very nice course about it from the developers of Potassco, one of the best open source Answer Set Programming framework [2].
The syntax looks like Prolog, but predicate negations are a first class citizen, avoids infinite loops.
Prolog's approach is like a depth first search through a search tree -- ASP is like a nondeterministic turing machine, exploring all branches simultaneously from the bottom up.
Schaefer's dichotomy theorem shows that, when possible, just make sure to use Horn clauses when possible.
Takes a bit of thinking but is superior to huristics or SAT solvers if you can refactor to allow for it.