1. A method implemented by a computing device, the method comprising: receiving a formula in order to determine a satisfiability of the formula; propagating truth assignments to atomic constraints of the formula by applying a Davis Putnam Longman Loveland (DPLL)-based technique; eliminating conjunctions associated with the formula; representing the formula by disjunctions and negations based in part on the eliminating of the conjunctions; tracking which truth assignments are relevant for determining satisfiability of the formula based in part on emulating a Tableau solving technique using the disjunctions and the negations; and propagating the truth assignments of only the relevant atomic constraints to a theory solver.