ABSTRACT. 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. input formula is quantifier-free), and found various interesting applications including string analysis. Despite these, 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). We provide 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
double exponential) blow-up.