Abstract
The paper compares two popular strategies for solving propositional satisfiability, backtracking search and resolution, and analyzes the complexity of a directional resolution algorithm (DR) as a function of the "width" (w*) of the problem's graph. Our empirical evaluation confirms theoretical prediction, showing that on low-w* problems DR is very eficient, greatly outperforming the backtracking-based Davis- Putnam-Logemann-Loveland procedure (DP). We also emphasize the knowledgecompilation properties of DR and extend it to a tree-clustering algorithm that facilitates query answering. Finally, we propose two hybrid algorithms that combine the advantages of both DR and DP. These algorithms use control parameters that bound the complexity of resolution and allow time/space trade-offs that can be adjusted to the problem structure and to the user's computational resources. Empirical studies demonstrate the advantages of such hybrid schemes.