Differences
This shows you the differences between two versions of the page.
|
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:45] vkuncak |
sav08:introductory_remarks_on_smt_provers [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Introductory Remarks on SMT Provers ====== | ||
| - | We next study techniques that help understand how modern SMT (satisfiability modulo-theories) provers work. | ||
| - | |||
| - | Meaning of name (recent): | ||
| - | * satisfiability: check satisfiability of formulas (to check validity, check satisfiability of negation) | ||
| - | * modulo theories: built-in support for arithmetic, arrays, algebraic data types | ||
| - | |||
| - | Example provers: | ||
| - | * [[http://doi.acm.org/10.1145/1066100.1066102|Simplify theorem prover]] (was very influential) | ||
| - | * [[http://www.springerlink.com/content/r6d4navlp2aw1q02|An Explicating Theorem Prover for Quantified Formulas]] | ||
| - | * [[http://research.microsoft.com/projects/Z3/|Z3]] | ||
| - | * [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] | ||
| - | * [[http://people.csail.mit.edu/vganesh/stp.html|STP]] | ||
| - | * [[http://code.google.com/p/opensmt/|OpenSMT]] | ||
| - | |||
| - | ===== SMT Prover Architecture ===== | ||
| - | |||
| - | Layers: | ||
| - | * 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]]) | ||
| - | * **specialized algorithms for quantifier-free formulas** - this is what we will talk about today | ||
| - | * heuristic quantifier instantiation (instantiation rule) | ||
| - | |||
| - | |||
| - | Note: formulas that are valid in the combination of quantifiers, linear integers, and uninterpreted functions are not enumerable (and neither are formulas that are not valid). The situation is worse than in pure first-order logic. | ||
| - | |||
| - | ===== Example ===== | ||
| - | |||
| - | Consider the following formula, where $f$ denotes functions from integers to integers and $a,b$ are integers. | ||
| - | \[\begin{array}{l} | ||
| - | (\forall x.\forall y.\ x \le y \rightarrow f(x) \le f(y))\ \land \\ | ||
| - | (\forall x.\forall y. f(x)=f(y) \rightarrow x=y)\ \land\\ | ||
| - | 2 f(a) \le 2f(b)+1\ \land\\ | ||
| - | b < a | ||
| - | \end{array} | ||
| - | \] | ||
| - | Is this formula satisfiable? ++|No. Why?++ | ||