Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:introductory_remarks_on_smt_provers [2008/04/17 11:37] vkuncak |
sav08:introductory_remarks_on_smt_provers [2009/05/06 00:24] vkuncak |
||
---|---|---|---|
Line 18: | Line 18: | ||
Two layers: | Two layers: | ||
* fast solving of quantifier-free formulas (see [[http://citeseer.ist.psu.edu/671087.html|DPLL(T) paper]]) | * fast solving of quantifier-free formulas (see [[http://citeseer.ist.psu.edu/671087.html|DPLL(T) paper]]) | ||
- | * SAT solver to 'enumerate' conjunctions of disjunctive normal form | + | * SAT solver to 'enumerate' conjunctions of disjunctive normal form ([[sav09:Lecture 08a]]) |
* **specialized algorithms for quantifier-free formulas** - this is what we will talk about today | * **specialized algorithms for quantifier-free formulas** - this is what we will talk about today | ||
* heuristic quantifier instantiation (instantiation rule) | * heuristic quantifier instantiation (instantiation rule) |