  Variable independence and decomposability are algorithmic techniques for
simplifying logical formulas by tearing apart connections between free
variables. These techniques were originally proposed to speed up query
evaluation in constraint databases, in particular by representing the query as
a Boolean combination of formulas with no interconnected variables. They also
have many other applications in SMT, string analysis, databases, automata
theory and other areas. However, the precise complexity of variable
independence and decomposability has been left open especially for the
quantifier-free theory of linear real arithmetic (LRA), which is central in
database applications. We introduce a novel characterization of formulas
admitting decompositions and use it to show that it is coNP-complete to decide
variable decomposability over LRA. As a corollary, we obtain that deciding
variable independence is in $ \Sigma_2^p $. These results substantially improve
the best known double-exponential time algorithms for variable decomposability
and independence. In many practical applications, it is crucial to be able to
efficiently eliminate connections between variables whenever possible. We
design and implement an algorithm for this problem, which is optimal in theory,
exponentially faster compared to the current state-of-the-art algorithm and
efficient on various microbenchmarks. In particular, our algorithm is the first
one to overcome a fundamental barrier between non-discrete and discrete
first-order theories. Formulas arising in practice often have few or even no
free variables that are perfectly independent. In this case, our algorithm can
compute a best-possible approximation of a decomposition, which can be used to
optimize database queries by exploiting partial variable independence, which is
present in almost every logical formula or database query constraint.
