# Differences

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

 sav08:idea_of_quantifier-free_combination [2008/04/24 14:08]vkuncak sav08:idea_of_quantifier-free_combination [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/05/13 10:37 vkuncak 2008/04/24 14:08 vkuncak 2008/04/24 13:50 vkuncak 2008/04/23 15:41 vkuncak 2008/04/23 10:13 vkuncak created Next revision Previous revision 2009/05/13 10:37 vkuncak 2008/04/24 14:08 vkuncak 2008/04/24 13:50 vkuncak 2008/04/23 15:41 vkuncak 2008/04/23 10:13 vkuncak created 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.