Modern SAT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted&Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignment that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for SAT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted&Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted&Greenbaum transformation with NNF preprocessing upfront -- which is typically not used in solving -- can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.

翻译：现代SAT求解器旨在处理以合取范式（CNF）表达的问题，因此非CNF问题必须预先转化为CNF形式，通常采用Tseitin变换或Plaisted&Greenbaum变换的变体。然而，当从求解过渡到枚举时，生成尽可能小的部分满足赋值的能力变得至关重要，这引发了一个问题：这类CNF编码是否同样适用于枚举。本文从理论和实证两方面研究了CNF转换对SAT枚举的有效性。在消极方面，我们证明：（i）Tseitin变换阻止求解器生成短的部分赋值，从而严重影响枚举的有效性；（ii）Plaisted&Greenbaum变换仅能部分克服这一问题。在积极方面，我们表明：将Plaisted&Greenbaum变换与通常求解中不使用的NNF预处理相结合，可以完全克服该问题，并显著减少部分赋值的数量和执行时间。