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:
- 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
Generalization when sharing more than equalities: