It is a well-known fact that propositional formulas in clause form (CNF formulas) with two literals per clause can be checked for satisfiability in polynomial time; that is, the problem 2-SAT is in P, while the problem k-SAT is NP-complete for each k greater than 2. The author presents a strategy for finding the shortest tree-like resolution refutation of an unsatisfiable formula. Due to the properties of the resolution calculus, such a refutation exists in the case that the formula of interest is indeed unsatisfiable.

The strategy strongly relies on some techniques from another paper [1], where it is proven that 2-SAT instances can be represented by “implication graphs,” which allow checking for satisfiability simply by checking for the existence of certain paths in the graph. The strategy can be formulated as a minimization problem exploiting a lemma proven here that states that the optimal-length refutation of a formula is composed of optimal-length derivations for some complementary literals in the formula. This allows for the formulation of a minimization procedure for the sum of the shortest proof lengths for complementary literals.

The strategy defined here is obvious, but original. Nevertheless, it would have been useful if the author had defined the concepts that are used in the argument, in particular the concept of implication graphs. This should not pose any space problems, since the paper is only five pages in length. So, the paper is not self-contained, which makes reading it more difficult.