Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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