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)
@@ Line 1: / Line 1: @@
 ====== 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
+    * $f(f(f(f(a)))) \neq a \land f(f(a))=a$
   * 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
+    * $x < y \land y < x + 1$
   * 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$
-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.