A new algorithm for testing satisfiability of propositional formulas in conjunctive normal form (CNF)
is described. It applies reasoning in the form of certain resolution operations, and identification of
equivalent literals. Resolution produces growth in the size of the formula, but within a global quadratic
bound; most previous methods avoid operations that produce any growth, and generally do not identify
equivalent literals. Computational experience indicates that the method does substantially less
\guessing" than previously reported algorithms, while keeping a polynomial time bound on the work
done between guesses. Experiments indicate that, for larger problems, the time investment in reasoning
returns a profit in reduced searching, and the profit increases with increasing problem size.