Abstract
The paper presents algorithm directional resolution, a variation on the original Davis-Putnam algorithm, and analyzes its worst-case behavior as a function of the topological structure on the theories. Th notions of induced width and diversity are shown to play a key role in bounding the complexity of the procedure. The inportance of our analysis lies in highlighting structure-based tractable classes of satisfiability and in providing theoretical guarantees on the time and space complexity of the algorithm. Contrary to previous assesments, we show that for many theories directional resolution could be an effective procedure. Our empirical test confirm theoretical prediction, showing that on problems with special structures, like chains, directional resolution greatly outperforms one of the most effective satisfiability algorithms known to date, namely the popular Davis-Puntnam procedure.