Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:idea_of_quantifier-free_combination [2009/05/13 10:37] vkuncak |
sav08:idea_of_quantifier-free_combination [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 16: | Line 16: | ||
| We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. | We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. | ||
| - | \[ | + | \begin{equation*} |
| F \ \ \leftrightarrow \ \ \bigvee_{i=1}^n C_i | F \ \ \leftrightarrow \ \ \bigvee_{i=1}^n C_i | ||
| - | \] | + | \end{equation*} |
| We therefore consider conjunctions of literals $C_i$. | We therefore consider conjunctions of literals $C_i$. | ||
| Consider a conjunction of literals $C$. If we can group literals into blocks | Consider a conjunction of literals $C$. If we can group literals into blocks | ||
| - | \[ | + | \begin{equation*} |
| C \leftrightarrow C_1 \land \ldots \land C_n | C \leftrightarrow C_1 \land \ldots \land C_n | ||
| - | \] | + | \end{equation*} |
| If one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable. | If one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable. | ||