LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:idea_of_quantifier-free_combination [2008/04/24 13:50]
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) +  * ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) ​- congruence closure 
-  * term algebras (interpreted over Herbrand model) +    * $f(f(f(f(a)))) \neq a \land f(f(a))=a$ 
-  * integer ​linear arithmetic +  * term algebras (interpreted over Herbrand model) ​- unification 
-  * real linear arithmetic+    * $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$
  
-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 wish to reason about quantifier-free ​formulas ​that contain all these different symbols in the same formula.
  
-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.+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 literlas ​$C$.  If we can represent it as separate conjunction $C_1$,...,$C_n$ then +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.