Comment by sirwhinesalot

A SAT solver without any preprocessing won't be competitive with SoTA SAT solver.

CDCL is core to the problem, but it is not sufficient. You even have SAT solvers like CryptoMiniSAT that try to detect clauses that encode xor gates so they can use Gaussian Elimination.

This is also true of ILP solvers. Simplex + Branch & Cut is elegant. But that's not how you get to the top.