We study the problem of enumerating Tarski fixed points, focusing on the relational lattices of equivalences, quasiorders and binary relations. We present a polynomial space enumeration algorithm for Tarski fixed points on these lattices and other lattices of polynomial height. It achieves polynomial delay when enumerating fixed points of increasing isotone maps on all three lattices, as well as decreasing isotone maps on the lattice of binary relations. In those cases in which the enumeration algorithm does not guarantee polynomial delay on the three relational lattices on the other hand, we prove exponential lower bounds for deciding the existence of three fixed points when the isotone map is given as an oracle, and that it is NP-hard to find three or more Tarski fixed points. More generally, we show that any deterministic or bounded-error randomized algorithm must perform a number of queries asymptotically at least as large as the lattice width to decide the existence of three fixed points when the isotone map is given as an oracle. Finally, we demonstrate that our findings yield a polynomial delay and space algorithm for listing bisimulations and instances of some related models of behavioral or role equivalence.
翻译:我们研究了枚举Tarski不动点的问题,重点关注等价关系、拟序关系和二元关系的关系格。针对这些格及其他多项式高度格,我们提出了一种多项式空间的Tarski不动点枚举算法。该算法在枚举三个格上递增保序映射的不动点以及二元关系格上递减保序映射的不动点时,实现了多项式延迟。然而,对于枚举算法无法保证在这三个关系格上实现多项式延迟的情形,我们证明了:当保序映射以预言机形式给出时,判定三个不动点存在性具有指数下界,且寻找三个或更多Tarski不动点是NP难的。更一般地,我们证明:任何确定性算法或有界错误随机算法,当保序映射以预言机形式给出时,要判定三个不动点的存在性,其查询次数渐近地至少与格宽度相当。最后,我们证明了这些结果可为列举双模拟关系及相关行为等价或角色等价模型的实例提供多项式延迟与空间的算法。