next up previous
Next: Application of The Up: Omega Test Previous: Omega Test

Capabilities of the Omega Test

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.



next up previous
Next: Application of The Up: Omega Test Previous: Omega Test



Generated by latex2html-95.1
Fri Jul 12 14:53:37 EDT 1996