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 and Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignments 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 and Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted and 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前置转换（这在求解中通常不被使用）相结合，能够完全解决上述问题，并显著减少部分赋值的数量和执行时间。