Projects per year
Abstract
Monadic decomposability is a notion of variable independence, which asks whether a given formula in a firstorder 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 quantifierfree), 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 RealClosed 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 coNPcomplete 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) blowup.
Original language  English 

Title of host publication  International Joint Conference on Automated Reasoning 
Subtitle of host publication  IJCAR 2020 
Publisher  SpringerVerlag 
Pages  122140 
Number of pages  19 
DOIs  
Publication status  Epub ahead of print  24 Jun 2020 
Event  International Joint Conference on Automated Reasoning  Paris, France Duration: 29 Jun 2020 → 6 Jul 2020 Conference number: 10 https://ijcar2020.org/ 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
Volume  12166 
Conference
Conference  International Joint Conference on Automated Reasoning 

Abbreviated title  IJCAR 
Country/Territory  France 
City  Paris 
Period  29/06/20 → 6/07/20 
Internet address 
Keywords
 Presburger Arithmetic, Monadic Decomposition, Logic, Theoretical Computer Science
Projects
 1 Finished

String Constraint Solving with RealWorld Regular Expressions
Hague, M. (PI)
Eng & Phys Sci Res Council EPSRC
1/07/19 → 30/06/22
Project: Research