2026-07-20T14:23:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26834 2026-07-09T11:31:09Z ddc:004 open_access

Constructing Small Monadic Decompositions in Presburger Arithmetic Ganardi, Moses Ricros, Marin Monadic decomposition variable independence 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Moses Ganardi and Marin Ricros 2026 Is Part Of LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.LICS.2026.47 urn:nbn:de:0030-drops-268346 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.47 eng https://creativecommons.org/licenses/by/4.0/legalcode