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
