论文标题
整数线性算术中的莫纳迪克分解（技术报告）
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
论文作者
论文摘要
莫尼达的可分解性是可变独立性的一个概念，它询问一阶理论中的给定公式是否可以作为该理论中的单质谓词的布尔组合表达。最近，Veanes等。在SMT的背景下（即输入公式不含量词），显示了单声道可分解性的有用性，并发现了包括字符串分析在内的各种有趣的应用。但是，通常不可确定地检查单质的可分解性。某些理论的可决定性是已知的（例如，伯堡算术，Tarski的真实领域），但是关于它们的计算复杂性的结果很少。在本文中，我们研究了SMT环境中整数线性算术的可分解性。我们表明，这个决策问题是综合的，并且在可声分解时，公式在最坏情况下承认了指数尺寸的分解。我们提供了结果的新应用，以通过长度约束来解决字符串约束。然后，我们将结果扩展到变异性的可分解性，其中谓词可以允许多个自由变量（与Monadic的可分解性相比）。最后，我们在整数线性算术中提供了消除量化器的应用，其中可以通过指数（而不是标准的双重指数）爆炸来消除一个量化器块（如果独立）中的变量。
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.
