论二维约束循环问题的判定
On Deciding the Constraint Loop Problem in Dimension Two
Daria Goliasova, Toghrul Karimov
AI 速览：作者通过分析无限运行见证的结构，将二维线性约束循环终止性判定从多项式空间改进到多项式时间，并给出基于 Z3 的实现。
Recently, Guilmant, Lefaucheux, Ouaknine, and Worrell [2] proved decidability of the termination problem for linear constraint loops over two real-valued variables, thus settling a wellknown open problem. Their algorithm is based on a theoretical result that such a loop does not terminate if and only if it has a witness of an infinite run of a specific shape. By analysing the structure of the witness carefully, we show that termination such loops can be decided in polynomial time, improving on the polynomial space bound argued by Guilmant et al. We also present an efficient implementation of the polynomial-time algorithm based on the satisfiability modulo theories (SMT) solver Z3.