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 [2009/05/06 09:25] vkuncak |
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:45] vkuncak |
||
---|---|---|---|
Line 17: | Line 17: | ||
===== SMT Prover Architecture ===== | ===== SMT Prover Architecture ===== | ||
- | Two layers: | + | 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 ([[sav09:Lecture 08a]]) | * SAT solver to 'enumerate' conjunctions of disjunctive normal form ([[sav09:Lecture 08a]]) | ||
Line 36: | Line 36: | ||
\end{array} | \end{array} | ||
\] | \] | ||
+ | Is this formula satisfiable? ++|No. Why?++ |