A wide range of symbolic analysis and optimization problems can be formalized using polyhedra. Sub-classes of polyhedra, also known as sub-polyhedral domains, are sought for their lower space and time complexity. We introduce the Strided Difference Bound Matrix (SDBM) domain, which represents a sweet spot in the context of optimizing compilers. Its expressiveness and efficient algorithms are particularly well suited to the construction of machine learning compilers. We present decision algorithms, abstract domain operators and computational complexity proofs for SDBM. We also conduct an empirical study with the MLIR compiler framework to validate the domain's practical applicability. We characterize a sub-class of SDBMs that frequently occurs in practice, and demonstrate even faster algorithms on this sub-class.

翻译：大量符号分析与优化问题均可通过多面体形式化表达。为降低时空复杂度，研究者常寻求多面体的子类（亦称子多面体域）。本文提出跨步差分界矩阵（SDBM）域，该域在优化编译器语境中实现了性能与表达能力的平衡。其表达能力和高效算法尤其适用于机器学习编译器的构建。我们为SDBM提供了判定算法、抽象域算子及计算复杂性证明，并基于MLIR编译器框架开展实证研究以验证该域的实际适用性。此外，我们刻画了实践中频繁出现的SDBM子类，并针对该子类展示了更快速的算法。