Exponential improvement of efficient backtracking: A strategy for plan-based deduction

Abstract

The paper presents a method of mechanical deduction along the lines indicated in [3]. Attempts to find refutation (s) are recorded in the form of triples: plan, constraints, conflicts. A plan corresponds to a portion of AND/OR graph search space and represents purely deductive structure of derivation. Constraints form a graph recording the attempts of unification, while con flicts identify minimal subset of the plan, removal of which restores unifiability. This method can be applied to any initial base of (nonnecessarily Horn) clauses. Unlike the exhaustive (blind) backtracking which treats all the goals deduced in the course of proof as equally probable source of failure, this approach detects the exact source of failure. In this method only a small fragment of solution space is kept on disk as as a collection of triples. The search strategy and the method of non-redundant processing of individual triples which leads to a solution (if it exists) is presented. This approach is compared — on a special case — with blind backtracking and an exponential improvement is demonstrated.