SC Chapter 5 SMT Solving
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 5 SMT Solving
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 5 SMT Solving
Kartei Details
| Karten | 35 |
|---|---|
| Sprache | English |
| Kategorie | Informatik |
| Stufe | Universität |
| Erstellt / Aktualisiert | 18.02.2017 / 27.02.2017 |
| Lizenzierung | Keine Angabe |
| Weblink |
https://card2brain.ch/box/20170218_sc_chapter_5_smt_solving
|
| Einbinden |
<iframe src="https://card2brain.ch/box/20170218_sc_chapter_5_smt_solving/embed" width="780" height="150" scrolling="no" frameborder="0"></iframe>
|
What is the definition of SMT Solving?
Expand propositional logic with theories extending SAT to SAT-modulo-theories (SMT)
What is provided by the SMT community? [3]
1. SMT-LIB exists with language benchmarks tutorials
2. SMT-COMP exists with measuring performance and capabilities of tools
3. SMT workshops are held annually
What is the idea behind the eager approach of SMT? [2]
1. First theory and then SAT solver
2. Transformation of all NP-complete problems with polynomial effort to equivalent SAT problems // Not always most effective
What is the idea behind the full lazy approach of SMT?
First SAT solver and then theory
What are current implementations? [10]
1. UCLID
2. STP
3. Spear
4. Boolector
5. Beaver
6. SONOLAR
7. SWORD
8. CVC3
9. MathSAT
10. Z3
What is the definition of equality logic with uninterpreted functions? [6]
1. Propositional with equalities (P) and uninterpreted functions (F)
2. Both are NP-complete thus they model same decision problems
3. Input in NNF
4. Formula of propositional logic is phi^B
5. Formula with equalities is phi^E
6. Formula with equalities and uninterpreted functions is phi^UF
What is the effort of the removing constants algorithm in SMT?
Algorithm for phiUF in polynomial time
What is the idea of reducing phiUF to phiE? [2]
1. Replace f(a) by xf(a)
2. Assume that for all a,b in Dn that f(a)!=f(b) → a!=b
