I know from Schaefer's Dichotomy Theorem that only a few types of satisfiability problems are in P and any other problem is NP-complete. However, all of the algorithms I know for them use specific techniques unique to that type of problem- e.g. unit propagation for Hornsat, linear algebraic techniques mod 2 for XORSAT, and various other techniques for 2-sat. Is there one general polytime algorithm which works for all of these problems in P? Thanks.
Schaefer's dichotomy theorem is proved by dividing CSPs into two types: those that can be reduced to one of a few specific problems in P, and the other to which SAT can be reduced (and so are NP-complete). Specifically, every CSP of the former type is either trivial (always satisfied by the constant 0 or the constant 1 assignment), can be reduced to 2SAT, can be reduced to HORN-SAT, or can be reduced to XOR-SAT. These are the only algorithms you need to solve these CSPs. There is no one single algorithm – there is a finite list of algorithms.
Look for papers/books written by Vijay Chandru, John Hooker and John Franco. Some of their techniques use Integer Programming (looking at special structures in the matrix generated by the CNF clauses of the SAT instance). The "extended Horn" formulas have a special structure when represented as graphs which make them polynomially solvable.
To quote Franco from his 2009 survey: The reader may have the impression that the number of polynomial time solvable classes is quite small due to the famous dichotomy theorem of Schaefer. But this is not the case. Schaefer proposed a scheme for defining classes of propositional expressions with a generalized notion of “clause.” He proved that every class definable within his scheme was either NP-complete or polynomial-time solvable, and he gave criteria to determine which. But not all classes can be defined within his scheme. The Horn and XOR classes can be, but we will describe several others including q-Horn, extended Horn, CC-balanced and SLUR that cannot be so defined. The reason is that Schaefer’s scheme is limited to classes that can be recognized in log space.