Constructing Small Monadic Decompositions in Presburger Arithmetic

A monadic decomposition of a formula over a first-order theory is an equivalent Boolean combination of atomic formulas, each containing only one variable. Monadic decomposition is a generic simplification technique that has found applications in various settings such as quantifier elimination, string solving, and constraint databases. Previous work has mostly focused on the decision problem of whether a formula admits a monadic decomposition. However, much less is known on how to efficiently produce a small monadic decomposition, which is required for any application.

We study this question for the quantifier-free fragment of Presburger arithmetic. Here, monadic decomposability is known to be coNP-complete, and monadic decompositions can be computed in exponential time. An exponential size lower bound was only known for monadic decompositions in disjunctive or conjunctive normal form (DNF or CNF). In this work, we extend this exponential lower bound to general monadic decompositions. Guided by this lower bound, we present fragments that admit polynomially-sized monadic decompositions, which, in many cases, can be constructed efficiently. A surprising key ingredient in our proof is a family of small-depth circuits for arithmetic operations in Chinese remainder representation.