Next: Remove Redundant Constraints Up: The Omega Test Previous: Eliminate Existentially Quantified

Verify the Existence of Solutions

The Omega test also provides direct support for checking if integer solutions exist to a set of linear constraints. It does this by treating all the variables as existentially quantified and eliminating variables until it produces a problem containing a single variable; such problems are easy to check for integer solutions. The Omega test incorporates several extensions over a naive application of variable elimination.


omega@cs.umd.edu