We study Satisfiability Modulo Theories (SMT) enriched with the so-called Ramsey quantifiers, which assert the existence of cliques (complete graphs) in the graph induced by some formulas. The extended framework is known to have applications in proving program termination (in particular, whether a transitive binary predicate is well-founded), and monadic decomposability of SMT formulas. Our main result is a new algorithm for eliminating Ramsey quantifiers from three common SMT theories: Linear Integer Arithmetic (LIA), Linear Real Arithmetic (LRA), and Linear Integer Real Arithmetic (LIRA). In particular, if we work only with existentially quantified formulas, then our algorithm runs in polynomial time and produces a formula of linear size. One immediate consequence is that checking well-foundedness of a given formula in the aforementioned theory defining a transitive predicate can be straightforwardly handled by highly optimized SMT-solvers. We show also how this provides a uniform semi-algorithm for verifying termination and liveness with completeness guarantee (in fact, with an optimal computational complexity) for several well-known classes of infinite-state systems, which include succinct timed systems, one-counter systems, and monotonic counter systems. Another immediate consequence is a solution to an open problem on checking monadic decomposability of a given relation in quantifier-free fragments of LRA and LIRA, which is an important problem in automated reasoning and constraint databases. Our result immediately implies decidability of this problem with an optimal complexity (coNP-complete) and enables exploitation of SMT-solvers. It also provides a termination guarantee for the generic monadic decomposition algorithm of Veanes et al. for LIA, LRA, and LIRA. We report encouraging experimental results on a prototype implementation of our algorithms on micro-benchmarks.

翻译：我们研究了在可满足性模理论（SMT）的基础上引入所谓拉姆齐量词的问题，这些量词断言由某些公式所诱导的图中存在团（完全子图）。已知该扩展框架在证明程序终止性（特别是传递二元谓词是否为良基的）以及SMT公式的单调可分解性方面具有应用价值。我们的主要成果是一种新算法，用于从三种常见的SMT理论中消除拉姆齐量词：线性整数算术（LIA）、线性实数算术（LRA）以及线性整数实数算术（LIRA）。特别地，若我们仅处理存在量化公式，则该算法在多项式时间内运行，并生成一个线性规模的公式。其直接推论是：通过高度优化的SMT求解器，可以简洁地判定上述理论中定义传递谓词的给定公式的良基性。我们还展示了该方法如何为几类著名的无限状态系统（包括简洁定时系统、单计数器系统和单调计数器系统）提供一种保证完备性（实际上具有最优计算复杂性）的、用于验证终止性和活性的统一半算法。另一直接推论是解决了LRA和LIRA无量词片段中给定关系单调可分解性判定的一个开放问题，该问题是自动推理和约束数据库领域的重要问题。我们的成果立即意味着该问题具有可判定性，并具有最优复杂度（coNP完全性），同时能够利用SMT求解器。该成果还为Veanes等人针对LIA、LRA和LIRA提出的通用单调分解算法提供了终止性保证。我们基于算法原型在微基准测试上的实验展现了令人鼓舞的结果。