Instead of combining DPLL SAT solver search with decision procedures for conjunctions, for several theories it is possible to encode the entire problem into a propositional formula and then just give it to a SAT solver.

• Ackermann's encoding

• Small Solutions for PA

Some systems based on this approach:

• STP
• UCLID
• Decision Procedures book by Daniel Kroening and Ofer Strichman

Note: as we mentioned the combination is often in NPTIME, so encoding into SAT often exists

• when this is efficient depends on the class of problems
• encoding into SAT can be simpler
• some results

Generalization when sharing more than equalities:

• On Combining Theories with Shared Set Operations