Optimizing Clause Resolution

Unification factoring addresses this problem by regarding the
indexing and unification phases of clause resolution as a single
process in which unification operations common to two or more clauses
are shared. This process is formalized through the construction of
factoring automata, an abstract model of the indexing/unification
process that accurately captures its cost. From a theoretical
standpoint, the challenging problem is the design of optimal
unification factoring, i.e., the construction of automata that
minimize the overall cost of unifying applicable clause heads with
any goal. We present complexity results for the construction of
optimal automata under a variety of conditions. On the practical
side, unification factoring is implemented through a source code
transformation that preserves the full semantics of Prolog. Using
this transformation, programs show performance improvements of up
to 300% across three widely used logic programming systems.
In addition, we show how factoring extends to the optimization
of tabled evaluation, which tightly integrates deductive database
and non-monotonic reasoning capabilities within a single logic
programming framework. The factoring automaton model is naturally
extended to account for the additional costs associated with tabled
evaluation. As with the basic factoring model, we show complexity
results for optimal factoring for tabled evaluation. Heuristics are
given for the cases in which optimal factoring is computationally
difficult, and the effectiveness of these heuristics is demonstrated
by performance improvements on a set of deductive database
benchmarks.