Abstract
Complete algorithms for solving propositional satisfiability fall into two main classes: backtracking (e.g., the Davis-Putnam Procedure [4]) and resolution (e.g., Directional Resolution [9]). Roughly speaking, backtracking amounts to "guessing" (making assumption), while resolution invokes "thinking" (inference). Experimental results show that both "pure guessing" and "pure thinking" might be inefficient. We propose an approach that combines resolution and backtracking and yields a family of hybrid algorithms, parameterized by a bound on the "effective" amount of resolution allowed. The idea is to divide the set of propositional variables into two classes: conditioning variables, which are assigned truth values, and resolution variables, which are resolved upon. We report on preliminary experimental results demonstrating that on certain classes of problems hybrid algorithms are more effective than either the Davis-Putnam Procedure or Directional Resolution in isolation.