If the concern is regarding real-world performance and not DoS attacks, then why can't they just adopt the conflict-driven clause learning techniques of practic

If the concern is regarding real-world performance and not DoS attacks, then why can't they just adopt the conflict-driven clause learning techniques of practical SAT solvers? The corresponding SAT instances are quite small, so the problems should be handled quickly by even a relatively naive CDCL implementation.