Tractable Classes for Directional Resolution

Abstract

The original, resolution-based Davis-Putnam satisfiability algorithm (Davis & Putnam 1960) was recently revived by (Dechter & Rish 1994) under the name "directional resolution" (DR). We provide new positive complexity results for DR. First, we identify a class of theories (ACT, Acyclic Component Theories) , which includes many real-world theories, for which DR takes polynomial time. Second, we present an improved analysis of the complexity of directional resolution through refined notions of induced width, which yields new tractable classes for DR, and much better predictions of its space and time requirements under various atom orderings. These estimates can be used for heuristically choosing among various orderings before running DR. Introduction The original, resolution-based Davis-Putnam satisfiability algorithm (Davis & Putnam 1960) was recently revived by (Dechter & Rish 1994; Rish & Dechter 2000) under the name "directional resolution" (DR). DR was shown to be a re...