Browse Prior Art Database

Quantifier Elimination for Conjunctions of Linear Constraints via a Convex Hull

IP.com Disclosure Number: IPCOM000110039D
Original Publication Date: 1992-Oct-01
Included in the Prior Art Database: 2005-Mar-25
Document File: 6 page(s) / 307K

Publishing Venue

IBM

Related People

Lassez, C: AUTHOR [+2]

Abstract

A new algorithm for quantifier (variable) elimination for systems of linear constraints is proposed which uses a quasi-dual formulation and an on-line convex hull construction. The algorithm provides an exact solution when the size of the output is small and an approximation (upper or lower) in the general case when the size of the output may be exponential. Apart from trivial cases, existing algorithms fail in both respect.

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

Quantifier Elimination for Conjunctions of Linear Constraints via a Convex Hull

       A new algorithm for quantifier (variable) elimination for
systems of linear constraints is proposed which uses a quasi-dual
formulation and an on-line convex hull construction.  The algorithm
provides an exact solution when the size of the output is small and
an approximation (upper or lower) in the general case when the size
of the output may be exponential.  Apart  from trivial cases,
existing algorithms fail in both respect.

      Tarski (1) proved that most problems in elementary algebra and
Euclidean geometry can be solved by a single algorithm: quantifier
elimination.  The enormous potential for applications to Robotics,
Graphics, Constructive Solid Geometry and to new Constraint-based
Languages, such as CLP(R), Prolog III, CHIP and Mathematica, has not,
however, been realized.  The existing algorithms have been designed
for theoretical purposes, few are implemented and they have no
significant practical value.  A main reason is that the size of the
output may be doubly exponential and even toy problems cannot yet be
solved (2,3).  It has been remarked (1,4) that really practical
solutions will come only by concentrating on special cases.

      This problem is addressed in the very restricted case of
conjunctions of linear constraints.  This restriction still allows us
to solve in principle a wide range of interesting problems (5,6) and
is an important case in CLP(R), PROLOG III, CHIP where auxiliary
variables introduced during execution of a program have to be
eliminated (7).  At the theoretical level, despite the simplicity of
the constraints, the size of the output may still be exponential
raising in practice very serious problems of redundancy and
degeneracy.  Existing algorithms in general fail to produce any
output (not even partial information) because of the size or the
amount of intermediate computations.  As a consequence, existing
implementations use simple heuristics that work only for trivial
input or when very few variables are to be eliminated (7,8).

      The main novel features of the proposed algorithm are:
.  based on geometric constructions rather than algebraic
manipulations
.  complexity essentially based on size of output
.  produces exact projection when size of output or number of
remaining variables small
.  otherwise, produces approximation to a user-defined size

      Many of the shortcomings of the existing algorithms are due to
the fact that they perform algebraic manipulations and are based on
the syntax of the constraints rather than on their semantics.
However, it is known that quantifier elimination can be viewed
geometrically as an operation of projection.  The algorithm proposed
here exploits systematically this observation.  Two cases are
considered depending on whether the polyhedral set defined by the
input set of constraints is bounded or not.

      In the bounded...