LARA

Differences

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

Link to this comparison view

sav08:idea_of_quantifier-free_combination [2008/04/24 14:08]
vkuncak
sav08:idea_of_quantifier-free_combination [2015/04/21 17:30]
Line 1: Line 1:
-====== Idea of Quantifier-Free Combination ====== 
- 
-We wish to reason about quantifier-free formulas that contain different symbols, such as 
-  * ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) - congruence closure 
-  * term algebras (interpreted over Herbrand model) - unification 
-  * real linear arithmetic - linear programming such as Simplex 
-  * integer linear arithmetic - integer linear programming (branch and bound, branch and cut), reduction to SAT 
- 
-We would like to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately. 
- 
-We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. ​ We therefore consider conjunctions of literals. 
- 
-Consider a conjunction of literals $C$.  If we can group literals into blocks, $C \leftrightarrow C_1 \land \ldots \land C_n$ and 
-  * 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.