Extending Modern SAT Solvers for Enumerating All Models

TL;DR

This paper extends modern SAT solvers to efficiently enumerate all models of a CNF formula, providing a practical approach validated on benchmark and real-world instances.

Contribution

It introduces an extension to CDCL-based SAT solvers specifically designed for model enumeration, a novel adaptation for this fundamental problem.

Findings

Effective enumeration of all models demonstrated on SAT challenge instances

Successful application to sequence mining problem encodings

Enhanced SAT solver capabilities for comprehensive solution space exploration

Abstract

In this paper, we address the problem of enumerating all models of a Boolean formula in conjunctive normal form (CNF). We propose an extension of CDCL-based SAT solvers to deal with this fundamental problem. Then, we provide an experimental evaluation of our proposed SAT model enumeration algorithms on both satisfiable SAT instances taken from the last SAT challenge and on instances from the SAT-based encoding of sequence mining problems.