[xavxav]

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?

[Karrot_Kream]

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.

[xavxav]

Oh right this is just Horn clauses, not CHCs

[thomasahle]

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