Monadic decomposability is a notion of variable independence, which
asks whether a given formula in a first-order theory is expressible as
a Boolean combination of monadic predicates in the theory. Recently,
Veanes et al.  showed the usefulness of monadic decomposability in the
context of SMT (i.e. the input formula is quantifier-free), and found
various interesting applications including string analysis.  However,
checking monadic decomposability is undecidable in
general. Decidability for certain theories is known (e.g. Presburger
Arithmetic, Tarski's Real-Closed Field), but there are very few
results regarding their computational complexity.  In this paper, we
study monadic decomposability of integer linear arithmetic in the
setting of SMT.  We show that this decision problem is coNP-complete
and, when monadically decomposable, a formula admits a decomposition
of exponential size in the worst case.  We provide a new application
of our results to string constraint solving with length constraints.
We then extend our results to variadic decomposability, where
predicates could admit multiple free variables (in contrast to monadic
decomposability). Finally, we give an application to quantifier
elimination in integer linear arithmetic where the variables in a
block of quantifiers, if independent, could be eliminated with an
exponential (instead of the standard doubly exponential) blow-up.