Solving Integer Programs from Dependence and Synchronization Problems

We present a method to determine whether a set of equations has a non-negative integer solution. The method is designed for the particular occurence of this problem in the context of compiler analysis of parallel programs. The system of equations is first transformed to Smith normal form to determine if any integer solutions exist. In case of multiple integer solutions, a parameterized solution space representing all non-negative solutions is obtained. Fourier-Motzkin elimination is employed to determine if the real solution space is empty. If the solution space is not empty, either the existence of an integer solution is readily verified, or a simplified convex region is obtained such that the original system of equations has a solution if and only if this convex region contains an integer point. The main result of the paper is a set of new heuristic search procedures that are used to identify an integer solution in a convex region, or to prove that no integer solution exists. These a..