From KSAT to delayed theory combination: exploiting DPLL outside the SAT domain