Bradley-Manna-Sipma 字典序排序函数的复杂性

本文将焦点转向由 Bradley、Manna 和 Sipma 在 2005 年 CAV 奠基性论文中引入的一类字典序排序函数，并首次确立了涉及为线性约束循环（无前条件）推断此类函数的一些问题的复杂性。我们表明，如果存在这样的函数，可以在多项式时间内找到它，且当变量取值范围为有理数（或实数）时，该方法是可靠且完备的。我们表明，当变量取值范围为整数时，问题更为困难——判定排序函数的存在性是 coNP-完全的。接下来，我们研究了最小化排序函数中分量数量（即维度）的问题。该数量在计算迭代界限和循环并行化等语境中很有趣。令人惊讶的是，与某些其他类字典序排序函数的情况不同，我们发现即使判定是否存在双分量排序函数也比无限制问题更难：在有理数上是 NP-完全的，在整数上是 $\Sigma^P_2$-完全的。