Propositional model enumeration, or All-SAT, is the task to record all models of a propositional formula. It is a key task in software and hardware verification, system engineering, and predicate abstraction, to mention a few. It also provides a means to convert a CNF formula into DNF, which is relevant in circuit design. While in some applications enumerating models multiple times causes no harm, in others avoiding repetitions is crucial. We therefore present two model enumeration algorithms, which adopt dual reasoning in order to shorten the found models. The first method enumerates pairwise contradicting models. Repetitions are avoided by the use of so-called blocking clauses, for which we provide a dual encoding. In our second approach we relax the uniqueness constraint. We present an adaptation of the standard conflict-driven clause learning procedure to support model enumeration without blocking clauses.Our procedures are expressed by means of a calculus and proofs of correctness are provided.

翻译：命题模型枚举，或称All-SAT，其任务是记录一个命题公式的所有模型。这是软件与硬件验证、系统工程以及谓词抽象等领域的核心任务之一。它同时也提供了一种将CNF公式转换为DNF公式的方法，这在电路设计中具有重要意义。虽然在部分应用中多次枚举模型并无妨害，但在其他应用中避免重复至关重要。为此，我们提出了两种模型枚举算法，它们采用对偶推理以缩短所找到的模型。第一种方法枚举两两矛盾的模型。通过使用所谓的阻塞子句来避免重复，我们为此提供了一种对偶编码。在我们的第二种方法中，我们放宽了唯一性约束。我们提出了一种对标准冲突驱动子句学习过程的改进，以支持无需阻塞子句的模型枚举。我们的过程通过演算形式表达，并提供了正确性证明。