带计数量词的双变量片段中加权一阶模型计数的复杂性：一个待超越的界限

我们研究了在具有两个变量和计数量词的逻辑语言上，加权一阶模型计数（WFOMC）的时间复杂性。已知该问题可在关于域大小的多项式时间内求解。然而，对于大多数实际应用而言相对较高的多项式次数，此前从未得到过妥善处理。首先，我们为现有求解带计数量词的 WFOMC 技术给出了一个时间复杂性界限。已知该界限是一个多项式，其次数取决于输入公式的单元数量。我们观察到，单元数量反过来以指数方式依赖于公式中出现的计数量词的参数。其次，我们提出了一种处理计数量词的新方法，将指数依赖关系降为二次依赖关系，从而获得了更紧的上界。多项式次数对计数量词的依赖关系能否进一步降低仍是一个开放问题，因此我们的新界限是一个待超越的界限。