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 | ||
|
sav07_lecture_5_skeleton [2007/03/28 10:51] vkuncak |
sav07_lecture_5_skeleton [2007/03/28 11:08] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Lecture 5 Skeleton ====== | ====== Lecture 5 Skeleton ====== | ||
| - | + | Two important techniques: | |
| - | + | * Nelson-Oppen combination method | |
| - | + | * Resolution | |
| ===== Basic idea of Nelson-Oppen combination ===== | ===== Basic idea of Nelson-Oppen combination ===== | ||
| Line 45: | Line 44: | ||
| * the same number of nodes | * the same number of nodes | ||
| * same properties on shared symbols (equality and sometimes more) | * same properties on shared symbols (equality and sometimes more) | ||
| + | |||
| + | Lazy approach to integrating solvers for conjunctions and SAT solvers | ||
| ==== General case ==== | ==== General case ==== | ||