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:idea_of_quantifier-free_combination [2008/04/24 13:50] vkuncak |
sav08:idea_of_quantifier-free_combination [2008/04/24 14:08] vkuncak |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| We wish to reason about quantifier-free formulas that contain different symbols, such as | We wish to reason about quantifier-free formulas that contain different symbols, such as | ||
| - | * ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) | + | * ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) - congruence closure |
| - | * term algebras (interpreted over Herbrand model) | + | * term algebras (interpreted over Herbrand model) - unification |
| - | * integer linear arithmetic | + | * real linear arithmetic - linear programming such as Simplex |
| - | * real linear arithmetic | + | * integer linear arithmetic - integer linear programming (branch and bound, branch and cut), reduction to SAT |
| - | For this, we would like to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately. | + | We would like to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately. |
| - | Note that we are checking satisfiability, and $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. We therefore consider conjunctions of literals. | + | We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. We therefore consider conjunctions of literals. |
| - | Consider a conjunction of literlas $C$. If we can represent it as separate conjunction $C_1$,...,$C_n$ then | + | Consider a conjunction of literals $C$. If we can group literals into blocks, $C \leftrightarrow C_1 \land \ldots \land C_n$ and |
| * if one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable | * if one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable | ||