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.

[1] https://en.wikipedia.org/wiki/Answer_set_programming

[2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfi...