On Enumerating Short Projected Models
Sibylle M\"ohle (Max Planck Institute for Informatics), Roberto, Sebastiani (University of Trento), Armin Biere (University of Freiburg)

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
