To guess or to think? Hybrid algorithms for SAT

Abstract

Complete algorithms for solving propositional satisfiability fall into two main classes: backtracking search (e.g., the Davis-Putnam Procedure [1]) and resolution (e.g., the original Davis-Putnam Algorithm [2] and Directional Resolution [4]). Backtracking may be viewed as a systematic "guessing" of variable assignments, while resolution is inferring, or "thinking". Experimental results show that "pure guessing" or "pure thinking" might be inefficient. We propose an approach that combines both techniques 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 efficient than either of their components in isolation.