# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision Next revision | Previous revision | ||

sav08:idea_of_quantifier-free_combination [2008/04/24 14:08] vkuncak |
sav08:idea_of_quantifier-free_combination [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 1: | Line 1: | ||

====== Idea of Quantifier-Free Combination ====== | ====== Idea of Quantifier-Free Combination ====== | ||

- | We wish to reason about quantifier-free formulas that contain different symbols, such as | + | We know of several classes of formulas that we can decide: |

* ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) - congruence closure | * ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) - congruence closure | ||

+ | * $f(f(f(f(a)))) \neq a \land f(f(a))=a$ | ||

* term algebras (interpreted over Herbrand model) - unification | * term algebras (interpreted over Herbrand model) - unification | ||

+ | * $cons(a,b)=cons(c,d) \land a \neq c$ | ||

* real linear arithmetic - linear programming such as Simplex | * real linear arithmetic - linear programming such as Simplex | ||

+ | * $x < y \land y < x + 1$ | ||

* integer linear arithmetic - integer linear programming (branch and bound, branch and cut), reduction to SAT | * integer linear arithmetic - integer linear programming (branch and bound, branch and cut), reduction to SAT | ||

+ | * $x < y \land y < x + 1$ | ||

- | We would like to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately. | + | We wish to reason about quantifier-free formulas that contain all these different symbols in the same formula. |

- | We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. We therefore consider conjunctions of literals. | + | The idea is to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately. |

- | Consider a conjunction of literals $C$. If we can group literals into blocks, $C \leftrightarrow C_1 \land \ldots \land C_n$ and | + | We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. |

- | * if one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable | + | \begin{equation*} |

+ | F \ \ \leftrightarrow \ \ \bigvee_{i=1}^n C_i | ||

+ | \end{equation*} | ||

+ | We therefore consider conjunctions of literals $C_i$. | ||

+ | | ||

+ | Consider a conjunction of literals $C$. If we can group literals into blocks | ||

+ | \begin{equation*} | ||

+ | C \leftrightarrow C_1 \land \ldots \land C_n | ||

+ | \end{equation*} | ||

+ | If one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable. | ||

The idea is to separate conjuncts into those specific to individual theories, and then solve each $C_i$ using a specialized decision procedure $P_i$ | The idea is to separate conjuncts into those specific to individual theories, and then solve each $C_i$ using a specialized decision procedure $P_i$ | ||

- | An important question is completeness: if each $C_i$ is satisfiable, is $C_1 \land \ldots \land C_n$ satisfiable? We will show that, under certain conditions, this holds. | + | An important question is **completeness**: if each $C_i$ is satisfiable, is $C_1 \land \ldots \land C_n$ satisfiable? We will show that, under certain conditions, this holds. |