Monadic Decomposition in Integer Linear Arithmetic

Matthew Hague, Anthony Lin, Philipp Ruemmer, Zhilin Wu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 Downloads (Pure)

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. 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.
Original languageEnglish
Title of host publicationInternational Joint Conference on Automated Reasoning
Subtitle of host publicationIJCAR 2020
PublisherSpringer-Verlag
Pages122-140
Number of pages19
DOIs
Publication statusE-pub ahead of print - 24 Jun 2020
EventInternational Joint Conference on Automated Reasoning - Paris, France
Duration: 29 Jun 20206 Jul 2020
Conference number: 10
https://ijcar2020.org/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12166

Conference

ConferenceInternational Joint Conference on Automated Reasoning
Abbreviated titleIJCAR
Country/TerritoryFrance
CityParis
Period29/06/206/07/20
Internet address

Keywords

  • Presburger Arithmetic, Monadic Decomposition, Logic, Theoretical Computer Science

Cite this