LARA

This is an old revision of the document!


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: