Forall-exist statements in pseudopolynomial time

Given a convex set Q ⊆ R m and an integer matrix W ∈ Z m×n , we consider statements of the form ∀b ∈ Q ∩ Z m ∃x ∈ Z n s.t. W x ≤ b. Such statements can be verified in polynomial time with the algorithm of Kannan and its improvements if n is fixed and Q is a polyhedron. The running time of the best-known algorithms is doubly exponential in n.

We provide a pseudopolynomial-time algorithm if m is fixed. Its running time is (m∆) O(m 2 ) where ∆ is the largest absolute value of an entry in W . Furthermore it applies to general convex sets Q.