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