Wait, this is very relevant to some work I’ve been doing recently, how do you conclude that Horn clauses should be preferred from Schaefer’s theorem?

Isn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.

Take a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem... (based on Schaefer's "The complexity of satisfiability problems"). Horn clause satisfiability problems (HORN SAT) fall in P-c.

Oh right this is just Horn clauses, not CHCs

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...