一句话:提出基于进度测度的准多项式时间奇偶博弈求解算法,将空间需求从准多项式降至近线性。
奇偶博弈求解长期是逻辑与验证中的核心问题,此前最优算法仅为温和次指数;Calude 等人的突破首次给出准多项式时间算法,但空间开销为准多项式。本文提出一种基于进度测度(progress measures)的替代准多项式时间算法,其核心是一个新的有序树编码概念,以及用有界自适应多计数器证明的简洁树编码结果。新算法在保持准多项式时间的同时,将所需空间从准多项式降到近线性。两个树编码工具本身也具有独立意义。评估主要通过理论算法分析与复杂度证明,而非实验。
The recent breakthrough paper by Calude et al. has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multi-counters, both of which are interesting in their own right.