Lab for Automated Reasoning and Analysis 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 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.
  
 
sav08/idea_of_quantifier-free_combination.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice