Abstract:
While clause resolution is central to logic programming, practical efforts to optimize resolution have largely concerned efficient clause indexing. One recent exception is Unification Factoring which optimizes backtracking through clause heads of a predicate. Now we consider the problem of optimizing clause resolution in a more general setting than Unification Factoring. One fundamental change is to use mode information to distinguish between elementary matching and unification operations that arise in unifying a term. In addition, we expand the traditional notion of clause resolution to allow for tabled predicates. The result is that our optimization technique becomes relevant for both top-down and bottom-up evaluations.Our technique uses Clause Resolution Automata (CRA), to model clause resolution in this expanded setting. The CRAs enable us to succinctly capture the cost of resolution. Furthermore, they can be readily implemented as a source transformation. After formally developing the notion of CRAs and their associated costs, we consider the problem of constructing optimal CRAs. We show that the complexity of construction depends on a variety of conditions: whether a predicate is tabled, whether clause order is to be preserved, and the information known about modes. For classes of programs where optimal CRAs can be constructed in polynomial time, dynamic programming algorithms are specified for their construction. For those classes of programs where construction of optimal CRAs is not known to be polynomial, we develop heuristics for constructing CRAs and establish their properties. Finally, we present experimental results that show the impact of our approach on the performance (time and space usage) of a set of representative programs.
Bibtex Entry:
@inproceedings{DRRS:ILPS95, author = {Steven Dawson and C. R. Ramakrishnan and I. V. Ramakrishnan and Terrance Swift}, title = {Optimizing Clause Resolution: Beyond Unification Factoring}, booktitle = {ilps}, publisher = {MIT Press}, pages = {194--208}, year = {1995} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)