The basic operation of the omega test is the elimination of an
existentially quantified variable. For example given a set of
constraints P over x,y and z, and a formula
,
the omega test is able to remove the existentially quantified variables
and report the answer just in term of the free variable x and y.
The omega test also provides directly support for checking if integer solution exists to set of linear constraints. It does this by treating all the variables as existentially quantified and eliminating variable until it produces a problem containing a single variable (these kind of problem are easy to check for integer solution).
In the normal omega test operation, any constraint that is made
redundant by any other single constraint, is eliminated.
By using this ability, formulas of the form of implication (
) can be
verified by checking to see if constraints of P are redundant, given
that Q are true.
The omega test simply decides if there is a solution to an integer
programming problem also it could be used for symbolic projection.
When used this way, the omega test is given as input an integer
programming program P and set of variables V, it projects P
into one or more problems involving only variables in V that
describe all the possible values of variables in V such that there
is an integer solution to P with those values.
The omega test doesn't put a domain constraints on an integer variable, and
it can take any values. This is a good property of the Omega test in
terms of polynomial time bounds. The time taken by the methods to
eliminate one equality constraints (in order to decreases the number
of variable) is
where m and n are the number
of constraints, variables respectively. C is coefficient with the
largest absolute value in the constraints.
Eliminating unbound variables takes
worst-case time, where
p is the number of passes required to eliminate all the variable that
became unbound.