Resolution Strategies ...
- unit preference: Clauses are prioritized, with unit clauses
(those with only one literal) preferred, or more generally, shorter clauses
preferred. Our goal is to reach □, which has zero literals and is
only obtained by resolving two unit clauses. Resolution with a unit clause
makes the result smaller.
- linear resolution: one clause in each step must be the result
of the previous step. This is a depth-first strategy. It may be necessary
to back up to a previous clause if no resolution with the current clause