  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.
