Cargando…
Monadic Decomposition in Integer Linear Arithmetic
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. t...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324128/ http://dx.doi.org/10.1007/978-3-030-51074-9_8 |
_version_ | 1783551886275641344 |
---|---|
author | Hague, Matthew Lin, Anthony W. Rümmer, Philipp Wu, Zhilin |
author_facet | Hague, Matthew Lin, Anthony W. Rümmer, Philipp Wu, Zhilin |
author_sort | Hague, Matthew |
collection | PubMed |
description | 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. |
format | Online Article Text |
id | pubmed-7324128 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73241282020-06-30 Monadic Decomposition in Integer Linear Arithmetic Hague, Matthew Lin, Anthony W. Rümmer, Philipp Wu, Zhilin Automated Reasoning Article 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. 2020-05-30 /pmc/articles/PMC7324128/ http://dx.doi.org/10.1007/978-3-030-51074-9_8 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic. |
spellingShingle | Article Hague, Matthew Lin, Anthony W. Rümmer, Philipp Wu, Zhilin Monadic Decomposition in Integer Linear Arithmetic |
title | Monadic Decomposition in Integer Linear Arithmetic |
title_full | Monadic Decomposition in Integer Linear Arithmetic |
title_fullStr | Monadic Decomposition in Integer Linear Arithmetic |
title_full_unstemmed | Monadic Decomposition in Integer Linear Arithmetic |
title_short | Monadic Decomposition in Integer Linear Arithmetic |
title_sort | monadic decomposition in integer linear arithmetic |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324128/ http://dx.doi.org/10.1007/978-3-030-51074-9_8 |
work_keys_str_mv | AT haguematthew monadicdecompositioninintegerlineararithmetic AT linanthonyw monadicdecompositioninintegerlineararithmetic AT rummerphilipp monadicdecompositioninintegerlineararithmetic AT wuzhilin monadicdecompositioninintegerlineararithmetic |