Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:eager_sat_encoding [2012/05/21 10:57]
vkuncak
sav08:eager_sat_encoding [2012/05/21 10:57] (current)
vkuncak
Line 3: Line 3:
 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. 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*+  * Ackermann'​s encoding
  
   * [[sav08:​small_solutions_for_quantifier-free_presburger_arithmetic|Small Solutions for PA]]   * [[sav08:​small_solutions_for_quantifier-free_presburger_arithmetic|Small Solutions for PA]]
 
sav08/eager_sat_encoding.txt · Last modified: 2012/05/21 10:57 by vkuncak
 
© EPFL 2018 - Legal notice