We study the problem of enumerating the answers to a query formulated in monadic second order logic (MSO) over an unranked forest F that is compressed by a straight-line program (SLP) D. Our main result states that this can be done after O(|D|) preprocessing and with output-linear delay (in data complexity). This is a substantial improvement over the previously known algorithms for MSO-evaluation over trees, since the compressed size |D| might be much smaller than (or even logarithmic in) the actual data size |F|, and there are linear time SLP-compressors that yield very good compressions on practical inputs. In particular, this also constitutes a meta-theorem in the field of algorithmics on SLP-compressed inputs: all enumeration problems on trees or strings that can be formulated in MSO-logic can be solved with linear preprocessing and output-linear delay, even if the inputs are compressed by SLPs. We also show that our approach can support vertex relabelling updates in time that is logarithmic in the uncompressed data. Our result extends previous work on the enumeration of MSO-queries over uncompressed trees and on the enumeration of document spanners over compressed text documents.
翻译:我们研究了在通过直线式程序(SLP)D压缩的无序森林F上,枚举以单子二阶逻辑(MSO)表述的查询结果的问题。我们的主要结果表明,经过O(|D|)的预处理后,可以在输出线性延迟(数据复杂度意义上)完成该枚举任务。这相较于先前已知的树结构上MSO求值算法有显著改进,因为压缩后的大小|D|可能远小于(甚至是对数级别于)实际数据大小|F|,且存在线性时间的SLP压缩器能在实际输入上实现高效压缩。特别地,这也构成了SLP压缩输入算法领域的一个元定理:所有可在MSO逻辑中表述的树或字符串枚举问题,即使输入被SLP压缩,也能以线性预处理和输出线性延迟求解。我们还证明了所提方法能以未压缩数据大小的对数时间支持顶点重标记更新。本研究成果扩展了先前关于未压缩树上MSO查询枚举以及压缩文本文档上文档跨度枚举的相关工作。