Tractable Classes for Directional Resolution

Alvaro del Val, Universidad Autónoma de Madrid

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.