We study the problem of enumerating the satisfying assignments for circuit classes from knowledge compilation, where assignments are ranked in a specific order. In particular, we show how this problem can be used to efficiently perform ranked enumeration of the answers to MSO queries over trees, with the order being given by a ranking function satisfying a subset-monotonicity property. Assuming that the number of variables is constant, we show that we can enumerate the satisfying assignments in ranked order for so-called multivalued circuits that are smooth, decomposable, and in negation normal form (smooth multivalued DNNF). There is no preprocessing and the enumeration delay is linear in the size of the circuit times the number of values, plus a logarithmic term in the number of assignments produced so far. If we further assume that the circuit is deterministic (smooth multivalued d-DNNF), we can achieve linear-time preprocessing in the circuit, and the delay only features the logarithmic term.
翻译:我们研究了知识编译中电路类满足赋值的枚举问题,其中赋值按特定顺序排序。特别地,我们展示了该问题如何高效用于对树结构上的MSO查询答案进行排序枚举,排序由满足子集单调性的排序函数决定。在变量数量恒定的假设下,我们证明可以对满足光滑性、可分解性且处于否定范式的所谓多值电路(光滑多值DNNF)按排序顺序枚举其满足赋值。该过程无需预处理,枚举延迟与电路规模乘以取值数量呈线性关系,且包含当前已生成赋值数量的对数项。若进一步假设该电路是确定性的(光滑多值d-DNNF),我们可在电路上实现线性时间预处理,延迟仅包含该对数项。