Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:combining_fol_models [2009/05/13 00:09] vkuncak |
sav08:combining_fol_models [2009/05/13 10:21] vkuncak |
||
---|---|---|---|
Line 89: | Line 89: | ||
* [[http://research.microsoft.com/projects/z3/smt07.pdf|Model-based Theory Combination]], Leonardo de Moura and Nikolaj Bjørner, Workshop on Satisfiability Modulo Theories (SMT), Berlin, Germany, 2007. | * [[http://research.microsoft.com/projects/z3/smt07.pdf|Model-based Theory Combination]], Leonardo de Moura and Nikolaj Bjørner, Workshop on Satisfiability Modulo Theories (SMT), Berlin, Germany, 2007. | ||
+ | ===== Complexity ===== | ||
+ | |||
+ | * if each theory is convex and polynomial time (e.g. congruence closure + real linear arithmetic), then conjunctions can be decided in PTIME | ||
+ | * if each theory is NP (e.g. we also allow integer linear programming), then (even for non-convex theories), any quantifier-free combination is in NP | ||
===== Theories with Non-Disjoint Languages ===== | ===== Theories with Non-Disjoint Languages ===== | ||
Line 103: | Line 107: | ||
Alternative method: | Alternative method: | ||
* [[http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.html|On Combining Theories with Shared Set Operations]] | * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.html|On Combining Theories with Shared Set Operations]] | ||
- | |||
- | ===== Complexity ===== | ||
- | |||
- | * if each theory is convex and polynomial time (e.g. congruence closure + real linear arithmetic), then conjunctions can be decided in PTIME | ||
- | * if each theory is NP (e.g. we also allow integer linear programming), then (even for non-convex theories), any quantifier-free combination is in NP | ||
===== References ===== | ===== References ===== |