Browse Prior Art Database

The Transformation of Arc Consistency over Herbrand Terms into Linear Constraints

IP.com Disclosure Number: IPCOM000116179D
Original Publication Date: 1995-Aug-01
Included in the Prior Art Database: 2005-Mar-30
Document File: 6 page(s) / 208K

Publishing Venue

IBM

Related People

Lock, HCR: AUTHOR

Abstract

The invention consists of the following steps: approximation of link sets by sets of flat linear terms (so-called types), coding of flat terms by bijective mapping to natural numbers, enlarging the program with type arguments and coding of the possible links of a predicate by constraints over type arguments. A significant point is the innovative coding of the constraints by linear inequalities over finite domains of natural numbers (so-called finite domain constraints), because efficient procedures exist for the solution of such inequality systems.

This text was extracted from an ASCII text file.
This is the abbreviated version, containing approximately 26% of the total text.

The Transformation of Arc Consistency over Herbrand Terms into Linear
Constraints

      The invention consists of the following steps: approximation of
link sets by sets of flat linear terms (so-called types), coding of
flat terms by bijective mapping to natural numbers, enlarging the
program with type arguments and coding of the possible links of a
predicate by constraints over type arguments.  A significant point is
the innovative coding of the constraints by linear inequalities over
finite domains of natural numbers (so-called finite domain
constraints), because efficient procedures exist for the solution of
such inequality systems.

      The central mechanism in the implementation of a (Horn-) logic
programming language resolves (solves) a set of indivisible formulae
(atoms) by resolving each atom while ensuring that the links of the
individual solution steps are mutually compatible.

      The mechanism can be compared with solving a crossword puzzle
by blind search, a vacant row or column playing the part of an atom
and the crossword puzzle that of the formula set.  Two words must
feature the same letter at the point where they intersect.  Finding
these letters can be compared with the task of finding compatible
links for variables occurring simultaneously in several atoms.
Filling in a vacant row or column can block other, correct solutions
at the intersection points, as a consequence of which a step
backwards must be taken in order to try an alternative solution.
Astonishingly, most implementations of logical programming languages,
e.g., Prolog, are based on this naive- search principle.

      What is needed to improve this approach is a look-ahead at the
restrictions which will result from future solution steps, in order
to discard those options which the look ahead has excluded.

      The disclosed approach offers an implementation for a
restricted form of generalized propagation: from an untyped program
types are derived which approximate the possible link sets of the
program variables.  The types are then inserted into the program in
the form of constraints, thus enlarging the program.  The innovation
is the concept of how this enlargement is technically carried out and
how the constraints are coded.

      The new transformation technique is based on two central ideas:
the bijective mapping of types (approximations) to natural numbers
and the mapping of unification conditions (from the program's clause
headings) to linear inequality systems over finite domains of natural
numbers.  Here the unification conditions are coded by number tuples,
and inequality systems define the set of all valid tuples in the
Cartesian product.  By means of the inequality systems (constraints)
possible insertions in the individual columns of the tuple can be
restricted, the columns here corresponding to variables occurring in
atoms and the tuples to the insertion combinations of all variables
occurring in the atom. ...