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),则可在电路上实现线性时间预处理,且延迟仅包含对数项。