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预处理（这在求解中通常不使用）相结合，可以完全克服该问题，并显著减少部分赋值的数量和执行时间。