Tractable Classes for Directional Resolution

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Computational Complexity of Reasoning

The original, resolution-based Davis-Putnam satisfiability algorithm (Davis and Putnam 1960) was recently revived by (Dechter and 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.