# Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

### Resolution – Properties of Clausal Forms

(1)
**
**
If
*
l
*
appears in some clause of
*
S
*
, but
*
l
*
*
^{c}
*
does not appear in any clause, then, if we delete all clauses in

*S*containing

*l*, the new clausal form

*S'*is satisfiable if and only if

*S*is satisfiable

Example: Satisfiability of is equivalent to satisfiability of

(2) Suppose
*
C
*
= {
*
l
*
} is a unit clause and we obtain
*
S'
*
from
*
S
*
by deleting
*
C
*
and
*
l
*
*
^{c}
*
from all clauses that contain it; then,

*S*is satisfiable if and only if

*S'*is satisfiable

Example: is satisfiable iff is satisfiable

**Speaker notes:**