We investigate conjunctive normal form (CNF) encodings of a function represented with a smooth decomposable negation normal form (DNNF). Several encodings of DNNFs and decision diagrams were considered by (Abio et al. 2016). The authors differentiate between encodings which implement consistency or domain consistency from encodings which implement unit refutation completeness or propagation completeness (in both cases implements means by unit propagation). The difference is that in the former case we do not care about properties of the encoding with respect to the auxiliary variables while in the latter case we treat all variables (the input ones and the auxiliary ones) in the same way. The latter case is useful if a DNNF is a part of a problem containing also other constraints and a SAT solver is used to test satisfiability. The currently known encodings of smooth DNNF theories implement domain consistency. Building on this and the result of (Abio et al. 2016) on an encoding of decision diagrams which implements propagation completeness, we present a new encoding of a smooth DNNF which implements propagation completeness. This closes the gap left open in the literature on encodings of DNNFs.

研究了使用可分解的否定范式（DNNF）表示的函数的共同正常形式（CNF）编码。作者区分了用于实现一致性或域一致性的编码和用于实现单元证明完备性或传播完备性的编码。当前已知的DNNF理论编码实现了域一致性。在此基础上，我们对决策图的传播完整编码进行了推广，并针对具有有限域的变量提出了DNNF的传播完整编码的推广。

平滑DNNF理论传播完全编码