Extending Modern SAT Solvers for Enumerating All Models
This addresses a fundamental problem in SAT solving for applications like sequence mining, but it appears incremental as it extends existing solvers.
The paper tackles the problem of enumerating all models of Boolean CNF formulas by extending CDCL-based SAT solvers, and it provides experimental evaluation on SAT challenge instances and SAT-based sequence mining problems.
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.