2.3 Resolution

Resolution (RES) is a widely studied simple proof system that can be used to prove unsatisfiability of CNF formulas. Our complexity results concerning the power of clause learning are in relation to this system. The resolution rule states that given clauses (A $\vee$ x) and (B $\vee$ $\neg$x), we can derive clause (A $\vee$ B) by resolving on x. A resolution derivation of C from a CNF formula F is a sequence $\pi$ = (C₁, C₂,..., C_s $\equiv$ C) where each clause C_i is either a clause of F (an initial clause) or derived by applying the resolution rule to C_j and C_k, j, k < i (a derived clause). The size of $\pi$ is s, the number of clauses occurring in it. We will assume that each C_j$\ne$C in $\pi$ is used to derive at least one other clause C_i, i > j. Any derivation of the empty clause $\Lambda$ from F, also called a refutation or proof of F, shows that F is unsatisfiable.

Despite its simplicity, unrestricted resolution is hard to implement efficiently due to the difficulty of finding good choices of clauses to resolve; natural choices typically yield huge storage requirements. Various restrictions on the structure of resolution proofs lead to less powerful but easier to implement refinements that have been studied well, such as tree-like, regular, linear, positive, negative, semantic, and Davis-Putnam resolution. Tree-like resolution uses non-empty derived clauses exactly once in the proof and is equivalent to an optimal DPLL procedure. Regular resolution allows any variable to be resolved upon at most once along any ``path'' in the proof from an initial clause to $\Lambda$, allowing (restricted) reuse of derived clauses. Linear resolution requires each clause C_i in a derivation (C₁, C₂,..., C_s) to be either an initial clause or be derived by resolving C_i-1 with C_j, j < i - 1. For any assignment $\alpha$ to the variables, an $\alpha$-derivation requires at least one clause involved in each resolution step to be falsified by $\alpha$. When $\alpha$ is the all FALSE assignment, the derivation is positive. When it is the all TRUE assignment, the derivation is negative. A derivation is semantic if it is an $\alpha$-derivation for some $\alpha$. Davis-Putnam resolution, also called ordered resolution, is a refinement of regular resolution where every sequence of variables in a path from an initial clause to $\Lambda$ respects the same ordering on the variables.

While all these refinements are sound and complete as proof systems, they differ in efficiency. For instance, regular, linear, positive, negative, semantic, and Davis-Putnam resolution are all known to be exponentially stronger than tree-like resolution (Bonet et al., 2000, Bonet and Galesi, 2001, Buresh-Oppenheim, 2003) whereas tree-like, regular, and Davis-Putnam resolution are known to be exponentially weaker than RES (Bonet et al., 2000, Alekhnovich et al., 2002).

Proposition 1   Tree-like, regular, linear, positive, negative, semantic, and Davis-Putnam resolution are natural refinements of RES.

Proposition 2 (Bonet et al. 2000, Alekhnovich et al. 2002)   Tree-like, regular, and Davis-Putnam resolution are exponentially-proper natural refinements of RES.