Lab for Automated Reasoning and Analysis LARA

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:

 
sav08/eager_sat_encoding.txt · Last modified: 2012/05/21 10:57 by vkuncak
 
© EPFL 2018 - Legal notice