Eager SAT Encoding

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

Some systems based on this approach:

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

Generalization when sharing more than equalities: