On Enumerating Short Projected Models

TL;DR

This paper introduces two novel algorithms for enumerating propositional models efficiently, focusing on avoiding repetitions through dual reasoning and blocking clauses, with formal correctness proofs.

Contribution

It presents two new model enumeration algorithms that utilize dual reasoning to shorten models and prevent duplicates, with formal calculus and correctness proofs.

Findings

Algorithms effectively avoid duplicate models.

Dual reasoning shortens found models.

Formal proofs ensure correctness.

Abstract

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.